README

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 typet -> bool, wheret is the type we are going to refine. This refinement, so, produces a subtype for such abstract typet. We can anyways inject this abstract typet as it were a type class (that is, applying a functor), and indeed it carries with itself a constraint operation (beingt -> 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 -> superend;;

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

module TypeClass : sig  type t  val where : t -> boolend;;

Wherewhere 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 theSubtype_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 throughfun x -> x >= 0, the subtraction operation will need further constraints for naturals suchfun (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 : tend;;

Wherevalue 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);;

Wheret 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

1. dune>= "1.11"
2. ocaml>= "3.12"

1. ounitwith-test

None

None