类型级编程的一些例子是什么？

Question

我不明白“类型级编程”是什么意思，也无法通过谷歌找到合适的解释。

请问有人能提供一个演示类型级编程的例子吗？对该范 Paradigm 的解释和/或定义也会很有用。

- Vanio Begic

---

我推荐阅读《The Monad Reader》第8期中的《Type-Level Instant Insanity》一文。您可以在此链接中获取该期刊：http://www.haskell.org/wikiupload/d/dd/TMR-Issue8.pdf。 - Gabriella Gonzalez

参见：https://dev59.com/0m855IYBdhLWcg3wUScW - Jesper

Answer 1

你已经熟悉“值级别”编程，通过它你可以操作如42 :: Int或'a' :: Char之类的值。在像Haskell、Scala等许多其他语言中，类型级别编程允许你操作像Int :: *或Char :: *这样的类型，其中*是具体类型的类别（Maybe a或[a]是具体类型，但Maybe或[]不是，它们的类别为* -> *）。

考虑这个函数

foo :: Char -> Int
foo x = fromEnum x

这里的foo接受一个类型为Char的value，并使用Char的Enum实例返回一个新的Int类型的值。该函数操作值。

现在将foo与启用了TypeFamilies语言扩展的这个类型族进行比较。

type family Foo (x :: *)
type instance Foo Char = Int

在这里，Foo 接受一种 kind 为 * 的 type 并使用简单的映射 Char -> Int 返回一个新的 * 类型。这是一个操作类型的类型级函数。

这只是一个非常简单的例子，你可能会想知道它如何可能有用。使用更强大的语言工具，我们可以开始在类型级别上对代码的正确性进行编码证明（更多信息请参见Curry-Howard correspondence）。

一个实际的例子是红黑树，它使用类型级编程来静态保证树的不变量。

红黑树具有以下简单属性：

1. 节点要么是红色的要么是黑色的。
2. 根节点是黑色的。
3. 所有叶子节点都是黑色的。（所有叶子节点与根节点颜色相同。）
4. 每个红色节点必须有两个黑色子节点。从给定节点到任何其后代叶节点的路径包含相同数量的黑节点。

我们将使用 DataKinds 和 GADTs，这是一种非常强大的类型级编程组合。

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

import GHC.TypeLits

首先，一些用于表示颜色的类型。

data Colour = Red | Black -- promoted to types via DataKinds

这定义了一个新类型Colour，它包含两种类型：Red和Black。请注意，这些类型中没有任何实际的数值（忽略底部），但我们也不需要它们。

红黑树节点由以下GADT表示：

-- 'c' is the Colour of the node, either Red or Black
-- 'n' is the number of black child nodes, a type level Natural number
-- 'a' is the type of the values this node contains
data Node (c :: Colour) (n :: Nat) a where
    -- all leaves are black
    Leaf :: Node Black 1 a
    -- black nodes can have children of either colour
    B    :: Node l     n a -> a -> Node r     n a -> Node Black (n + 1) a
    -- red nodes can only have black children
    R    :: Node Black n a -> a -> Node Black n a -> Node Red n a

GADT让我们可以直接在类型中表达R和B构造函数的Colour。

树的根看起来像这样

data RedBlackTree a where
    RBTree :: Node Black n a -> RedBlackTree a

现在创建一个违反上述四条属性之一的类型化的RedBlackTree是不可能的。

1. 第一个限制显然是正确的，只有两种类型居住于Colour中。
2. 根据RedBlackTree的定义，根节点是黑色的。
3. 根据Leaf构造函数的定义，所有叶子都是黑色的。
4. 根据R构造函数的定义，它的两个子节点都必须是Black节点。同样，每个子树的黑色子节点数目相等（左右子树的类型中使用相同的n）。

GHC会在编译时检查所有这些条件，这意味着我们永远不会因为某些行为不当的代码而得到运行时异常，从而使我们对红黑树的假设无效。重要的是，这些额外的好处没有与之相关的运行时成本，所有工作都在编译时完成。

- cdk

---

红黑树示例点赞 +1。 - mbatchkarov

Answer 2

在大多数静态类型语言中，你有两个“领域”：值级别和类型级别（某些语言甚至有更多）。类型级别编程涉及在类型系统中编码逻辑（通常是函数抽象），这在编译时进行评估。一些例子包括模板元编程或 Haskell 类型家族。

为了在 Haskell 中完成这个示例，需要一些语言扩展，但现在你可以忽略它们，只需将类型家族视为在类型级别数字（Nat）上的函数即可。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits
import Data.Proxy

-- value-level
odd :: Integer -> Bool
odd 0 = False
odd 1 = True
odd n = odd (n-2)

-- type-level
type family Odd (n :: Nat) :: Bool where
    Odd 0 = False
    Odd 1 = True
    Odd n = Odd (n - 2)

test1 = Proxy :: Proxy (Odd 10)
test2 = Proxy :: Proxy (Odd 11)

这里我们不是测试自然数value是否为奇数，而是测试自然数type是否为奇数，并将其在编译时降级为类型级别的布尔值。如果您评估此程序，则会在编译时计算test1和test2的类型：

λ: :type test1
test1 :: Proxy 'False
λ: :type test2
test2 :: Proxy 'True

这就是类型级编程的精髓，根据语言的不同，你可以在类型级别上编码复杂逻辑，其具有各种用途。例如限制值级别上的某些行为、管理资源终止或存储更多关于数据结构的信息。

- Stephen Diehl

---

为什么你在这里需要UndecidableInstances？这样的工具应该只在实际使用的模块中使用，是吧？ - dfeuer

否则，“Odd n = Odd (n-2)”将无法通过类型族递归条件检查器的检查。 - Stephen Diehl

我接受了你的答案，因为你回答了我的原始问题，即关于类型级编程的定义。非常感谢你。 - Vanio Begic

Answer 3

其他答案非常好，但我想强调一点。我们的编程语言理论基于Lambda演算的术语。一个“纯”Lisp（一种编程语言）（或多或少）对应于一个重度糖化的无类型Lambda演算。程序的含义由评估规则定义，这些规则说明Lambda Calculus术语在程序运行时如何被约简。

在类型化语言中，我们为术语分配类型。对于每个评估规则，我们有一个相应的类型规则，显示如何通过评估来保留类型。根据类型系统，还有其他规则定义类型之间的关系。事实证明，一旦您获得足够有趣的类型系统，类型及其规则系统也对应于Lambda演算的变体！

尽管现在将Lambda演算视为一种编程语言很常见，但最初它是作为逻辑系统设计的。这就是它对于推理编程语言中的术语类型很有用的原因。但Lambda演算的编程语言方面允许人们编写由类型检查器评估的程序。

希望现在您可以看到，“类型级别编程”与“术语级别编程”并没有实质上的不同之处，只是目前很少有语言中使用了强大到需要在其类型系统中编写程序的类型系统。

- Levi Pearson

---

最后一段非常好。Coq证明助手中使用的语言Gallina是一个将类型和术语视为同等重要的编程语言的例子。 - Clément