<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;">Hi all,
<div><br /></div>
<div>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. </div>
<div><br /></div>
<div>It uses </div>
<div> data Nat = Zero | Succ Nat<br /></div>
<div><br /></div>
<div> data SNat a where</div>
<div> SZero :: SNat Zero</div>
<div> SSucc :: SNat a -> SNat (Succ a)</div>
<div>to do the encoding. </div>
<div><br /></div>
<div>The vector is defined based on the natural number encoding: </div>
<div> data Vec a n where</div>
<div> VNil :: Vec a Zero</div>
<div> VCons :: a -> Vec a n -> Vec a (Succ n)</div>
<div><br /></div>
<div><br /></div>
<div>There are some type families declared for manipulating the natural numbers, and one of them that is relevant to the question is </div>
<div> type family (Add (a :: Nat) (b :: Nat)) :: Nat</div>
<div> type instance Add Zero b = b </div>
<div> type instance Add a Zero = a </div>
<div> type instance Add (Succ a) (Succ b) = Succ (Succ (Add a b))</div>
<div>where the `Add` function adds natural numbers. </div>
<div><br /></div>
<div>The problem I am stuck with is the concatenation of two vectors: </div>
<div> (++) :: Vec v m -> Vec v n -> Vec v (Add m n)</div>
<div> VNil ++ b = b</div>
<div> (VCons x xs) ++ b = VCons x $ xs ++ b</div>
<div><br /></div>
<div>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 </div>
<div><br /></div>
<div><br /></div>
<div>Warm Regards, </div>
<div>Qingbo Liu</div>
<div><br /></div>
<div>[1] <a href="https://www.codewars.com/kata/singletons/train/haskell">https://www.codewars.com/kata/singletons/train/haskell</a></div>
<div>[2] <a href="https://byorgey.wordpress.com/2010/07/06/typed-type-level-programming-in-haskell-part-ii-type-families/">https://byorgey.wordpress.com/2010/07/06/typed-type-level-programming-in-haskell-part-ii-type-families/</a></div>
</div>
<div name="messageReplySection" style="font-size: 14px; font-family: -apple-system, BlinkMacSystemFont, sans-serif;"><br /></div>
</body>
</html>