[Haskell-beginners] Programming with Singletons

[mukesh tiwari]

Hi Quentin,
I changed your pattern little bit in Add function and it is working
fine. I think the problem was that type of (VCons x xs) ++++ b is Vec
v (Add (Succ m1) + n) which was not present in your
Add function pattern.



{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
module Tmp where

data Nat = Zero | Succ Nat

data SNat a where
  SZero :: SNat Zero
  SSucc :: SNat a -> SNat (Succ a)

data Vec a n where
  VNil :: Vec a Zero
  VCons :: a -> Vec a n -> Vec a (Succ n)

type family (Add (a :: Nat) (b :: Nat)) :: Nat
type instance Add Zero b = b
type instance Add (Succ a) b = Succ (Add a b)

(++++) :: Vec v m -> Vec v n -> Vec v (Add m n)
VNil ++++ b = b
(VCons x xs) ++++ b = VCons x $ xs ++++ b

On Thu, Nov 16, 2017 at 11:21 AM, Quentin Liu
<quentin.liu.0415 at gmail.com> wrote:
> 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/
>
>
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>