haskell - OCaml 中的 haskell TypeError 的等效项

Question

在 Haskell 中，可以在类型推断期间抛出类型错误，以强制对 DSL 进行类型约束。

即

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

OCaml 中可能有类似的事情吗？

Answer 1

我不知道 TypeError 的等价物在 OCaml 中，快速搜索并没有发现任何明显的东西。但我可以想到两种方法来实现您正在寻求的效果:对 DSL 实现类型约束。

类型化最终(无标签最终)样式 EDSL

您可能想查看"typed final" style Oleg 描述的嵌入 DSL 的方法。它似乎恰好具有您想要的属性:

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.

教程 Modular, composable, typed optimizations in the tagless-final style提供了使用 OCaml 以这种方式编写 EDSL 的分步说明。

多态类型变体

OCaml 提供了另一种更轻量级(但可能表现不佳？)的方法来对此类子类型关系施加类型约束:polymorphic variants 。

我们可以使用多态变体来定义区间类型:

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

哪里<表示变体的任何子集都可以构造 'a interval 类型的值(暂时忽略类型变量)。

因此，我们可以编写一个标准函数，它接受 _ interval到 string ，它将检查类型为 _ interval -> string ，如预期:

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

但是我们也可以定义一个函数，它只接受 _ interval 类型的一些值:

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

喜欢interval_to_string , even_interval_to_int也是 _ 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 *)

这是因为[< <code>Fourth |</code>Octave | <code>Second |</code>Sixth ]是 _ interval 的子类型.

转向您的示例(请原谅我对音乐理论的无知)，我们可以将小调和大调和声间隔编码为 _ 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
  ]

然后约束我们的 type harmonic_interval ，这样 Major和Minor构造函数只能构造具有适当排序变体的值:

type harmonic_interval =
  | Major of major_harmonic_interval
  | Minor of minor_harmonic_interval

这将使我们构建我们想要的谐波音程:

let major_second = Major `Second

但强制​​类型系统禁止我们不禁止的任何调和音程

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 *)

同时，我们仍然可以使用我们编写的对 _ interval 类型的值进行操作的函数。 :

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