在 Haskell 中,种类除了星形序列之外还能是其他什么吗?

Jam*_*ter 15 haskell

如果这个问题很愚蠢,请原谅我。

在阅读 Haskell 类型时,我注意到一个主题:

*
* -> *
* -> * -> *
Run Code Online (Sandbox Code Playgroud)

我的印象是 Haskell 中的类型最终归结为星号的数量。您可能会说,类型的种类实际上只是在它变成 * 之前需要应用于它的类型数量。换句话说,您可以计算除最后一个之外的所有 *,并通过整数定义类型的种类。说 0、1、2 等。

这是我的问题:

这是对 Haskell 类型系统的正确观察吗?或者它是否允许 * 之外的其他内容出现在您通常看到 * 的地方?例如:

* -> a -> *
Run Code Online (Sandbox Code Playgroud)

例如,我想有人可能想要这样做来限制类型变量具有类型类的实例。

Functor a, Applicative b => * -> a -> b -> *
Run Code Online (Sandbox Code Playgroud)

这是一件事吗?

Ben*_*Ben 16

这种语言的最基本形式仅包含*(或者Type在更现代的 Haskell 中;我怀疑我们最终会放弃*) 和->

但是,使用该语言可以构建的东西比仅通过“计算 s 的数量”所能表达的东西要多*。重要的不仅仅是*或的数量->,还有它们的嵌套方式。例如* -> * -> *,是采用两个类型参数来生成类型的事物,但是(* -> *) -> *采用单个参数来生成类型的事物,其中该参数本身必须是采用类型参数来生成类型的事物。data ThreeStars a b = Cons a b使用 kind 创建类型构造函数* -> * -> *,同时data AlsoThreeStars f = AlsoCons (f Integer)使用 kind 创建类型构造函数(* -> *) -> *

有几种语言扩展可以为同类语言添加更多功能。

PolyKinds添加类型变量,其工作方式与类型变量的工作方式完全相同。现在我们可以有类似的类型forall k. (* -> k) -> k

ConstraintKinds=>使约束( in 类型签名左侧的内容,例如Eq a)成为一种新类型的普通类型级实体:Constraint。现在可以接受的是带有 kind 的东西,而不是=>与语言的其余部分完全脱节的特殊用途语法的剩余部分Constraint。像这样的类Eq成为带有 kind 的类型构造函数* -> Constraint;您将其应用于类似Eq Bool生成Constraint. 优点是现在我们可以使用所有语言功能来操作类型级实体来操作约束(包括PolyKinds!)。

DataKinds添加了创建包含新类型级别事物的新用户定义类型的能力,与在 vanilla Haskell 中我们可以创建包含新术语级别事物的新用户定义类型完全相同。(完全相同的方式;实际工作的方式DataKinds是它允许您data正常使用声明,然后您可以在类型或种类级别使用生成的类型构造函数)

还有一些用于未装箱/未提升类型的类型,它们不得与“普通”Haskell 类型混合,因为它们具有不同的内存布局;它们不能包含 thunk 来实现惰性求值,因此运行时必须知道永远不要尝试将它们作为代码指针“输入”,或查找其他标头位等。它们需要在种类级别保持分离,以便普通类型变量*不能用这些未提升/未装箱的类型实例化(这将允许您将这些需要特殊处理的类型传递给不知道提供特殊处理的通用代码)。我隐约知道这个东西,但从未真正使用过它,所以我不会再添加任何东西,以免我弄错任何东西。(任何知道自己在说什么的人都可以在这里写一个简短的总结段落,请随时编辑答案)

可能还有其他一些我忘记了。但当然,这种语言比 OP 想象的仅具有基本 Haskell 功能更丰富,而且一旦您打开一些(相当广泛使用的)扩展,它还有更多功能。

  • 类型的另一个来源是其值可能是“未提升”或“未装箱”的类型类型。“*”又名“Type”,是像“Int”这样的类型,其值是“提升”的,也就是说,可以是挂起的计算(thunks),甚至是“未定义”。但 Haskell 也有像 `Int#` 这样的类型,它们是实际的“机器整数”,不能是 thunk。每种可能的内存表示都有其自己的类型。GHC 的这一方面仍在不断发展。https://downloads.haskell.org/~ghc/9.0.1/docs/html/users_guide/exts/primitives.html#unboxed-type-kinds (5认同)