这星期的文章是

http://cs.brynmawr.edu/~rae/papers/2012/singletons/paper.pdf。

这paper在codewars上，可以做做看：Singletons | Codewars

这文章在说两件事情：

0：用一种design pattern来做DT

1：这个design pattern可以用库automate一大部分

0：

假设我们有普普通通的data Nat = Z | S Nat。

首先，如果我们要把这用上type level（因为dependent type就是value可以在typelevel使用），我们需要额外的两个类型，一个ZType :: *，一个SType :: * -> *，来表示Nat的type level表示。然后，type level的Nat函数，可以用type family写出。

然后，可以用GADT表示inductive dependent type，比如Vec之类的。如果不支持GADT（什么鬼，不支持还想玩奇怪特性）可以考虑考虑用gadtless programming，换句话说用Leibniz Equality手动解constraint。。。

但是，由于parametricity，这无法做到：给入一个type level Nat，输出一个该长度的Vec。。。所以，做法是，再弄一个GADT inductive type，这个GADT的value是indexed on type level nat的。换言之，每一个type level nat，都能在这个GADT中找到一个unique的对应值。这就叫singleton

最后，很多时候singleton可以隐式推出，所以可以弄成一个constraint。

总结，一个datatype有4种做法：普通的，type level的，singleton，singleton变成constraint（换句话说，typeclass）。

1：

type level的可以由GHC的DataKinds扩展自动生成。

singleton constraint可以统一到一个typeclass

由template haskell可以从普通函数生成singleton函数跟type level函数（type family）

最后：singleton constraint跟Data.Constraint有异曲同工之妙:)

还有，下期想看啥接着私信我。。。no monad tutorial，no 女装=/=