时间戳

首页 > 解决方案 > 如何在 OCaml 中解释此 GADT 错误？

ocaml - 如何在 OCaml 中解释此 GADT 错误？

问题描述

抱歉，这里有“我在这里错过了什么”的问题风格，但我只是在这里遗漏了一些东西。

我试图了解 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
;;

它工作正常。

更新（更多上下文）：

更新（解决方案）：

标签： ocamlgadt

解决方案

错误的直接原因是您使用的库（可能是 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

推荐阅读