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

您将收到信息性错误消息

No type declaration for Main.myId

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

myId : _
myId = \x => x

When checking right hand side of myId with expected type iType

Type mismatch between _ -> _ (Type of \x => x) and iType (Expected type)

好的，让我们试试函数类型：

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

When checking right hand side of myId with expected type ty -> hole

Type mismatch between ty (Type of x) and hole (Expected type)

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

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

因此我们必须指定 myId 的完整类型，但类型变量 a 的宇宙级别除外。

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

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

Type of anonymous identity function in Idris