Re: [Haskell-beginners] Programming with Singletons

Thank you so much! Indeed changing the definition of `Add` helps solve the problem. Following this idea, I changed the definition of `Minus` and `Min` also. Now they are defined as

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

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

The change, however, breaks the `tail` and `drop` function.

drop :: SNat a -> Vec s b -> Vec s (Sub b a) drop SZero     vcons        = vcons drop (SSucc a) (VCons x xs) = drop a xs

tail :: ((Zero :< a) ~ True) => Vec s a -> Vec s (Sub a (Succ Zero)) tail (VCons x xs) = xs

So why does the code break and what would be the solution? The error message seems to confirm that even right now GHD still does not support type expansion. Regards, Qingbo Liu On Nov 15, 2017, 19:51 -0500, mukesh tiwari , wrote:

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 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-has...

_______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners