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)

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

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