OCaml - GADT映射

Question

我很难理解在OCaml中使用GADT的一些方面。让我试着告诉你我的榜样和我的理解..。

我正在尝试实现西蒙·佩顿-琼斯关于组合合同(https://www.microsoft.com/en-us/research/wp-content/uploads/2000/09/pj-eber.pdf)的经典论文。

我希望能够操作一个可观察的函数，定义为从日期到某种类型的值(实际上是一个float或bool)。因此，我使用GADT定义了一个函数类型和一个观察类型。

type _ value = 
| Float : float -> float value
| Bool : bool -> bool value

type _ obs = Observation : (date -> 'v value) -> (date -> 'v) obs  

我想我要定义的是

• value要么是float，要么是bool (使用Float或Bool构造函数构建)和
• obs是从date到value类型之一的函数，所以不是date -> float就是date -> bool

现在我定义了一个表达式，它使我能够组合可观察到的

type _ expr =
| Konst : 'v value -> 'v expr
| Obs : 'v obs -> 'v expr
| Lift : ('v1 -> 'v2) * 'v1 expr -> 'v2 expr  

到目前一切尚好。表达式要么是常量，要么是观察(即date->float或date->bool)，要么是应用于表达式的函数。

现在我想要评估一个可以观察到的。在现实中，一个可观测的过程是建立在一个随机过程上的，所以我有一个Distribution模块(注意，在最初的论文中，我们的思想是将一个可观测的概念从它的实现中分离出来--这样我们就可以通过格子、蒙特卡罗或者我们想要的任何方法来实现)。

module type Distribution_intf =
  sig
    type element = Element of float * float
    type t = element list

    val lift : t -> f:(float -> float) -> t
    val expected : t -> float
  end

因此，给出一个compose函数，让它组成f= -> f (g )

我应该能够考虑Observable的评估。下面是一个映射函数(为了清楚起见，我已经取出了布尔情况)

type rv = date -> Distribution.t

let rec observable_to_rv : type o. o Observable.expr -> rv = 
  let open Distribution in
  function
  | Konst (Float f) -> fun (_:date) -> [Element(1.0, f)]
  | Lift (f,obs) -> compose (lift ~f) (observable_to_rv o) (*ERROR HERE *)

现在事情变得有问题了。当我尝试编译时，我得到以下错误消息(在Lift模式匹配上)：

Error: This expression has type v1#0 -> o
   but an expression was expected of type float -> float
   Type v1#0 is not compatible with type float

我不明白为什么：Lift表达式有类型

Lift: ('v1 -> 'v2) * 'v1 expr -> 'v2 expr 

因此，在给定一个Lift(f,o)时，编译器不应该限制它，因为observable_to_rv有date -> float类型，那么'v2必须是float，因为lift具有float -> float类型，所以'v1必须是浮点，所以应该在(float -> float, float expr)类型的任何元组上定义Lift。

我错过了什么？

史蒂夫

Answer 1

您忽略了以下事实: Lift中的类型变量'v1是存在量化的：

Lift: ('v1 -> 'v2) * 'v1 expr -> 'v2 expr

手段

Lift: ∃'v1. ('v1 -> 'v2) * 'v1 expr -> 'v2 expr

换句话说，给定一个值Lift(f,x): 'b expr，类型检查器所拥有的唯一信息就是存在一个类型'a，例如f:'a -> 'b和x:'a expr，仅此而已。

特别是回到您的错误消息(编译器的最新版本(≥4.03))：

类型$Lift_'v1与浮动类型不兼容

不可能将电梯构造函数引入的存在类型统一到浮点类型或任何具体类型，因为类型系统中没有隐藏在'v1后面的实际具体类型的信息。

编辑:问题的本质是，您正在尝试从表达式链'a expr构建一个浮动随机变量，该变量可以包含任何类型的中间表达式，只需要使用'a表达式生成。由于您既不能在类型系统中表示条件only float sub-expression，也不能用当前的设计构造非浮点随机变量，这将带来麻烦。

解决方案要么删除构建非浮点表达式的能力，要么添加处理非浮动随机变量.Taking的能力，第二个选项如下所示

module Distribution:
  sig
    type 'a element = {probability:float; value: 'a}
    type 'a t = 'a element list

    val lift : 'a t -> f:('a -> 'b) -> 'b t
    val expected : float t -> float
  end = struct … end

然后，键入为observable_to_rv的随机变量'a expr -> 'a rv将进行类型检查。