Может кто-нибудь объяснить синтаксис типа, используемый в этой программе OCaml? - PullRequest
Новая
       57

Может кто-нибудь объяснить синтаксис типа, используемый в этой программе OCaml?

0 голосов
/ 29 мая 2018

Типы, приведенные ниже, взяты из этого вопроса 

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

Может ли кто-нибудь помочь мне заполнить пробел в моих знаниях?

Ответы [ 2 ]

0 голосов
/ 30 мая 2018

Я думаю, что комментарии и ответ @ octachron предоставляют достаточно подробностей, но я хотел бы показать два моих любимых примера мощности GADT.

Прежде всего вы можете написать функцию, которая будет возвращать (вроде) различные типы! 

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

Очевидно, что вы не можете достичь этого с помощью простых алгебраических типов.

Второй момент заключается в том, что компилятор GADT имеет достаточно информации о значении, которое вы передаете функции, поэтому вы можете "отбросить" некоторую бессмысленную ветвь в сопоставлении с образцом: 

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

Из-за bool expression -> bool OCaml знает, что negation работает только для bool, поэтому нет никаких предупреждений об отсутствии ветки Int i.И если вы попытаетесь вызвать его с помощью Int i, вы увидите ошибку типа: 

# 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 он потерпит неудачу только во время выполнения.

0 голосов
/ 30 мая 2018

Эти типы являются обобщенными алгебраическими типами данных.Также известен как ГАДЦ .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.
...