OCaml — GADT — логическое выражение

Вы должны давать разные имена конструкторам типов, потому что бывают ситуации, когда gadt действительно ведет себя как adt.

Предположим, что вы хотите определить свой тип следующим образом:

type 'canonical boolean_expression =
  | Bool : bool -> canonical boolean_expression (* here I assume that you wanted to have that case too *)
  | Var : int -> not_canonical boolean_expression
  | Not : 'canonical boolean_expression -> 'canonical boolean_expression
  | BinOpC : canonical boolean_expression * binary_operator * canonical boolean_expression -> canonical boolean_expression
  | BinOpNC : _ boolean_expression * binary_operator * _ boolean_expression -> not_canonical boolean_expression
 ;;

Теперь рассмотрим этот тип с небольшой модификацией:

type 'canonical boolean_expression =
  | Bool : bool -> canonical boolean_expression
  | Var : int -> not_canonical boolean_expression
  | Not : 'canonical boolean_expression -> 'canonical boolean_expression
  | BinOpC : canonical boolean_expression * binary_operator * canonical boolean_expression -> canonical boolean_expression
  | BinOpNC : 'a boolean_expression * binary_operator * 'a boolean_expression -> 'a boolean_expression
;;

Теперь вы можете получить бинарную операцию canonical boolean_expression, используя любой из двух последних конструкторов. Очевидно, свобода, которую вы получаете, произвольно выбирая тип результирующего значения, имеет свои последствия: вы можете создавать гаджеты с перекрывающимися «вариантами типов». При этом любая функция, принимающая любое из этих значений, должна проверять оба случая. Следовательно, имена конструкторов не могут быть идентичными, потому что типов может быть недостаточно, чтобы понять, с какими значениями мы имеем дело.

Например, функция ниже:

 let rec compute = function 
    | Bool b -> b   
    | BinOpC (a,And,b) -> compute a && compute b
    | BinOpC (a,Or,b) -> compute a || compute b
 ;;

учитывая ваше определение, должен без проблем проверять тип и заботиться о канонических выражениях. С моей модификацией компилятор справедливо будет жаловаться, что BinOpNC может также содержать выражение canonical.

Это кажется глупым примером (и это действительно так) для демонстрации этого аспекта gadt, потому что мое измененное определение логического выражения явно неверно (с точки зрения семантики), но компиляторы не заботятся о прагматическом значении типа.

По сути, gadt по-прежнему недействительны, потому что вы все еще можете столкнуться с ситуациями, когда вы должны рассчитывать на конструктор, чтобы выбрать правильный курс действий.