Idris中匿名身份函数的类型

Question

在Idris中检查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

- Athan Clark

---

这不仅仅是因为 Idris 没有函数类型推断吗？ - Cactus

Answer 1

通常情况下，依赖类型的类型推断是不可判定的，例如请参考这篇CS.SE问题的答案。在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

- Cactus