haskell - Haskell 类型构造函数可以有非类型参数吗？

Question

类型构造函数产生给定类型的类型。例如，Maybe 构造函数

data Maybe a = Nothing | Just a

可以是一个给定的具体类型，如 Char，并给出一个具体的类型，如 Maybe Char。就种类而言，有

GHCI> :k Maybe
Maybe :: * -> *

我的问题:是否可以定义一个类型构造函数，它会产生一个给定 Char 的具体类型，比如说？换句话说，是否可以在类型构造函数的类型签名中混合类型和类型？就像是

GHCI> :k my_type
my_type :: Char -> * -> *

Answer 1

Can a Haskell type constructor have non-type parameters?

让我们解开类型参数的含义。 “类型”这个词(至少)有两种可能的含义:您是指狭义的类型事物吗 * ，或者更广泛意义上的类型级别的事物？我们(还)不能在类型中使用值，但现代 GHC 具有非常丰富的种类语言，允许我们使用除具体类型之外的广泛事物作为类型参数。

高级类型

Haskell 中的类型构造函数总是承认非 *参数。例如，仿函数不动点的编码在普通的 Haskell 98 中工作:

newtype Fix f = Fix { unFix :: f (Fix f) }

ghci> :k Fix
Fix :: (* -> *) -> *

Fix由类型为 * -> * 的仿函数参数化, 不是一种类型 * .

超越 *和 -> DataKinds扩展通过用户声明的种类丰富了 GHC 的种类系统，因此种类可以由除 * 以外的部分构成和 -> .它的工作原理是促进所有 data声明到种类级别。也就是说，一个 data声明之类的

data Nat = Z | S Nat  -- natural numbers

介绍一种 Nat和类型构造函数 Z :: Nat和 S :: Nat -> Nat ，以及通常的类型和值构造函数。这允许您编写由类型级别数据参数化的数据类型，例如习惯的向量类型，它是一个按长度索引的链表。

data Vec n a where
    Nil :: Vec Z a
    (:>) :: a -> Vec n a -> Vec (S n) a

ghci> :k Vec
Vec :: Nat -> * -> *

有一个相关的扩展名为 ConstraintKinds , 释放约束，如 Ord a从“肥箭”的轭 => ，允许它们按照大自然的意图漫游在类型系统的景观中。 Kmett 使用这种力量 build 了一个 category of constraints , 与新型 (:-) :: Constraint -> Constraint -> *表示“包含”:类型为 c :- d 的值是证明如果 c然后持有 d也持有。例如，我们可以证明 Ord a暗示 Eq [a]所有 a :

ordToEqList :: Ord a :- Eq [a]
ordToEqList = Sub Dict

以后的生活 forall
但是，Haskell 目前在类型级别和值级别之间保持严格的分离。类型级别的东西总是在程序运行之前被删除，(几乎)总是可推断的，在表达式中不可见，并且(依赖)由 forall 量化.如果您的应用程序需要更灵活的东西，例如对运行时数据的相关量化，那么您必须使用单例编码手动模拟它。

例如 split的规范说它根据它的(运行时!)参数以一定的长度切割一个向量。输出向量的类型取决于 split 的值的论点。我们想写这个...

split :: (n :: Nat) -> Vec (n :+: m) a -> (Vec n a, Vec m a)

...我在哪里使用类型函数 (:+:) :: Nat -> Nat -> Nat ，代表添加类型级自然数，以确保输入向量至少与 n 一样长...

type family n :+: m where
    Z :+: m = m
    S n :+: m = S (n :+: m)

...但 Haskell 不允许声明 split !没有任何类型的值 Z或 S n ;只有种类 *包含值。我们无法访问 n在运行时直接，但我们可以使用 GADT，我们可以对其进行模式匹配来了解类型级别 n是:

data Natty n where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)

ghci> :k Natty
Natty :: Nat -> *

Natty被称为单例，因为对于给定的(明确定义的) n只有一个(明确定义的)类型的值 Natty n .我们可以使用 Natty n作为 n 的运行时替代品.

split :: Natty n -> Vec (n :+: m) a -> (Vec n a, Vec m a)
split Zy xs = (Nil, xs)
split (Sy n) (x :> xs) =
    let (ys, zs) = split n xs
    in (x :> ys, zs)

无论如何，关键是值——运行时数据——不能出现在类型中。复制 Nat 的定义很乏味以单例形式(如果您希望编译器推断此类值，情况会变得更糟)；依赖类型的语言，如 Agda、Idris 或 future 的 Haskell，摆脱了将类型与值严格分离的束缚，并为我们提供了一系列富有表现力的量词。您可以使用诚实的人 Nat如 split的运行时参数并在返回类型中独立提及其值。

@pigworker 写了大量关于 Haskell 在现代依赖类型编程中严格分离类型和值的不适用性的文章。例如，参见 the Hasochism paper ，或他的 talk四个十年的 Hindley-Milner 式编程灌输给我们的未经检验的假设。

依赖种类

最后，对于它的值(value)，与 TypeInType现代 GHC 统一了类型和种类，允许我们使用讨论类型变量的相同工具来讨论种类变量。在 a previous post关于我使用的 session 类型 TypeInType为标记的类型级序列定义一种类型:

infixr 5 :!, :?
data Session = Type :! Session  -- Type is a synonym for *
             | Type :? Session
             | E