不是类型构造函数的类型级别函数的示例

Question

与其他类型级函数相比,Haskell中"类型构造函数"概念的独特之处是什么？

据我所知他们:

• 允许用户在编译期间向它们应用参数
• 在提供有限数量的参数后,会产生一个简单的类型(例如,不是约束)

Answer 1

短语"type constructor"有两种常见的用法.有些人将它们用于任何带箭头的类型; 但是Haskell报告以不同的方式使用它,所以我将谈论这个定义.

构造函数由声明data和newtype声明创建,并且是这些声明在类型级别引入的单个新名称.以下是类型构造函数的一些示例:

Either
Maybe
[]
Bool

哎呀,你注意到最后一个吗？没错,关于"类型构造函数"的短语并不意味着它必须能够接受参数.Bool是由数据声明引入的类型级名称 - 因此是类型构造函数.以下是一些非构造函数的类型示例:

Maybe Int
a -> b
Either ()
m -- even if we know, say, Monad m holds

哎呀,你注意到了最后两个吗？这是正确的,朝着另一个方向发展,没有什么可以采取进一步的类型参数,使你成为一个类型构造函数.每个Either和()都是构造函数,但是Eitherto 的应用()不是,因为它不是由声明data或newtype声明创建的单个类型级名称.类似地,m是一个类型变量,而不是构造函数 - 它的含义不是由任何data或newtype声明修复的.

除了构造函数和变量之外,标准Haskell中还有另一种类型级别的名称:类型别名.类型别名和构造函数之间有两个主要区别:

1. 构造函数是单射的,别名可能不是.如果FooC a b c和FooC a' b' c'是同一类型,FooC是一个构造函数,然后a和a'属于同一类型,b并且b'是同一类型,c并且c'是同一类型.对比

   type FooA a = String
   

   其中FooA ()和FooA Bool是相同的类型,即使()并且Bool不是同一类型.

2. 构造函数可能部分应用,类型别名不能.例如,如果你写

   type BarA a = Maybe a
   

   然后StateT Int BarA ()是无效的 - BarA必须立即给它的类型参数 - 即使StateT Int Maybe ()是.当然,有

   type BarEtaA = Maybe
   

   然后StateT Int BarEtaA ()再次有效,因为别名BarEtaA在扩展到其定义值之前不需要任何参数Maybe.

别名和构造函数之间存在一些其他小的差异,但它们不是基本的(并且通过适当的GHC扩展放宽).

在标准Haskell中我可以想到的构造函数和变量之间只有一个区别,即它们与类型类机制的交互.具体而言,实例必须是形式instance <class> (<constructor> <variable> <variable> <variable> ...) where ...,约束/上下文必须是形式<class> (<constructor> <variable> <variable> ...) => ....适当的GHC扩展可以放宽这些限制.

GHC实现的扩展Haskell还包括两种其他形式的已定义类型级别名称,类型系列和数据系列,它们混合了上述某些属性.数据族定义的名称与构造函数非常相似(它们是单射的,可以部分应用),而类型族定义的名称与别名非常相似(它们不能保证是单射的,也不能部分应用).主要区别在于它们可以进行"类型级模式匹配",其中有多种定义适用于不同情况.完整描述可能不适合StackOverflow答案,但手册描述了它们并链接到讨论它们的几篇冗长的论文.