haskell - 函数不仅有类型 : They ARE Types. 和种类。和排序。帮助重振精神

Question

我正在做我通常的“睡前阅读 LYAH 一章”的例行程序，感觉我的大脑在每个代码示例中都在膨胀。在这一点上，我确信我了解了 Haskell 的核心优势，现在只需要了解标准库和类型类，这样我就可以开始编写真正的软件了。

所以我正在阅读有关应用仿函数的章节时，突然这本书声称函数不仅具有类型，它们也是类型，并且可以这样对待(例如，通过使它们成为类型类的实例)。 (->) 是一个和其他类型构造函数一样的类型构造函数。

我的脑子又被炸了，我立刻从床上跳起来，打开电脑，去GHCi，发现了以下内容:

Prelude> :k (->)
(->) :: ?? -> ? -> *

这到底是什么意思？

如果 (->) 是类型构造函数，那么值构造函数是什么？我可以猜测，但不知道如何在传统 data (->) ... = ... | ... | ... 中定义它格式。使用任何其他类型的构造函数很容易做到这一点:data Either a b = Left a | Right b .我怀疑我无法以这种形式表达它与非常奇怪的类型签名有关。

我刚刚偶然发现了什么？更高级的类型具有类型签名，如 * -> * -> * .想想看... (->) 也出现在实物签名中!这是否意味着它不仅是类型构造函数，而且还是类构造函数？这与类型签名中的问号有关吗？

我在某处读过(希望我能再次找到它，谷歌让我失望)关于能够通过从值到值的类型、类型的种类、种类的种类、种类的其他东西来任意扩展类型系统，到别的东西到别的东西，以此类推。这是否反射(reflect)在 (->) 的类型签名中？因为我也遇到了 Lambda 多维数据集和构造演算的概念而没有花时间真正研究它们，如果我没记错的话，可以定义接受类型和返回类型、接受值和返回值的函数，取类型和返回值，取返回类型的值。

如果我不得不猜测一个接受一个值并返回一个类型的函数的类型签名，我可能会这样表达:

a -> ?

或者可能

a -> *

尽管我没有看到为什么第二个示例不能轻易解释为从 a 类型的值到 * 类型的值的函数，其中 * 只是 string 或其他类型的同义词，但我没有看到根本不变的原因。

第一个例子更好地表达了一个函数，它的类型超越了我心中的类型签名:“一个函数，它接受类型 a 的值并返回一些不能表示为类型的东西。”

Answer 1

你在你的问题中触及了很多有趣的点，所以我是
恐怕这将是一个很长的答案:)

种类 (->)

那种(->)是 * -> * -> * , 如果我们忽略 boxity GHC
插入。但是没有循环，-> s 在
种(->)是种类箭头，而不是功能箭头。的确，要
区分它们的箭头可以写成(=>) ， 进而
那种(->)是 * => * => * .

我们可以把(->)作为类型构造函数，或者更确切地说是一种类型
运算符(operator)。同样，(=>)可以看作是一个善意的运算符，并且
正如您在问题中所建议的那样，我们需要提高一个“级别”。我们
稍后在 部分返回此内容超越种类 ， 但首先:

依赖类型语言中的情况如何

你问类型签名如何寻找一个函数
值并返回一个类型。这在 Haskell 中是不可能做到的:
函数不能返回类型!您可以使用模拟此行为
类型类和类型族，但让我们来作说明
语言到依赖类型语言
Agda .这是一个
与 Haskell 语法相似的语言，其中将类型组合在一起
值(value)观是第二天性。

为了处理一些事情，我们定义了一个自然的数据类型
数字，为了方便一元表示，如
Peano Arithmetic .
数据类型写入
GADT风格:

data Nat : Set where
    Zero : Nat
    Succ : Nat -> Nat

Set 相当于 Haskell 中的 *，所有(小)类型的“类型”，
比如自然数。这告诉我们 Nat 的类型是 Set ，而在 Haskell 中，Nat 没有类型，它会有
一种，即 * .在 Agda 中没有种类，但一切都有
一种。

我们现在可以编写一个函数，它接受一个值并返回一个类型。
下面是一个取自然数 n 的函数和一个类型，
并迭代 List构造函数 n应用于此
类型。 (在 Agda 中， [a] 通常写成 List a )

listOfLists : Nat -> Set -> Set
listOfLists Zero     a = a
listOfLists (Succ n) a = List (listOfLists n a)

一些例子:

listOfLists Zero               Bool = Bool
listOfLists (Succ Zero)        Bool = List Bool
listOfLists (Succ (Succ Zero)) Bool = List (List Bool)

我们现在可以制作 map作用于 listsOfLists 的函数.
我们需要取一个自然数，即迭代次数
列表构造函数。基本情况是当数字是 Zero ，然后 listOfList只是身份，我们应用功能。
另一个是空列表，返回空列表。
步骤案例有点涉及:我们申请 mapN到头
列表中，但这少了一层嵌套，和 mapN到列表的其余部分。

mapN : {a b : Set} -> (a -> b) -> (n : Nat) ->
       listOfLists n a -> listOfLists n b
mapN f Zero     x         = f x
mapN f (Succ n) []        = []
mapN f (Succ n) (x :: xs) = mapN f n x :: mapN f (Succ n) xs

在 mapN的类型, Nat参数名为 n ，所以剩下的
类型可以取决于它。所以这是一个类型的例子
取决于一个值。

作为旁注，这里还有另外两个命名变量，
即第一个参数， a和 b , 类型 Set .类型
变量在 Haskell 中被隐式地普遍量化，但是
这里我们需要把它们拼出来，并指定它们的类型，即 Set .括号是为了使它们在
定义，因为它们总是可以从其他参数中推断出来的。

集合是抽象的

你问 (->)的构造函数是什么是。需要指出的一件事
是 Set (以及 Haskell 中的 *)是抽象的:你不能
模式匹配就可以了。所以这是非法的 Agda:

cheating : Set -> Bool
cheating Nat = True
cheating _   = False

同样，您可以在类型构造函数上模拟模式匹配
Haskell 使用类型家族，给出了一个规范的例子
Brent Yorgey's blog .
我们可以定义 ->在 Agda ？因为我们可以从
函数，我们可以定义一个自己的版本 ->如下:

_=>_ : Set -> Set -> Set
a => b = a -> b

(中缀运算符写成 _=>_ 而不是 (=>) )
定义内容很少，和做一个很相似
在 Haskell 中输入同义词:

type Fun a b = a -> b

超越种类:海龟一路向下

正如上面所 promise 的，Agda 中的一切都有一个类型，但是 _=>_的类型必须有类型!这触及你的观点
关于 sorts，可以说是 Set(种类)之上的一层。
在 Agda 中，这被称为 Set1 :

FunType : Set1
FunType = Set -> Set -> Set

事实上，他们有一个完整的层次结构!集合是类型
“小”类型:haskell 中的数据类型。但是我们有 Set1 , Set2 , Set3 ， 等等。 Set1是提到的类型的类型 Set .这种层次结构是为了避免不一致，如吉拉德的
悖论。

正如您在问题中所注意到的， ->用于类型和种类
Haskell，并且完全相同的符号用于函数空间
Agda 中的级别。这必须被视为内置类型运算符，
并且构造函数是 lambda 抽象(或函数
定义)。这种类型的层次结构类似于
System F omega ， 和更多
信息可以在后面的章节中找到
Pierce's Types and Programming Languages .

纯类型系统

在 Agda 中，类型可以依赖值，函数可以返回类型，
如上所示，我们还有一个层次结构
类型。对不同系统的 lambda 进行系统研究
在 Pure Type Systems 中更详细地研究了演算。一个好的
引用是
Lambda Calculi with Types巴伦德里格特，
其中第 96 页介绍了 PTS，以及第 99 页及以后的许多示例。
您还可以在那里阅读有关 lambda 多维数据集的更多信息。