<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).<br><br><br>type family (Sub (a :: Nat) (b :: Nat)) :: Nat<br>type instance Sub a Zero = a<br>type instance Sub Zero     b = b<br>type instance Sub (Succ a) (Succ b) = Sub a b<br><br>No use of Min in your code, but I changed it anyway.<br><br>type family (Min (a :: Nat) (b :: Nat)) :: Nat<br>type instance Min Zero b = Zero<br>type instance Min a Zero = Zero<br>type instance Min (Succ a) (Succ b) = Succ (Min a b)<br><br>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><b></b></div></div></div><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:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">



<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 #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><div class="h5">
<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 #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>
<<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 #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] <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-<wbr>programming-in-haskell-part-<wbr>ii-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-<wbr>bin/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-<wbr>bin/mailman/listinfo/beginners</a><br></blockquote>
</div>
</div></div></div>

<br>______________________________<wbr>_________________<br>
Beginners mailing list<br>
<a href="mailto:Beginners@haskell.org">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-<wbr>bin/mailman/listinfo/beginners</a><br>
<br></blockquote></div><br></div>