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

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

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

解决方法

在大多数静态类型的语言中，您有两个“域”的值级别和类型级别(一些语言甚至更多)。类型级编程涉及在编译时评估的类型系统中的编码逻辑(通常是函数抽象)。一些示例将是模板元编程或Haskell类型族。

在Haskell中需要几个语言扩展来做这个例子，但是你现在就忽略它们，只需将type-family视为一个函数，而不是类型级别的数字(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

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