类型声明中的类型限制

Question

类型级自然数有著名的例子：

data Zero
data Succ n

我对应用类型构造函数时的理想限制有疑问Succ。例如，如果我们想在函数定义中做这样的限制，我们可以使用 class 和上下文，就像在这段代码中：

class Nat n where
  toInt :: n -> Int
instance Nat Zero where
  toInt _ = 0
instance (Nat n) => Nat (Succ n) where
  toInt _ = 1 + toInt (undefined :: n)

用不了toInt (undefined :: Succ Int)，没关系

但是如何在类型级构造上实现类似的限制（可能使用一些高级类型扩展）？

例如，我想允许类型构造函数 Succ 仅与类型 Zero 和类似这样的东西一起使用：Succ (Succ Zero)、Succ (Succ (Succ Zero)) 和很快。如何在编译时避免这样的坏例子：

type Test = Succ Int

（暂时没有编译错误）

P.S.: 对我来说更有趣的是如何对最后一个示例的类型声明创建限制

Answer 1

如今，我们使用 DataKinds 扩展名：

{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables #-}

-- N is a type, but is also a kind now
-- Zero, Succ Zero, ... are values, but are also type-level values of
-- kind N
data N = Zero | Succ N

-- (We could import Proxy the library, instead)
data Proxy (n :: N) = Proxy

-- Now n is restricted to kind N
class Nat (n :: N) where
  toInt :: proxy n -> Int

instance Nat Zero where
  toInt _ = 0
instance (Nat n) => Nat (Succ n) where
  toInt _ = 1 + toInt (undefined :: Proxy n)

然后我们可以使用toInt (Proxy :: Proxy (Succ Zero))。相反，toInt (Proxy :: Proxy (Succ Int)) 会根据需要引发类型错误。

就我个人而言，我也会用更现代的东西替换代理，例如 AllowAmbiguousTypes 和 TypeApplications，以便删除未使用的参数。

{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables,
             AllowAmbiguousTypes, TypeApplications #-}

data N = Zero | Succ N

-- Now n is restricted to kind N
class Nat (n :: N) where
  toInt :: Int

instance Nat Zero where
  toInt = 0
instance (Nat n) => Nat (Succ n) where
  toInt = 1 + toInt @n

将其用作toInt @(Succ Zero)。 toInt @n 语法选择类型类中的 n。它不对应于运行时交换的任何值，仅对应于编译时存在的 type-level 参数。

正在使用

type Foo = Succ Int

也会根据需要出错：

    • Expected kind ‘N’, but ‘Int’ has kind ‘*’
    • In the first argument of ‘Succ’, namely ‘Int’
      In the type ‘Succ Int’
      In the type declaration for ‘Foo’

类型声明中的类型限制

Type restriction in type declaration

haskell

type-systems

gadt

phantom-types

data-kinds