[Haskell-beginners] Programming with Singletons

Fri Nov 17 08:06:36 UTC 2017

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 <mukeshtiwari.iiitm at gmail.com
> 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 <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-pr
>> ogramming-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/bbf6f91c/attachment.html>