函数不只是types：它们是types。 和种类。 和sorting。 帮助把头脑重新凝聚起来

我正在按照惯例“ 睡觉前阅读LYAH的一章”，感觉就像我的大脑随着每个代码样本的扩展一样。 在这一点上，我确信我理解了Haskell的核心优势，现在只需要了解标准库和types类，就可以开始编写真正的软件。

所以我正在阅读关于应用函数的章节，突然之间，书中宣称函数不仅仅是types， 而是types，并且可以被视为types类（例如，通过使它们成为types类的实例）。 （ – >）是一个types构造器像任何其他。

我的思绪再次被吹起，我立即跳下床，启动计算机，去了GHCi，发现了以下情况：

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

• 这到底是什么意思？
• 如果（ – >）是一个types构造函数，那么值构造函数是什么？ 我可以猜测，但不知道如何定义传统data (->) ... = ... | ... | ... data (->) ... = ... | ... | ... data (->) ... = ... | ... | ...格式。 用任何其他types的构造函数都可以做到这一点很简单： data Either ab = Left a | Right b data Either ab = Left a | Right b 。 我怀疑我无法用这种forms来expression它与极端奇怪的types签名有关。
• 我刚刚发现了什么？ 更高的亲属types具有类似签名，如* -> * -> * 。 来想一想…（ – >）也出现在实物签名！ 这是否意味着它不仅是一个types构造函数，而且是一种构造函数？ 这是否与types签名中的问号相关？

我已经阅读过某处（希望我可以再次find它，Google失败了），关于能够从值，types的值，types的types，types的类别到类别的其他types，任意地扩展types系统，到其他东西的东西，等等永远。 这是否反映在（ – >）的亲笔签名中？ 因为我也遇到了Lambda多维数据集的概念和构造的微积分，而没有花时间来真正调查它们，如果我没有记错的话，可以定义带有types和返回types的函数，取值和返回值，获取types和返回值，并获取返回types的值。

如果我不得不猜测一个函数的types签名，该函数需要一个值并返回一个types，我可能会这样表示：

 a -> ? 

或者可能

 a -> * 

尽pipe我没有看到为什么第二个例子不容易被解释为一个从atypes的值到types*值的函数的根本不可变的原因，其中*只是string或类似的types的同义词。

第一个例子更好地expression了一个函数，它的types在我脑海中超越了types签名：“一个函数，它接受一个types为a的值，并返回一个不能被expression为types的东西”。

Answer 1

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

（ – >）

(->)是* -> * -> * ，如果我们不考虑盒子GHC插入。 但是没有循环， (->)中的(->)是友善的箭头，而不是function箭头。 事实上，为了区分它们，可以将类箭头写成(=>) ，然后(->)是* => * => * 。

我们可以把(->)看作是一个types构造函数，或者也许是一个types运算符。 同样， (=>)可以被看作是一种操作符 ，正如你在你的问题中提出的那样，我们需要去一个“关卡”。 我们稍后在“ 超越种类 ”一节中回到这一点，但首先：

情况如何看起来依赖型语言

你问如何types签名会寻找一个函数，它接受一个值并返回一个types。 这在Haskell中是不可能的：函数不能返回types！ 您可以使用typestypes和types族来模拟这种行为，但是让我们将语言更改为依赖types的语言Agda 。 这是一种与Haskell具有相似语法的语言，在这种语言中，types与值的交错是第二性质的。

为了有一些工作，我们定义一个数据types的自然数，为了方便一元表示，如在Peano算术 。 数据types以GADT风格编写：

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

在Haskell中，Set相当于所有（小）types的“types”，比如自然数。 这告诉我们， Nat的types是Set ，而在Haskell中，Nat不会有types，它会有一种types，即* 。 在阿格达没有种类，但一切都有一个types。

我们现在可以编写一个函数，它接受一个值并返回一个types。 下面是一个函数，它取自然数n和一个types，并且迭代List构造函数n应用于这个types。 （在Agda中， [a]通常被写成List a ）

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

一些例子：

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

我们现在可以制作一个listsOfLists的map函数。 我们需要取一个自然数，即列表构造函数的迭代次数。 基本情况是当数字是Zero ，然后listOfList只是身份，我们应用该function。 另一个是空列表，返回空列表。 步骤案例涉及到：我们将mapN应用到列表的头部，但是这种方法只有一层嵌套， mapN到列表的其余部分。

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

在mapN的types中， Nat参数被命名为n ，所以types的其余部分可以依赖于它。 所以这是一个依赖于值的types的例子。

_{作为一个方面说明，这里还有两个其他的命名variables，即typesSet的第一个参数a和b 。 typesvariables在Haskell中被隐含地普遍量化，但是在这里我们需要把它们拼出来，并指定它们的types，即Set 。 括号是在那里使它们在定义中是不可见的，因为它们总是可以从其他论点推断出来。}

设置是抽象的

你问(->)的构造函数是什么。 有一件事要指出的是Set （和Haskell中的* ）是抽象的：你不能在它上面进行匹配。 所以这是非法的Agda：

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

再次，您可以使用types族来模拟Haskell中types构造函数的模式匹配，在Brent Yorgey的博客上给出了一个典型的例子。 我们可以定义->在Agda？ 既然我们可以从函数返回types，我们可以定义一个自己的->版本，如下所示：

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

（infix操作符写成_=>_而不是(=>) ）这个定义的内容非常less，和在Haskell中做types同义词非常相似：

 type Fun ab = a -> b 

超越种类：乌龟一路下来

正如上面所承诺的，Agda中的所有东西都有一个types，但是_=>_的types必须有一个types！ 这触及了你的观点，也就是说，可以说Set（Set）之上的一层。 在Agda中，这被称为Set1 ：

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

事实上，它们有一个完整的层次结构！ Set是haskell中“small”types的数据types。 但是，我们有Set1 ， Set2 ， Set3等等。 Set1是提到Set的types。 这个层次是为了避免矛盾，如吉拉德的悖论。

正如你的问题所注意到的， ->用于Haskell中的types和types，并且在Agda的所有级别上都使用相同的符号表示函数空间。 这必须被视为一个内置的types运算符，而构造函数是lambda抽象（或函数定义）。 types的层次结构与System F omega中的设置类似，更多的信息可以在Pierce的types和编程语言的后面的章节中find。

纯粹的系统

在Agda中，types可以依赖于值，函数可以返回types，如上所示，而且我们也有types的层次结构。 纯系统中更详细地研究了λ结石的不同系统的系统研究。 一个很好的参考是Barendregt types的Lambda Calculi，第96页介绍了PTS，以及第99页及其后的许多例子。 你也可以阅读关于lambda立方体的更多信息。

Answer 2

首先， ?? -> ? -> * ?? -> ? -> * kind是GHC特定的扩展。 这个? 和?? 只是在那里处理unboxedtypes，其行为不同于只是* （必须被装箱，据我所知）。 那么?? 可以是任何正常types或非装箱types（例如Int# ）; ? 可以是其中之一，也可以是取消装箱的元组。 这里有更多的信息： Haskell奇怪的种类：（ – >）的种类是？ – >？ – > *

我认为一个函数不能返回一个unboxedtypes，因为函数是懒惰的。 由于懒惰值是一个值或一个thunk，它必须被装箱。 盒装意味着它是一个指针，而不仅仅是一个值：它就像Integer()和Java中的int一样。

既然你可能不会在LYAH级别的代码中使用unboxedtypes，你可以想象那种->就是* -> * -> * 。

由于? 和?? 基本上只是*更一般的版本，他们与sorting或类似的东西没有任何关系。

但是，由于->只是一个types构造函数，所以实际上可以部分应用它。 例如(->) e是Functor和Monad一个实例。 弄清楚如何写这些实例是一个很好的伸展运动。

至于价值构造函数去，他们将不得不只是lambda（ \ x -> ）或函数声明。 由于函数对于语言来说非常重要，所以它们有自己的语法。