代码之家 › 专栏 › 技术社区 › Mulan

有人能解释这个ocaml程序中使用的类型语法吗?

gadt variant ocaml polymorphism

3

Mulan · 技术社区 · 8 年前

(* 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 ?如何在此类型中存储数据?

在下面的操作程序中,他/她正在匹配“正常”类型,例如 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)}

有人能帮我填补知识空白吗?

2 回复 | 直到 8 年前

1

6

octachron 8 年前

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

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

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

在这里, AndThen 是采用两个参数的构造函数:类型为的回调 'a -> 'b task 和A 'a task 并返回类型为的任务 'b task . 这个定义的一个显著特点是类型变量 'a 只出现在构造函数的参数中。一个自然的问题是我是否有价值 AndThen(f,t): 'a task ,什么类型的 f ?

答案是 f 部分未知,我只知道有一种类型 ty 使两者都 f: ty -> 'a task 和 t: 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 在构造函数中 然后呢 如果可能的话, 使用信息而不是构造函数 然后呢 始终存储一对兼容的回调和任务。

例如

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.

2

4

vonaka 8 年前

我认为评论和@octachron的回答提供了足够的细节,但我想展示我最喜欢的两个小工具功能的例子。

首先,您可以编写函数,它将返回(类型)不同的类型!

type _ expression = Int : int -> int expression
                  | Bool : bool -> bool expression

let evaluate : type t. t expression -> t = function
  | Int i -> i
  | Bool b -> b

type t. t expression -> t 意味着函数接受某种类型的表达式并返回该类型的值。

# evaluate (Int 42);;
- : int = 42
# evaluate (Bool true);;
- : bool = true

显然,用简单的代数类型无法实现这一点。

第二点是,有了gadts编译器,您就有了足够的关于传递给函数的值的信息,因此您可以在模式匹配中“丢弃”一些毫无意义的分支:

let negation : bool expression -> bool = function
  | Bool b -> not b

因为 bool expression -> bool OCAML知道 negation 仅适用于 bool 所以没有关于 Int i Int一世 您将看到一个类型错误:

# negation (Int 42);;
Characters 9-17:
  negation (Int 42);;
       ^^^^^^^^

错误:此表达式的类型为int表达式但表达式应为bool表达式类型 int类型与bool类型不兼容

对于简单的代数类型,此示例将如下所示:

let negation = function
  | Bool b -> not b
  | Int i -> failwith "not a bool"

你不仅有一根无用的树枝,而且如果你不小心路过 Int 42 它只能在运行时失败。