Полиморфный вариант ограничения в определении варианта - PullRequest
0 голосов
/ 10 ноября 2018

Предположим, что я хочу смоделировать простой тип выражения в OCaml:

type expr = 
| `Int of int
| `Str of string
| `IntAdd of expr * expr
| `StrAdd of expr * expr

Можно ли ограничить expr в expr * expr конкретными конструкторами самого expr (т. Е. Я бы хотел, чтобы IntExpr разрешал только Int)? Я могу имитировать это с рисунком соответствие, но оно становится громоздким после расширения expr. Можно как нибудь использовать систему типов OCaml для достижения этой цели?

Я попытался использовать верхние границы полиморфного типа следующим образом:

type expr = 
| `Int of int
| `Str of string
| `IntAdd of [< `Int] * [< `Int]
| `StrAdd of [< `Str] * [< `Str]

но компилятор не принимает это (с сообщением In case IntAdd of [< Int ] * ([< Int ] as 'a) the variable 'a is unbound). Есть ли какая-нибудь хитрость, чтобы заставить это работать?

1 Ответ

0 голосов
/ 10 ноября 2018

Данный пример достаточно прост для полиморфных вариантов:

type int_expr = [`Int of int | `Add of int_expr * int_expr]
type string_expr = [`String of string | `Concat of string_expr * string_expr]
type expr = [int_expr | string_expr]

Если вам нужны более интересные функции, такие как полиморфные структуры данных, необходимы GADT:

type _ expr =
  | Int : int -> int expr
  | Add : int expr * int expr -> int expr
  | String : string -> string expr
  | Concat : string expr * string expr -> string expr
  | Pair : 'a expr * 'b expr -> ('a * 'b) expr
  | Fst : ('a * 'b) expr -> 'a expr
  | Snd : ('a * 'b) expr -> 'b expr

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

...