[Haskell-beginners] Programming with Singletons

Fri Nov 17 02:08:15 UTC 2017

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 <quentin.liu.0415 at gmail.com>
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 <mukeshtiwari.iiitm at gmail.com>,
> 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
> <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
>
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
>
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/beginners/attachments/20171117/a89ab021/attachment-0001.html>