无法解决与 gadt 类型不匹配的问题

Question

我对 x 与 gadt 有以下类型定义。

type x = X : 'a option -> x

我正在尝试编写一个函数来获取带有标签 X 的选项的值

我首先尝试了以下方法

let get = fun (X a)->a

并获得以下错误消息

Error: This expression has type $X_'a option but an expression was expected of type 'a The type constructor $X_'a would escape its scope

其次我尝试了这个

let get : type a.x-> a option =  fun (X a)->a

以及以下

Error: This expression has type $X_'a option but an expression was expected of type a option Type $X_'a is not compatible with type a

我认为由于类型 x 内的选项的类型 'a 没有出现在类型注释中，因此无法显式地写出 'a 在类型注释中的实际含义。我需要帮助！！

Answer 1

你说得完全正确。您无法访问该类型。这是一种存在类型，这意味着它无法恢复。从运行时值重建此类类型没有什么神奇的技巧，因为这需要编译器在编译时了解表达式的运行时值。

也许您打算将类型

'a

作为

x

类型的一部分？

type 'a x = X : 'a option -> 'a x

不再需要 GADT 语法，可以更简洁地编写为

type 'a x = X of 'a option