时间戳

首页 > 解决方案 > 不是类型构造函数的类型级函数示例

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

问题描述

与其他类型级函数相比，Haskell 中的“类型构造函数”概念有何独特之处？

据我所知，他们：

标签： haskelltype-level-computation

解决方案

短语“类型构造函数”有两种常见用法。有些人将它们用于任何带有箭头的类型；但是 Haskell 报告以不同的方式非常一致地使用它，所以我将讨论这个定义。

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

Either
Maybe
[]
Bool

哎呀，你注意到最后一个了吗？没错，“类型构造函数”这个短语并没有暗示它必须能够接受参数。Bool是由数据声明引入的类型级别名称 - 因此是类型构造函数。以下是一些不是构造函数的类型示例：

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

哎呀，你注意到最后两个了吗？没错，在另一个方向上，没有什么可以让你成为类型构造函数的更多类型参数。每个Eitherand()都是构造函数，但Eitherto的应用不是，因为它不是由or声明()创建的单个类型级名称。同样，is 是一个类型变量，而不是构造函数——它的含义不是由任何or声明固定的。datanewtypemdatanewtype

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

  1. 构造函数是单射的，别名可能不是。如果FooC a b candFooC a' b' c'是同一类型，andFooC是构造函数，则aanda'是同一类型，bandb'是同一类型，candc'是同一类型。对比

    type FooA a = String

    其中FooA ()和FooA Bool是同一类型，即使()和Bool不是同一类型。

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

    type BarA a = Maybe a

    thenStateT Int BarA ()是无效的——BarA必须总是立即给出它的类型参数——即使StateT Int Maybe ()是。当然，与

    type BarEtaA = Maybe

    thenStateT Int BarEtaA ()再次有效，因为别名BarEtaA在扩展为其定义的值之前不需要任何参数Maybe。

别名和构造函数之间还有一些其他小的差异，但它们不是基本的（并且可以通过合适的 GHC 扩展来放松）。

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

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

推荐阅读