Как мне интерпретировать эту ошибку GADT в OCaml? - PullRequest
Новая
       43

Как мне интерпретировать эту ошибку GADT в OCaml?

0 голосов
/ 26 сентября 2019

Извините за вопрос «что мне здесь не хватает», но я просто кое-что здесь упускаю.

Я пытался понять, как работают GADT в OCaml, я определяю следующее (вutop): 

 type value =
| Bool : bool -> value
| Int : int -> value
;;

type _ value =
| Bool : bool -> bool value
| Int : int -> int value
;;

type _ expr =
| Value : 'a value -> 'a expr
| If : bool expr * 'a expr * 'a expr -> 'a expr
| Lt : 'a expr * 'a expr -> bool expr
| Eq : 'a expr * 'a expr -> bool expr
| Gt : 'a expr * 'a expr -> bool expr
;;

Я определил функцию eval: 

let rec eval : type a. a expr -> a = function
| Value (Int i) -> i
| Value (Bool b) -> b
| Lt (a, b) -> (eval a) < (eval b)
| Gt (a, b) -> (eval a) > (eval b)
| Eq (a, b) -> (eval a) = (eval b)
| If (c, a, b) -> if eval c then (eval a) else (eval b)
;;

, но получил ошибку: 

Line 4, characters 15-23:
Error: This expression has type $Lt_'a but an expression was expected of type
         int

Что именноэто значит?

Просто для дальнейшего тестирования я изменил выражение GADT следующим образом: 

type _ expr =
| Value : 'a value -> 'a expr
| If : bool expr * 'a expr * 'a expr -> 'a expr
| Lt : int expr * int expr -> bool expr
| Eq : 'a expr * 'a expr -> bool expr
| Gt : int expr * int expr -> bool expr
;;

, а затем вижу 

Line 6, characters 15-23:
Error: This expression has type $Eq_'a but an expression was expected of type
         int

Когда янаконец, измените его на 

type _ expr =
| Value : 'a value -> 'a expr
| If : bool expr * 'a expr * 'a expr -> 'a expr
| Lt : int expr * int expr -> bool expr
| Eq : int expr * int expr -> bool expr
| Gt : int expr * int expr -> bool expr
;;

, он работает нормально.

Обновление (более контекстно):

  • Версия Ocaml: 4.08.1
  • Библиотеки, открытые во время этого сеанса: Base

Обновление (решение):

  • оказалось(как упомянуто в первой строке выбранного ответа), потому что я уже раньше, в течение utop запуска open Base ;;
  • В новом сеансе я могу ввести типы, упомянутые изначально, и eval - этодоволен этим.

1 Ответ

2 голосов
/ 26 сентября 2019

Непосредственной причиной ошибки является то, что вы используете библиотеку (может быть, Base или Core?), Которая скрывает полиморфные операторы сравнения (<, <=, =, >=, >)и замените их целочисленными операторами сравнения.

Что касается сообщения об ошибке, когда вы сопоставляете шаблон с конструктором GADT с экзистенциальными типами, 

| Lt (a, b) -> (eval a) < (eval b)

, средство проверки типов вводит новые типы для представления экзистенциальных типов.Здесь в (оригинальном) определении Lt, 

| Lt : 'a expr * 'a expr -> bool expr

есть одна экзистенциально квантифицированная переменная типа: 'a.

При сопоставлении с образцом на Lt нам нужнозаменить эту переменную типа новым типом.Более того, в сообщении об ошибке весьма полезно попытаться выбрать значимое имя для этого типа.Для этого средство проверки типов создает поэлементно новое имя типа как $ + Lt + 'a:

  • $: чтобы отметить экзистенциальный тип
  • Lt: указать, что он был введен конструктором Lt
  • a: запомнить, что переменная экзистенциального типа была названа 'a в определении конструктора

Другими словами, в приведенном выше шаблонном сопоставлении мы имеем что-то похожее на 

| Lt ( (a: $Lt_'a eval), (b: $Lt_'a eval)) -> (eval a) < (eval b)

И при наборе: 

  (eval a) < (eval b)

проверка типов сравнивает тип <: int -> int с типом eval a: $Lt_'a и выводит исходное сообщение об ошибке: 

 Line 4, characters 15-23:
 Error: This expression has type $Lt_'a but an expression was expected of type
     int
...