哈斯克尔单身人士：我们从SNat获得什么
我正在尝试追查哈斯克尔的单身人士。
在论文中依赖类型化编程单身人士和在他的博客文章singletons v0.9发布！ Richard Eisenberg定义了用peano公理定义自然数的数据类型Nat：
data Nat = Zero | Succ Nat
通过使用语言扩展DataKinds，该数据类型被提升为类型级别。 数据构造器Zero和Succ被提升为类型构造器的“零”和“Succ”。 有了这个，我们可以为每个自然数获得一个类型级别上唯一且唯一的对应类型。 例如，对于3，我们得到'Succ（'Succ（'Succ'Zero））。 所以我们现在有自然数作为类型。
然后，他在数值级别上定义了函数加，并在类型级别上定义了类型族Plus以具有加法操作可用。 通过singletons库的提升函数/ quasiqoter，我们可以从plus函数自动创建Plus类型系列。 所以我们可以避免写这种类型的家庭自己。
到现在为止还挺好！
使用GADT语法，他还定义了一个数据类型SNat：
data SNat :: Nat -> * where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
基本上他只把Nat类型包装成SNat构造函数。 为什么这是必要的？ 我们得到什么？ 数据类型Nat和SNat不是同构的吗？ 为什么SNat是一个单身人士，为什么Nat不是一个单身人士？ 在这两种情况下，每种类型都有一个单一的值，即相应的自然数。
我们得到什么？ 嗯。 单身人士的地位是尴尬的，但目前是必要的解决办法，我们越早取消他们就越好。
让我看看我能否澄清这幅画。 我们有一个数据类型Nat ：
data Nat = Zero | Suc Nat
（战争已经开始了，甚至比Suc中'c's的数量还要多）
类型Nat具有在类型级别无法区分的运行时值。 Haskell类型系统目前具有替换属性，这意味着在任何类型良好的程序中，您可以用具有相同范围和类型的替代子表达式来替换任何已打好类型的子表达式，并且程序将继续保持良好的类型。 例如，你可以重写每一个出现的地方
if <b> then <t> else <e>
至
if <b> then <e> else <t>
你可以确定没有任何问题会出现......检查你的程序类型的结果。
置换物业是一个尴尬。 很明显，你的类型系统在意义开始变得重要的时刻就放弃了。
现在，通过作为运行时间值的数据类型， Nat也变成了一种类型值为'Zero 'Suc和'Suc 'Zero的类型。 后者仅以Haskell的类型语言生活，根本没有运行时间存在。 请注意，尽管在类型级别存在'Zero 'Suc ，但将它们称为“类型”并且目前这样做的人应该停止是没有帮助的。 他们没有类型* ，因此不能对值得分类的值进行分类。
在运行时和类型级Nat之间没有直接的交换方式，这可能是一种麻烦。 典范示例涉及向量的关键操作：
data Vec :: Nat -> * -> * where
VNil :: Vec 'Zero x
VCons :: x -> Vec n x -> Vec ('Suc n) x
我们可能想要计算给定元素的副本的向量（可能是Applicative实例的一部分）。 给这种类型看起来可能是个好主意
vec :: forall (n :: Nat) (x :: *). x -> Vec n x
但可以工作吗？ 为了制作n副本，我们需要在运行时知道n ：一个程序必须决定是否部署VNil并停止或部署VCons并继续前进，并且需要一些数据来执行此操作。 一个很好的线索是forall量词，它是参数：表示这就是量化信息只提供给类型，并通过运行时间删除。
哈斯克尔目前强制执行相关的定量（什么之间的完全站不住脚的巧合forall一样）和擦除的运行时间。 它不支持依赖但未擦除的量词，我们通常称其为pi 。 vec的类型和实现应该是类似的
vec :: pi (n :: Nat) -> forall (x :: *). Vec n x
vec 'Zero x = VNil
vec ('Suc n) x = VCons x (vec n x)
在pi -positions中的参数是用类型语言编写的，但数据在运行时可用。
那么我们做什么呢？ 我们使用单例来间接获取它作为类型级数据的运行时副本的含义。
data SNat :: Nat -> * where
SZero :: SNat Zero
SSuc :: SNat n -> SNat (Suc n)
现在， SZero和SSuc创建运行时数据。 SNat与Nat构：前者具有类型Nat -> * ，而后者具有类型* ，所以尝试使它们同构是一种类型错误。 Nat有许多运行时间值，类型系统不区分它们; 在每个不同的SNat n只有一个运行时间值（值得一提），所以类型系统无法区分它们的事实就在这一点上。 点是每个SNat n是一种不同类型的对于每个不同的n ，并且GADT模式匹配（其中一个图案可以是GADT类型，已知的是被匹配的更具体的实例的）可以改进我们的知识n 。
我们现在可以写
vec :: forall (n :: Nat). SNat n -> forall (x :: *). x -> Vec n x
vec SZero x = VNil
vec (SSuc n) x = VCons x (vec n x)
单例允许我们通过利用运行时分析的唯一形式来弥补运行时间和类型级数据之间的差距，从而允许对类型信息进行优化。 想知道他们是否真的有必要，而且他们目前只是因为这种差距还没有被消除，这是相当明智的。
链接地址: http://www.djcxy.com/p/33347.html