<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;">Thanks a lot!
<div><br /></div>
<div>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?</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 17, 2017, 03:15 -0500, mukesh tiwari <mukeshtiwari.iiitm@gmail.com>, wrote:<br />
<blockquote type="cite" style="margin: 5px 5px; padding-left: 10px; border-left: thin solid #1abc9c;">
<div dir="ltr">Disregard my previous mail, because I realized that your Sub is correct except (Succ a). Sorry for the confusion. New definition below<br />
<br />
type family (Sub (a :: Nat) (b :: Nat)) :: Nat<br />
type instance Sub a Zero = a<br />
type instance Sub Zero b = Zero<br />
type instance Sub (Succ a) (Succ b) = Sub a b<br />
<br /></div>
<div class="gmail_extra"><br />
<div class="gmail_quote">On Fri, Nov 17, 2017 at 1:08 PM, mukesh tiwari <span dir="ltr"><<a href="mailto:mukeshtiwari.iiitm@gmail.com" target="_blank">mukeshtiwari.iiitm@gmail.com</a>></span> wrote:<br />
<blockquote class="gmail_quote" style="margin: 5px 5px; padding-left: 10px; border-left: thin solid #e67e22;">
<div dir="ltr">
<div>
<div>Changed your Sub code to this and drop works now. You drop function<br />
drop SZero vcons = vcons so you are returning the second vector if first one is empty (length Zero).<span class=""><br />
<br />
<br />
type family (Sub (a :: Nat) (b :: Nat)) :: Nat<br /></span>type instance Sub a Zero = a<br />
type instance Sub Zero b = b<span class=""><br />
type instance Sub (Succ a) (Succ b) = Sub a b<br />
<br /></span>No use of Min in your code, but I changed it anyway.<span class=""><br />
<br />
type family (Min (a :: Nat) (b :: Nat)) :: Nat<br /></span>type instance Min Zero b = Zero<br />
type instance Min a Zero = Zero<span class=""><br />
type instance Min (Succ a) (Succ b) = Succ (Min a b)<br />
<br /></span>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.<br />
I am getting <b>Not in scope: type constructor or class ‘:<’<br />
<br /></b></div>
</div>
</div>
<div class="HOEnZb">
<div class="h5">
<div class="gmail_extra"><br />
<div class="gmail_quote">On Fri, Nov 17, 2017 at 12:01 PM, Quentin Liu <span dir="ltr"><<a href="mailto:quentin.liu.0415@gmail.com" target="_blank">quentin.liu.0415@gmail.com</a>></span> wrote:<br />
<blockquote class="gmail_quote" style="margin: 5px 5px; padding-left: 10px; border-left: thin solid #3498db;">
<div>
<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 #d35400;">
<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 #d35400;">
<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>
<div class="m_1436017000147736697h5">
<div name="messageReplySection" style="font-size:14px;font-family:-apple-system,BlinkMacSystemFont,sans-serif"><br />
On Nov 15, 2017, 19:51 -0500, mukesh tiwari <<a href="mailto:mukeshtiwari.iiitm@gmail.com" target="_blank">mukeshtiwari.iiitm@gmail.com</a>><wbr />, wrote:<br />
<blockquote type="cite" style="margin: 5px 5px; padding-left: 10px; border-left: thin solid #d35400;">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 />
<<a href="mailto:quentin.liu.0415@gmail.com" target="_blank">quentin.liu.0415@gmail.com</a>> wrote:<br />
<blockquote type="cite" style="margin: 5px 5px; padding-left: 10px; border-left: thin solid #34495e;">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] <a href="https://www.codewars.com/kata/singletons/train/haskell" target="_blank">https://www.codewars.com/kata/<wbr />singletons/train/haskell</a><br />
[2]<br />
<a href="https://byorgey.wordpress.com/2010/07/06/typed-type-level-programming-in-haskell-part-ii-type-families/" target="_blank">https://byorgey.wordpress.com/<wbr />2010/07/06/typed-type-level-pr<wbr />ogramming-in-haskell-part-ii-<wbr />type-families/</a><br />
<br />
<br />
______________________________<wbr />_________________<br />
Beginners mailing list<br />
<a href="mailto:Beginners@haskell.org" target="_blank">Beginners@haskell.org</a><br />
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners" target="_blank">http://mail.haskell.org/cgi-bi<wbr />n/mailman/listinfo/beginners</a><br />
<br /></blockquote>
______________________________<wbr />_________________<br />
Beginners mailing list<br />
<a href="mailto:Beginners@haskell.org" target="_blank">Beginners@haskell.org</a><br />
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners" target="_blank">http://mail.haskell.org/cgi-bi<wbr />n/mailman/listinfo/beginners</a><br /></blockquote>
</div>
</div>
</div>
</div>
<br />
______________________________<wbr />_________________<br />
Beginners mailing list<br />
<a href="mailto:Beginners@haskell.org" target="_blank">Beginners@haskell.org</a><br />
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bi<wbr />n/mailman/listinfo/beginners</a><br />
<br /></blockquote>
</div>
<br /></div>
</div>
</div>
</blockquote>
</div>
<br /></div>
_______________________________________________<br />
Beginners mailing list<br />
Beginners@haskell.org<br />
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners<br /></blockquote>
</div>
</body>
</html>