Equivalent of haskell TypeError in OCaml

Viewed 119

In Haskell it is possible to throw type errors during the type inference to enforce typing constraints on DSLs.

ie

class ValidHarmInterval (i :: IntervalType)
instance TypeError (Text "Minor seconds forbidden.")
=> ValidHarmInterval (Interval Min Second)
instance TypeError (Text "Major sevenths forbidden.")
=> ValidHarmInterval (Interval Maj Seventh)
instance {-# OVERLAPPABLE #-} ValidHarmInterval i

Is something similar to this possible in OCaml?

1 Answers

I do not know of an equivalent to TypeError in OCaml, and a quick search didn't turn up anything obvious. But I can think of two ways of achieving the effect you're seeking: enforcing type constraints on DSLs.

Typed final (tagless-final) style EDSLs

You may want to check out the "typed final" style of embedding DSLs descibred by Oleg. It seems to have precisely the properties you want:

The typed final approach is particularly attractive if the DSL to embed is also typed. We can then represent in the host language not only terms but also the type system (type derivations) of the DSL. Only well-typed DSL terms are embeddable.

The tutorial Modular, composable, typed optimizations in the tagless-final style gives step-by-step instruction on writing EDSLs in this style with OCaml.

Polymorphic Type Variants

OCaml offers another, more light weight (but perhaps less well behaved?) way to impose type constraints on subtyping relations of this sort: polymorphic variants.

We can define a type for intervals using polymorphic variants thus:

type 'a interval =
  [< `Unison
  | `Second
  | `Third
  | `Fourth
  | `Fifth
  | `Sixth
  | `Seventh
  | `Octave
  ] as 'a

where < indicates that any subset of the variants can construct a value of type 'a interval (ignore the type variable for the time being).

Thus, we can write a standard function that takes an _ interval to a string, and it will type check as _ interval -> string, as expected:

let interval_to_string : _ interval -> string = function
  | `Unison  -> "Unison"
  | `Second  -> "Second"
  | `Third   -> "Third"
  | `Fourth  -> "Fourth"
  | `Fifth   -> "Fifth"
  | `Sixth   -> "Sixth"
  | `Seventh -> "Seventh"
  | `Octave  -> "Octave"

But we can also define a function that takes only some values of type _ interval:

let even_interval_to_int : _ interval -> int = function
  | `Second -> 2
  | `Fourth -> 4
  | `Sixth  -> 6
  | `Octave -> 8

Like interval_to_string, even_interval_to_int is also a function of values of type _ interval, but type checking will fail if you apply it to an unsupported interval:

let invalid_int_of_even_interval = even_interval_to_int `Third
(* Error: This expression has type [> `Third ]
 *        but an expression was expected of type
 *          [< `Fourth | `Octave | `Second | `Sixth ]
 *        The second variant type does not allow tag(s) `Third *)

This is because [< Fourth |Octave | Second |Sixth ] is a subtype of _ interval.

Turning to your example (and please excuse my ignorance of music theory), we can encode our minor and major harmonic intervals as intersecting, but non-identical subsets of _ interval:

type major_harmonic_interval =
  [ `Unison
  | `Second
  | `Third
  | `Fourth
  | `Fifth
  | `Sixth
  (* No Seventh *)
  | `Octave
  ]

type minor_harmonic_interval =
  [ `Unison
  (* No Second*)
  | `Third
  | `Fourth
  | `Fifth
  | `Sixth
  | `Seventh
  | `Octave
  ]

Then constrain our type harmonic_interval, so that the Major and Minor constructors can only construct values with variants of the appropriate sort:

type harmonic_interval =
  | Major of major_harmonic_interval
  | Minor of minor_harmonic_interval

This will let us construct the harmonic intervals we want:

let major_second = Major `Second

but compel the type system to forbid any harmonic intervals we don't

let minor_second = Minor `Second
(* Error: This expression has type [> `Second ]
 *        but an expression was expected of type minor_harmonic_interval
 *        The second variant type does not allow tag(s) `Second *)

Meanwhile, we can still make use of the functions we've written that operate on values of type _ interval:

let harmonic_interval_to_string : harmonic_interval -> string = function
  | Major interval -> "Major " ^ interval_to_string interval
  | Minor interval -> "Minor " ^ interval_to_string interval
Related