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

Question

我不明白"类型级编程"的含义,也无法使用Google找到合适的解释.

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

Answer 1

您已经熟悉"价值级"编程,您可以通过它来操作诸如42 :: Int或之类的值'a' :: Char.在比如Haskell,Scala和许多其他语言,类型级编程让您操作类型,如Int :: *或Char :: *在那里*是一种具体类型的(Maybe a或者[a]是具体的类型,但不能Maybe或[]具有实物* -> *).

考虑这个功能

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

这里foo取一个type 值,并使用实例for 返回一个新的type值.此函数操纵值. CharIntEnumChar

现在与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让我们表达Colour的R和B建设者直接在类型.

树的根看起来像这样

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)

这里不是测试自然数值是否是奇数,而是测试自然数字类型是否为奇数,并在编译时将其减少为类型级布尔值.如果您评估此程序test1,test2则在编译时计算和的类型为:

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

这是类型级编程的本质,取决于您可以在类型级别编码具有各种用途的复杂逻辑的语言.例如,限制值级别的某些行为,管理资源最终化或存储有关数据结构的更多信息.

Answer 3

其他答案非常好,但我想强调一点.我们的编程语言术语理论基于Lambda微积分."纯粹的"Lisp对应于(或多或少)严重加糖的无类型Lambda微积分.程序的含义由评估规则定义,该规则说明在程序运行时如何减少Lambda微积分项.

在类型语言中,我们将类型分配给术语.对于每个评估规则,我们都有一个相应的类型规则,显示如何通过评估保留类型.根据类型系统,还有其他规则定义类型彼此之间的关系.事实证明,一旦你得到一个足够有趣的类型系统,类型及其规则系统也对应于Lambda微积分的变体!

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

希望您现在可以看到"类型级编程"与"术语级编程"并不是完全不同的事情,只是现在在类型系统中使用一种功能足够强大的语言并不常见.在其中编写程序的理由.