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