package subtype-refinement

subtype-refinement

Refinement types encoded with private types in OCaml.

Installation

Production/release version:

$ opam install subtype-refinement

Development/snapshot version (on this project directory):

$ opam install .

Usage

This package provides statically checked refinement types, but casts into such refined types are deferred until runtime (this is due the use of functions as constraints, so these constraints must be evaluated before they are applied to "type-check" some value). By "statically checked", I mean that this library generates fresh types for constraints of type t -> bool, where t is the type we are going to refine. This refinement, so, produces a subtype for such abstract type t. We can anyways inject this abstract type t as it were a type class (that is, applying a functor), and indeed it carries with itself a constraint operation (being t -> bool). The result fresh "subtype" is wrapped inside a result module, and the functor used to produce it is seen as a Dependent Pi Type. Such result module will have the following result type:

module Result : sig
  type super
  type t = private super

  exception FailedDownCast of super

  val downcast : super -> t
  val upcast   : t -> super
end;;

Where super is the previously injected type t (don't confuse with this t type, which is the fresh subtype). As you can notice easily, the sole exception in this library occurs while downcasting (honestly, when the constraint returns false). On the other hand, our local type class will have the following signature:

module TypeClass : sig
  type t

  val where : t -> bool
end;;

Where where is the refinement constraint carried together. To apply the refinement functor, we will rather use the pattern below (assuming that you have installed this library, it is required as "subtype-refinement" and provides the Subtype_refinement module):

open Subtype_refinement;;

module Result = Refine (TypeClass);;

The fresh subtype is somewhat opaque, it doesn't inherit operations from its supertype (it's really hard, anyways, to know which kind of operations preserve the constraint invariants, for example, if the constraint refines integers into naturals through fun x -> x >= 0, the subtraction operation will need further constraints for naturals such fun (x, y) -> x >= y, where (x, y) is the pair which we are going to perform subtraction). Said that, the only valid operations for this subtype are the casts, more specifically, upcasts and downcasts. So, to use super type's operations into this subtype, we need to perform casts to ensure the preservation of invariants (it would be really nice if implicits casts were provided in OCaml as they're provided in Scala).

Singletons are degenerate cases of refinements where the constraint compares against a known value. If this comparison succeeds, we certainly have a singleton value/"subtype" and we can have the cookie & the cake as well (that is, we can have nice things). To use singletons directly without doing such comparison, the type class must be somehow modified in something like that below:

module SingletonTypeClass : sig
  type t

  val value : t
end;;

Where value is our known value to compare against. A different functor for singletons is also provided (but the result module's signature is the same):

open Subtype_refinement;;

module SingletonResult = Singleton (SingletonTypeClass);;

'Cause OCaml provides first-class modules through explicit packing/unpacking, a shorter version of the refinement functor is provided as:

open Subtype_refinement;;

let result = refine constraint;;

To unpack it, we just need to say:

module Module = (val result : Subtype with type super = t);;

Where t is the type used in the constraint. The short counterpart of singleton refinements is not provided due my laziness, so maybe tomorrow I'll find my way home.

Contributors

• zapashcanon