有哪些类型级编程的例子？ [关闭]

Question

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

有人可以提供一个演示类型级编程的示例吗？范式的解释和/或定义将是有用和赞赏的。

Answer 1

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

考虑这个函数

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

这里foo 采用类型 Char 的值 并使用Char 的Enum 实例返回Int 类型的新值。此函数操作值。

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

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

这里Foo 采用类型 种类 * 并使用简单映射Char -> Int 返回一种新类型*。这是一个操作类型的类型级函数。

这是一个非常简单的示例，您可能想知道这怎么可能有用。使用更强大的语言工具，我们可以开始在类型级别对代码正确性的证明进行编码（有关更多信息，请参阅Curry-Howard 通信）。

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

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

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 违反上述 4 个属性中的任何一个。

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

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

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

这就是类型级编程的精髓，这取决于您可能能够在类型级编码具有多种用途的复杂逻辑的语言。例如，在价值级别限制某些行为、管理资源最终确定或存储有关数据结构的更多信息。

Answer 3

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

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

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

希望您现在可以看到“类型级编程”与“术语级编程”并没有本质上的不同，只是现在在类型系统中拥有足够强大的语言并不常见有理由在里面写程序。