什么是类型级编程的一些例子？ [英] What are some examples of type-level programming?

问题描述

我不明白type-level programming是什么意思，也不能用Google找到合适的解释。

有人可以提供一个演示类型的例子级编程？

解决方案

在大多数静态类型语言中，您有两个域价值层面和类型层面（一些语言甚至更多）。类型级编程涉及在编译时评估的类型系统中的编码逻辑（通常是函数抽象）。一些例子是模板元编程或者Haskell类型族。

在Haskell中做这个例子需要一些语言扩展，但你现在忽略它们，只是看在类型家族中作为一个函数，而不是类型级数字（ Nat ）。

  { - ＃LANGUAGE DataKinds＃ - } 
 { - ＃LANGUAGE TypeFamilies＃ - } 
 { - ＃LANGUAGE TypeOperators＃ - } 
 { - ＃LANGUAGE UndecidableInstances＃ - } 
 
导入GHC.TypeLits 
导入Data.Proxy 
 
  - 值级
 odd :: Integer  - > Bool 
 odd 0 = False 
 odd 1 = True 
 odd n = odd（n-2）
 
  - 类型级
类型系列Odd （n :: Nat）:: Bool其中
奇数0 =假
奇数1 =真
奇数n =奇数（n  -  2）
 
 test1 =代理:: Proxy（Odd 10）
 test2 = Proxy :: Proxy（Odd 11）
  

在这里，我们不是测试一个自然数的值是否是一个奇数，而是测试一个自然数 type 是否是一个奇数并将其减少到一个类型级布尔值在编译时。如果你评估这个程序，在编译时计算 test1 和 test2 的类型为：

 λ：：type test1 
 test1 :: Proxy'False 
λ：：type test2 
 test2 ::代理'真正的
  

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

I do not understand what "type-level programming" means, nor can I find a suitable explanation using Google.

Could someone please provide an example that demonstrates type-level programming? Explanations and/or definitions of the paradigm would be useful and appreciated.

解决方案

In most statically typed languages you have two "domains" the value-level and the type-level (some languages have even more). Type-level programming involves encoding logic ( often function abstraction ) in the type-system which is evaluated at compile-time. Some examples would be template metaprogramming or Haskell type-families.

A few languages extensions are needed to do this example in Haskell but you kind of ignore them for now and just look at the type-family as being a function but over type-level numbers (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)

Here instead of testing whether a natural number value is an odd number, we're testing whether a natural number type is an odd number and reducing it to a type-level Boolean at compile-time. If you evaluate this program the types of test1 and test2 are computed at compile-time to:

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

That's the essence of type-level programming, depending on the language you may be able to encode complex logic at the type-level which have a variety of uses. For example to restrict certain behavior at the value-level, manage resource finalization, or store more information about data-structures.

这篇关于什么是类型级编程的一些例子？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！