Programming with Singletons

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

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



_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: 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
<[hidden email]> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Programming with Singletons

Quentin Liu
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 <[hidden email]>, 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
<[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Programming with Singletons

mukesh tiwari
Changed your Sub code to this and drop works now.  You drop function
drop SZero     vcons        = vcons  so you are returning the second vector if first one is empty (length Zero).


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

No use of Min in your code, but I changed it anyway.

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

I am not able to compile your tail code, so could you please paste your whole code github, or any preferred link which you like.
I am getting  Not in scope: type constructor or class ‘:<’


On Fri, Nov 17, 2017 at 12:01 PM, Quentin Liu <[hidden email]> wrote:
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 <[hidden email]>, 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
<[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners



_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Programming with Singletons

mukesh tiwari
Disregard my previous mail, because I realized that your Sub is correct except (Succ a). Sorry for the confusion. New definition below

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


On Fri, Nov 17, 2017 at 1:08 PM, mukesh tiwari <[hidden email]> wrote:
Changed your Sub code to this and drop works now.  You drop function
drop SZero     vcons        = vcons  so you are returning the second vector if first one is empty (length Zero).


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

No use of Min in your code, but I changed it anyway.

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

I am not able to compile your tail code, so could you please paste your whole code github, or any preferred link which you like.
I am getting  Not in scope: type constructor or class ‘:<’


On Fri, Nov 17, 2017 at 12:01 PM, Quentin Liu <[hidden email]> wrote:
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 <[hidden email]>, 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
<[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners




_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Programming with Singletons

Quentin Liu
Thanks a lot! 

Conceptually pattern matching against (Succ a) and then returning (Succ a) is equivalent to directly matching against a, but why is the compiler unable to recognize this?

Regards, 
Qingbo Liu 

On Nov 17, 2017, 03:15 -0500, mukesh tiwari <[hidden email]>, wrote:
Disregard my previous mail, because I realized that your Sub is correct except (Succ a). Sorry for the confusion. New definition below

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


On Fri, Nov 17, 2017 at 1:08 PM, mukesh tiwari <[hidden email]> wrote:
Changed your Sub code to this and drop works now.  You drop function
drop SZero     vcons        = vcons  so you are returning the second vector if first one is empty (length Zero).


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

No use of Min in your code, but I changed it anyway.

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

I am not able to compile your tail code, so could you please paste your whole code github, or any preferred link which you like.
I am getting  Not in scope: type constructor or class ‘:<’


On Fri, Nov 17, 2017 at 12:01 PM, Quentin Liu <[hidden email]> wrote:
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 <[hidden email]>, 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
<[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners



_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners