有人可以解释这个OCaml程序中使用的类型语法吗？

Question

以下类型取自此问题

(* contains an error, later fixed by the OP *)
type _ task =
| Success : 'a -> 'a task
| Fail : 'a -> 'a task
| Binding : (('a task -> unit) -> unit) -> 'a task
| AndThen : ('a -> 'b task) * 'a task -> 'b task
| OnError : ('a -> 'b task) * 'a task -> 'b task

type _ stack =
| NoStack : 'a stack
| AndThenStack : ('a -> 'b task) * 'b stack -> 'a stack
| OnErrorStack : ('a -> 'b task) * 'b stack -> 'a stack

type 'a process = 
{ root: 'a task 
; stack: 'a stack 
}

我对OCaml比较陌生,但我以前从未见过这样的:语法.例如,我已经看到使用of语法定义的多态类型

type 'a expr =
    | Base  of 'a
    | Const of bool
    | And   of 'a expr list
    | Or    of 'a expr list
    | Not   of 'a expr

在最初的问题中,对于我来说,变体是如何构造的并不明显,因为看起来每个变体都不接受参数.以此简化为例

type 'a stack =
  | Foo : int stack
  | Bar : string stack
;;
type 'a stack = Foo : int stack | Bar : string stack

尝试int stack使用Foo

Foo 5;;
Error: The constructor Foo expects 0 argument(s),
       but is applied here to 1 argument(s)

但是,没有争论

Foo;;
- : int stack = Foo

好的,但是在哪里int？如何存储此类型的数据？

在下面的OP程序中,他/她匹配"正常"类型,例如Success value -> ...或Fail value -> ....同样,如果变体构造函数不接受参数,那么如何构造此值？

let rec loop : 'a. 'a process -> unit = fun proc ->
match proc.root with
| Success value -> 
    let rec step = function
    | NoStack -> ()
    | AndThenStack (callback, rest) -> loop {proc with root = callback value; stack = rest }
    | OnErrorStack (_callback, rest) -> step rest  <-- ERROR HERE
    in
    step proc.stack
| Fail value -> 
    let rec step = function
    | NoStack -> ()
    | AndThenStack (_callback, rest) -> step rest
    | OnErrorStack (callback, rest) -> loop {proc with root = callback value; stack = rest }
    in
    step proc.stack
| Binding callback -> callback (fun task -> loop {proc with root = task} )
| AndThen (callback, task) -> loop {root = task; stack = AndThenStack (callback, proc.stack)}
| OnError (callback, task) -> loop {root = task; stack = OnErrorStack (callback, proc.stack)}

有人能帮助我填补我的知识空白吗？

Answer 1

这些类型是广义代数数据类型.也称为GADT.GADT可以改进构造函数和类型之间的关系.

在您的示例中,GADT用作引入存在量化类型的方法:删除不相关的构造函数,可以编写

type 'a task =
| Done of 'a
| AndThen : ('a -> 'b task) * 'a task -> 'b task

这里AndThen是一个带有两个参数的构造函数:一个类型的回调 'a -> 'b task和一个'a task返回类型的任务'b task.此定义的一个显着特征是类型变量'a仅出现在构造函数的参数内.一个自然的问题是,如果我有一个值AndThen(f,t): 'a task,那是什么类型的f？

得到的答复是,该类型f是部分未知的,我只知道有一种类型ty,使得两个f: ty -> 'a task和t: ty.但是在这一点上,除了存在之外的所有信息ty都已丢失.因此,该类型ty称为存在量化类型.

但在这里,这些小信息仍然足以有意义地操纵这样的价值.我可以定义一个功能步骤

let rec step: type a. a task -> a task = function
| Done _ as x -> x
| AndThen(f,Done x) -> f x
| AndThen(f, t) -> AndThen(f, step t)

如果可能的话,尝试f在构造函数中应用函数AndThen,使用信息而不是构造函数AndThen总是存储兼容的回调和任务对.

例如

let x: int task = Done 0
let f: int -> float task =  fun x -> Done (float_of_int (x + 1))
let y: float task = AndThen(f,x)
;; step y = Done 1.