[Haskell-beginners] Programming with Singletons

[Quentin Liu]

Hi all,

I was doing the “Singletons” problem at codewars[1]. The basic idea is to use dependent types to encode the length of the vector in types.

It uses
 data Nat = Zero | Succ Nat

 data SNat a where
   SZero :: SNat Zero
   SSucc :: SNat a -> SNat (Succ a)
to do the encoding.

The vector is defined based on the natural number encoding:
 data Vec a n where
   VNil :: Vec a Zero
   VCons :: a -> Vec a n -> Vec a (Succ n)


There are some type families declared for manipulating the natural numbers, and one of them that is relevant to the question is
 type family (Add (a :: Nat) (b :: Nat)) :: Nat
  type instance Add Zero b = b
  type instance Add a    Zero = a
  type instance Add (Succ a) (Succ b) = Succ (Succ (Add a b))
where the `Add` function adds natural numbers.

The problem I am stuck with is the concatenation of two vectors:
 (++) :: Vec v m -> Vec v n -> Vec v (Add m n)
 VNil ++ b = b
 (VCons x xs) ++ b = VCons x $ xs ++ b

The program would not compile because the compiler found that `VCons x $ xs ++ b`gives type `Vec v (Succ (Add n1 n))`, which does not follow the declared type `Vec v (Add m n)`. Is it because ghc does not expand `Add m n’ that the type does not match? I read Brent Yorgey’s blog on type-level programming[2] and he mentioned that would not automatically expand types. But the posted time of the blog is 2010 and I am wondering if there is any improvement to the situation since then? Besides, what would be the solution to this problem


Warm Regards,
Qingbo Liu

[1] https://www.codewars.com/kata/singletons/train/haskell
[2] https://byorgey.wordpress.com/2010/07/06/typed-type-level-programming-in-haskell-part-ii-type-families/

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/beginners/attachments/20171115/06cbb447/attachment.html>