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

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

让我们通过类型参数解开你的意思.这个词类型有(至少)两个潜在的意思:你的意思类型中的狭义样的东西*,或在更广泛的意义上的东西在类型级别？我们不能(还)在类型中使用值,但现代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已经使用这种能力构建了一类约束,newtype (:-) :: 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或未来的Haskell,逃避了严格地将类型与值分开的暴政,并为我们提供了一系列富有表现力的量词.您可以使用诚实的优点Nat作为split运行时参数,并在返回类型中依赖于它的值.

@pigworker已经写了大量关于Haskell在现代依赖类型编程中严格区分类型和值的不适合性.见,例如,该Hasochism纸,或他的谈话对已经通过四个十年辛德米尔纳式编程的灌输给我们浑浑噩噩的假设.

依赖种类

最后,对于它的价值,TypeInType现代GHC统一了类型和种类,允许我们使用我们用来讨论类型变量的相同工具来讨论类型变量.在之前关于会话类型的帖子中,我使用了TypeInType为类型的标记类型级序列定义一种类型:

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