Idris 中匿名身份函数的类型

Question

在 Idris 检查类型 if id 时，我们得到了预期的结果：

> :type id
id : a -> a

但是，检查 lambda 表达式版本会引发一个棘手的错误：

> :type \x => x
(input):Incomplete term \x => x

这是为什么？如果我使用一个函数将 x 的上下文强制转换为一个类型，我会得到我所期望的：

> :type \x => x+1
\x => x + 1 : Integer -> Integer

Answer 1

类型推断通常对于依赖类型是不可判定的，参见例如the answers to this CS.SE question。在 Idris 中，您可以不为某些术语指定类型，但不是全部。

如果您将定义添加到 .idr 文件并尝试加载它，例如

myId = \x => x

您将收到信息性错误消息

Main.myId 没有类型声明

那么让我们看看在给它一个类型方面我们需要走多远（下面是 Idris 0.10.2）：

myId : _
myId = \x => x

当检查 myId 的右侧与预期类型时 iType

之间的类型不匹配 _ -> _（\x => x 的类型） 和 iType（预期类型）

好的，我们试试一个函数类型：

myId : _ -> _
myId = \x => x

当检查 myId 的右侧与预期类型时 ty -> hole

之间的类型不匹配 ty（x 的类型）和 hole（预期类型）

我会省去你后续的步骤，但基本上 myId : {a : Type} -> a -> _ 和 myId : {a : Type} -> _ -> a 都以同样的方式失败，留给我们

myId : {a : _} -> a -> a
myId = \x => x

所以我们必须指定myId 的完整类型，除了类型变量a 的全域级别。

myId的类型签名最终版本也可以写成

myId : a -> a
myId = \x => x