Dependently Typed Programming with Singletons

這星期的文章是

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 女裝=/=