函数不仅具有类型:它们是类型.和种类.并排序.帮助把一个强大的思想重新组合在一起

Question

我正常做着"读睡前LYAH的一章"的例行公事,感觉我的大脑正随着每个代码样本而扩展.在这一点上,我确信我理解了Haskell的核心功能,现在只需要理解标准库和类型类,这样我就可以开始编写真正的软件了.

所以我正在阅读有关应用函子的章节,突然之间,本书声称函数不仅仅有类型,它们是类型,并且可以这样处理(例如,通过使它们成为类型类的实例).( - >)是一个类似于任何其他类型的构造函数.

我的思绪又被吹了,我立刻跳下床,启动计算机,去了GHCi并发现了以下内容:

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

• 究竟是什么意思？
• 如果( - >)是一个类型构造函数,那么值构造函数是什么？我可以猜一猜,但不知道如何用传统data (->) ... = ... | ... | ...格式定义它.使用任何其他类型的构造函数都可以轻松完成:data Either a b = Left a | Right b.我怀疑我无法以这种形式表达它与极端奇怪的类型签名有关.
• 我偶然发现了什么？较高的kinded类型有类似的签名* -> * -> *.想一想......( - >)也会出现在亲切的签名中!这是否意味着它不仅是一个类型构造函数,而且还是一种类型的构造函数？这与类型签名中的问号有关吗？

我已经阅读了某个地方(希望我能再次找到它,谷歌让我失望)关于能够通过从值,值类型,到各种类型,各种类型,到其他各种类型,任意扩展类型系统,到别的东西,等等永远.这是否反映在( - >)的签名中？因为我也遇到了Lambda多维数据集的概念和构造的微积分而没有花时间去真正研究它们,如果我没记错,可以定义采用类型和返回类型的函数,取值和返回值,获取类型和返回值,并获取返回类型的值.

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

a -> ?

或者可能

a -> *

虽然我没有看到根本不可变的原因,为什么第二个例子不能轻易地被解释为从类型a的值到类型*的值的函数,其中*只是字符串或类似的类型同义词.

第一个例子更好地表达了一个函数,它的类型在我的脑海中超越了一个类型签名:"一个函数,它接受一个类型为a的值并返回一些不能表示为类型的东西."

Answer 1

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

种( - >)

种的(->)就是* -> * -> *,如果我们忽略boxity GHC插入.但是没有循环,->s (->)是那种善良的箭头,而不是功能箭头.事实上,为了区分它们那种箭头可以写成(=>),然后那种(->)是* => * => *.

我们可以将其(->)视为类型构造函数,或者更确切地说是类型运算符.同样,(=>)可以看作是一种善意的操作员,正如你在你的问题中所建议的那样,我们需要进行一次"升级".我们稍后将在Beyond Kinds一节中回到此处,但首先:

情况如何以依赖类型的语言显示

您询问类型签名如何查找带有值并返回类型的函数.这在Haskell中是不可能的:函数不能返回类型!您可以使用类型类和类型族来模拟此行为,但让我们将插图更改为依赖类型语言 Agda.这是一种语法与Haskell类似的语言,其中将值与值一起变为第二本质.

为了使用某些东西,我们定义了自然数的数据类型,以便在Peano算术中实现一元表示 .数据类型以GADT样式编写 :

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

Set相当于Haskell中的*,是所有(小)类型的"类型",例如自然数.这告诉我们的类型Nat是 Set,而在Haskell中,Nat不会有类型,它会有一种类型,即*.在阿格达没有种类,但一切都有类型.

我们现在可以编写一个获取值并返回类型的函数.下面是一个采用自然数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的博客上给出了一个实例 .我们可以->在Agda中定义吗？由于我们可以从函数返回类型,因此我们可以定义自己的版本,->如下所示:

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

(编写中缀运算符_=>_而不是(=>))此定义的内容非常少,与在Haskell中执行类型同义词非常相似:

type Fun a b = a -> b

除了种类:海龟一路下来

如上面所承诺的,一切都在阿格达有一个类型,但随后的类型的_=>_ 必须有型!这触及你关于排序的观点,可以说是Set之上的一层(种类).在Agda这称为Set1:

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

事实上,它们有一个完整的层次结构!Set是"小"类型的类型:haskell中的数据类型.但是,我们有Set1, Set2,Set3,等.Set1是提到的类型 Set.这种层次结构是为了避免像Girard悖论这样的不一致.

正如您在问题中所注意到的,->用于Haskell中的类型和种类,并且Agda中所有级别的函数空间都使用相同的表示法.这必须被视为内置类型运算符,构造函数是lambda抽象(或函数定义).这种类型的层次结构类似于System F omega中的设置 ,更多信息可以在Pierce的类型和编程语言的后续章节中找到 .

纯型系统

在Agda中,类型可以依赖于值,函数可以返回类型,如上所示,我们还有类型的层次结构.在Pure Type Systems中更详细地研究了λ结石的不同系统的系统研究.一个很好的参考是 Lambda Calculi和 Barendregt的类型,其中PTS在第96页介绍,许多例子在第99页及以后介绍.您还可以在那里阅读有关lambda多维数据集的更多信息.

Answer 2

首先,这种?? -> ? -> *类型是GHC特定的扩展.该?和??只是有对付未装箱的类型,它们的行为不同于只*(其中有被装箱,因为据我所知).因此??可以是任何普通类型或未装箱类型(例如Int#); ?可以是那些或未装箱的元组.这里有更多的信息:Haskell Weird Kinds:种类( - >)是?? - >？ - >*

我认为函数不能返回未装箱的类型,因为函数是惰性的.由于惰性值是值或thunk,因此必须将其装箱.盒装只是意味着它是一个指针,而不仅仅是一个值:它就像在Java中的Integer()vs.int

由于你可能不会在LYAH级代码中使用未装箱的类型,你可以想象那种->只是* -> * -> *.

由于?和??基本上只是更一般的版本*,它们与排序或类似的东西没有任何关系.

但是,因为->它只是一个类型构造函数,所以你实际上可以部分地应用它; 例如,(->) e是一个实例Functor和Monad.弄清楚如何编写这些实例是一个很好的思维伸展运动.

就值构造函数而言,它们必须只是lambdas(\ x ->)或函数声明.由于函数是语言的基础,因此它们有自己的语法.