<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title></title>
</head>
<body>
<div name="messageBodySection" style="font-size: 14px; font-family: -apple-system, BlinkMacSystemFont, sans-serif;">Thank you so much! Indeed changing the definition of `Add` helps solve the problem.
<div><br /></div>
<div>Following this idea, I changed the definition of `Minus` and `Min` also. Now they are defined as </div>
<div><br /></div>
<blockquote style="margin: 5px 5px; padding-left: 10px; border-left: thin solid #1abc9c;">
<div>
<div>type family (Sub (a :: Nat) (b :: Nat)) :: Nat </div>
type instance Sub (Succ a) Zero = Succ a <br />
type instance Sub Zero b = Zero<br />
type instance Sub (Succ a) (Succ b) = Sub a b<br />
<br />
type family (Min (a :: Nat) (b :: Nat)) :: Nat <br />
type instance Min Zero Zero = Zero<br />
type instance Min Zero (Succ b) = Zero<br />
type instance Min (Succ a) Zero = Zero<br />
type instance Min (Succ a) (Succ b) = Succ (Min a b)</div>
</blockquote>
<div><br /></div>
<div>The change, however, breaks the `tail` and `drop` function.</div>
<div><br /></div>
<blockquote style="margin: 5px 5px; padding-left: 10px; border-left: thin solid #1abc9c;">
<div>
<div>drop :: SNat a -> Vec s b -> Vec s (Sub b a)</div>
<div>drop SZero vcons = vcons</div>
<div>drop (SSucc a) (VCons x xs) = drop a xs </div>
</div>
<div><br /></div>
<div>
<div>tail :: ((Zero :< a) ~ True) => Vec s a -> Vec s (Sub a (Succ Zero))</div>
<div>tail (VCons x xs) = xs</div>
</div>
</blockquote>
<div><br /></div>
<div>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. </div>
</div>
<div name="messageSignatureSection" style="font-size: 14px; font-family: -apple-system, BlinkMacSystemFont, sans-serif;"><br />
Regards,
<div>Qingbo Liu</div>
</div>
<div name="messageReplySection" style="font-size: 14px; font-family: -apple-system, BlinkMacSystemFont, sans-serif;"><br />
On Nov 15, 2017, 19:51 -0500, mukesh tiwari <mukeshtiwari.iiitm@gmail.com>, wrote:<br />
<blockquote type="cite" style="margin: 5px 5px; padding-left: 10px; border-left: thin solid #1abc9c;">Hi Quentin,<br />
I changed your pattern little bit in Add function and it is working<br />
fine. I think the problem was that type of (VCons x xs) ++++ b is Vec<br />
v (Add (Succ m1) + n) which was not present in your<br />
Add function pattern.<br />
<br />
<br />
<br />
{-# LANGUAGE TypeFamilies #-}<br />
{-# LANGUAGE DataKinds #-}<br />
{-# LANGUAGE KindSignatures #-}<br />
{-# LANGUAGE GADTs #-}<br />
{-# LANGUAGE InstanceSigs #-}<br />
module Tmp where<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
data SNat a where<br />
SZero :: SNat Zero<br />
SSucc :: SNat a -> SNat (Succ a)<br />
<br />
data Vec a n where<br />
VNil :: Vec a Zero<br />
VCons :: a -> Vec a n -> Vec a (Succ n)<br />
<br />
type family (Add (a :: Nat) (b :: Nat)) :: Nat<br />
type instance Add Zero b = b<br />
type instance Add (Succ a) b = Succ (Add a b)<br />
<br />
(++++) :: Vec v m -> Vec v n -> Vec v (Add m n)<br />
VNil ++++ b = b<br />
(VCons x xs) ++++ b = VCons x $ xs ++++ b<br />
<br />
On Thu, Nov 16, 2017 at 11:21 AM, Quentin Liu<br />
<quentin.liu.0415@gmail.com> wrote:<br />
<blockquote type="cite" style="margin: 5px 5px; padding-left: 10px; border-left: thin solid #e67e22;">Hi all,<br />
<br />
I was doing the “Singletons” problem at codewars[1]. The basic idea is to<br />
use dependent types to encode the length of the vector in types.<br />
<br />
It uses<br />
data Nat = Zero | Succ Nat<br />
<br />
data SNat a where<br />
SZero :: SNat Zero<br />
SSucc :: SNat a -> SNat (Succ a)<br />
to do the encoding.<br />
<br />
The vector is defined based on the natural number encoding:<br />
data Vec a n where<br />
VNil :: Vec a Zero<br />
VCons :: a -> Vec a n -> Vec a (Succ n)<br />
<br />
<br />
There are some type families declared for manipulating the natural numbers,<br />
and one of them that is relevant to the question is<br />
type family (Add (a :: Nat) (b :: Nat)) :: Nat<br />
type instance Add Zero b = b<br />
type instance Add a Zero = a<br />
type instance Add (Succ a) (Succ b) = Succ (Succ (Add a b))<br />
where the `Add` function adds natural numbers.<br />
<br />
The problem I am stuck with is the concatenation of two vectors:<br />
(++) :: Vec v m -> Vec v n -> Vec v (Add m n)<br />
VNil ++ b = b<br />
(VCons x xs) ++ b = VCons x $ xs ++ b<br />
<br />
The program would not compile because the compiler found that `VCons x $ xs<br />
++ b`gives type `Vec v (Succ (Add n1 n))`, which does not follow the<br />
declared type `Vec v (Add m n)`. Is it because ghc does not expand `Add m n’<br />
that the type does not match? I read Brent Yorgey’s blog on type-level<br />
programming[2] and he mentioned that would not automatically expand types.<br />
But the posted time of the blog is 2010 and I am wondering if there is any<br />
improvement to the situation since then? Besides, what would be the solution<br />
to this problem<br />
<br />
<br />
Warm Regards,<br />
Qingbo Liu<br />
<br />
[1] https://www.codewars.com/kata/singletons/train/haskell<br />
[2]<br />
https://byorgey.wordpress.com/2010/07/06/typed-type-level-programming-in-haskell-part-ii-type-families/<br />
<br />
<br />
_______________________________________________<br />
Beginners mailing list<br />
Beginners@haskell.org<br />
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners<br />
<br /></blockquote>
_______________________________________________<br />
Beginners mailing list<br />
Beginners@haskell.org<br />
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners<br /></blockquote>
</div>
</body>
</html>