哈斯克尔单身人士：我们从SNat获得什么 [英] Haskell singletons: What do we gain with SNat
问题描述
在独立编程单身计划
和他的博客文章 singletons v0.9已发布！
Richard Eisenberg定义了数据类型 Nat ，它用peano公理定义自然数：
数据Nat = Zero | Succ Nat
通过使用语言扩展名 DataKinds ，此数据类型被提升为类型级别。
数据构造函数 Zero 和 Succ 被提升为类型构造函数'Zero 和'Succ 。
通过这个，我们可以得到每个自然数在类型级别上唯一且唯一的对应类型。例如，对于 3 ，我们得到'Succ（'Succ（'Succ'Zero））。
所以我们现在有自然数作为类型。
可以进行加法操作。
通过singletons库的 promote 函数/ quasiqoter，我们可以自动从$ em $加上 创建 Plus 功能。所以我们可以避免写这个类型的家庭自己。
到目前为止好！
使用GADT语法，他也定义一个数据类型 SNat ：
data SNat :: Nat - > *其中
SZero :: SNat零
SSucc :: SNat n - > SNat（Succ n）
基本上他只是将 Nat 类型换成 SNat 构造函数。
为什么这是必要的？我们得到什么？
数据类型 Nat 和 SNat 不同构吗？为什么 SNat 是单身人士，为什么Nat 不是
单身人士？在这两种情况下，每种类型都有一个单一的值，即相应的自然数。
我们得到什么？嗯。单身人士的地位是尴尬，但目前必要的解决方法，我们越早取消他们，越好。
让我看看我是否可以澄清图片。我们有一个数据类型 Nat ：
数据Nat = Zero | （战争已经开始了，甚至更多的微不足道的问题比'c'的数量在替换属性，这意味着在任何类型良好的程序中，您可以用具有相同范围和类型的备选子表达式来替换任何类型良好的子表达式，并且程序将继续打得很好。例如，如果< b>>，则可以重写每次出现的
然后< t>其他< e>
至
如果< b>然后< e>其他< t>
并且您可以确定没有任何问题会发生......检查程序类型的结果。
置换物业是一种尴尬。这明显证明了你的类型系统在意义开始变得重要的时刻就放弃了。
现在，通过作为运行时值的数据类型， Nat 也成为一种类型级别的值'Zero 和'Suc 。后者仅以Haskell的类型语言生活，根本没有运行时间存在。请注意，尽管在类型级别存在'Zero 和'Suc ，但将其称为类型和目前这样做的人应该停止。他们没有类型 * ，因此不能对值进行分类，这是值得称呼的类型。
在运行时和类型级 Nat s之间没有直接的交换方式，这可能是一个麻烦。示例性示例涉及对向量的关键操作：
数据Vec :: Nat - > * - > *其中
VNil :: Vec'零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 量词，它是参数：它表明量化信息只能用于类型，并且被运行时间擦除。
Haskell目前在相关量化（ forall ）和执行擦除操作时强制执行完全虚假的重合。它不会支持一个依赖但未被擦除的量词，我们通常称它为 pi 。 vec 的类型和实现应该类似于
vec :: pi（n :: Nat） - > forall（x :: *）。 Vec nx
vec'Zero x = VNil
vec（'Suc n）x = VCons x（vec nx）
其中 pi -positions中的参数用类型语言编写，但数据在运行时可用。
那么我们做什么呢？我们使用单例来间接捕获它是什么意思是一个类型级别数据的运行时拷贝。
data SNat :: Nat - > *其中
SZero :: SNat Zero
SSuc :: SNat n - > SNat（Suc n）
现在， SZero 和 SSuc 生成运行时数据。 SNat 不同构于 Nat ：前者的类型为 Nat - > * ，而后者的类型为 * ，所以尝试使它们同构是一种类型错误。在 Nat 中有许多运行时值，类型系统不区分它们;在每个不同的 SNat n 中只有一个运行时间值（值得一提），所以类型系统无法区分它们的事实就在这一点上。关键是每个 SNat n 对于每个不同的 n 都是不同的类型，并且GADT模式匹配（其中a模式可以是GADT类型的一个更具体的实例，它可以改进我们对 n 的了解。
我们现在可以写出
vec :: forall（n :: Nat）。 SNat n - > forall（x :: *）。 x - > Vec nx
vec SZero x = VNil
vec（SSuc n）x = VCons x（vec nx）
通过利用唯一的运行时分析形式可以改进类型信息，单例允许我们缩短运行时间和类型级别数据之间的差距。想知道他们是否真的有必要，而且他们目前只是因为这种差距还没有被消除是相当明智的。
I'm trying to grook Haskell singletons.
In the paper Dependently Typed Programming with Singletons
and in his blog post singletons v0.9 Released!
Richard Eisenberg defines the data type Nat which defines natural numbers with the peano axioms:
data Nat = Zero | Succ Nat
By using the language extension DataKinds this data type is promoted to the type level.
The data constuctors Zero and Succ are promoted to the type constructors 'Zero and 'Succ.
With this we get for every Natural number a single and unique corresponding type on the type level. Eg for 3 we get 'Succ ( 'Succ ( 'Succ 'Zero)).
So we have now Natural numbers as types.
He then defines on the value level the function plus and on the type level the type family Plus
to have the addition operation available.
With the promote function/quasiqoter of the singletons library we can automatically
create the Plus type family from the plus function. So we can avoid writing the type family ourselfs.
So far so good!
With GADT syntax he also defines a data type SNat:
data SNat :: Nat -> * where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
Basically he only wraps the Nat type into a SNat constructor.
Why is this necessary? What do we gain?
Are the data types Nat and SNat not isomorphic? Why is SNat a singleton, and why is Nat not
a singleton? In both cases every type is inhabited by one single value, the corresponding natural number.
解决方案 What do we gain? Hmm. The status of singletons is that of awkward but currently necessary workaround, and the sooner we can do away with them, the better.
Let me see if I can clarify the picture. We have a data type Nat:
data Nat = Zero | Suc Nat
(wars have been started over even more trivial issues than the number of 'c's in Suc)
The type Nat has run-time values which are indistinguishable at the type level. The Haskell type system currently has the replacement property, which means that in any well typed program, you may replace any well typed subexpression by an alternative subexpression with the same scope and type, and the program will continue to be well typed. For example, you can rewrite every occurrence of
if <b> then <t> else <e>
to
if <b> then <e> else <t>
and you can be sure that nothing will go wrong...with the outcome of checking your program's type.
The replacement property is an embarrassment. It's clear proof that your type system gives up at the very moment that meaning starts to matter.
Now, by being a data type for run-time values, Nat also becomes a type of type-level values 'Zero and 'Suc. The latter live only in Haskell's type language and have no run-time presence at all. Please note that although 'Zero and 'Suc exist at the type level, it is unhelpful to refer to them as "types" and the people who currently do that should desist. They do not have type * and can thus not classify values which is what types worthy of the name do.
There is no direct means of exchange between run-time and type-level Nats, which can be a nuisance. The paradigmatic example concerns a key operation on vectors:
data Vec :: Nat -> * -> * where
VNil :: Vec 'Zero x
VCons :: x -> Vec n x -> Vec ('Suc n) x
We might like to compute a vector of copies of a given element (perhaps as part of an Applicative instance). It might look like a good idea to give the type
vec :: forall (n :: Nat) (x :: *). x -> Vec n x
but can that possibly work? In order to make n copies of something, we need to know n at run time: a program has to decide whether to deploy VNil and stop or to deploy VCons and keep going, and it needs some data to do that. A good clue is the forall quantifier, which is parametric: it indicates thats the quantified information is available only to types and is erased by run time.
Haskell currently enforces an entirely spurious coincidence between dependent quantification (what forall does) and erasure for run time. It does not support a dependent but not erased quantifier, which we often call pi. The type and implementation of vec should be something like
vec :: pi (n :: Nat) -> forall (x :: *). Vec n x
vec 'Zero x = VNil
vec ('Suc n) x = VCons x (vec n x)
where arguments in pi-positions are written in the type language, but the data are available at run time.
So what do we do instead? We use singletons to capture indirectly what it means to be a run-time copy of type-level data.
data SNat :: Nat -> * where
SZero :: SNat Zero
SSuc :: SNat n -> SNat (Suc n)
Now, SZero and SSuc make run-time data. SNat is not isomorphic to Nat: the former has type Nat -> *, while the latter has type *, so it is a type error to try to make them isomorphic. There are many run-time values in Nat, and the type system does not distinguish them; there is exactly one run-time value (worth speaking of) in each different SNat n, so the fact that the type system cannot distinguish them is beside the point. The point is that each SNat n is a different type for each different n, and that GADT pattern matching (where a pattern can be of a more specific instance of the GADT type it is known to be matching) can refine our knowledge of n.
We may now write
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)
Singletons allow us to bridge the gap between run time and type-level data, by exploiting the only form of run-time analysis that allows the refinement of type information. It's quite sensible to wonder if they're really necessary, and they presently are, only because that gap has not yet been eliminated.
这篇关于哈斯克尔单身人士：我们从SNat获得什么的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
