<div dir="ltr">Hi Gabor,<div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jan 3, 2014 at 9:33 AM, Gabor Greif <span dir="ltr"><<a href="mailto:ggreif@gmail.com" target="_blank">ggreif@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">Hi devs,<br>
<br>
with recent iterations of GHC.TypeLits (HEAD) I am struggling to get<br>
something simple working. I have<br>
<br>
> data Number nat = KnownNat nat => Number !(Proxy nat)<br>
<br>
and want to write<br>
<br>
> addNumbers :: Number a -> Number b -> Maybe (Number (a + b))<br>
<br>
Unfortunately I cannot find a way to create the necessary KnownNat (a<br>
+ b) constraint.<br>
<br></blockquote><div> </div><div>Indeed, there is no way to construct `KnownNumber (a + b)` from `(Known a, Known b)`. This is not something that we lost, it was just never implemented.  We could make something like it work, I think, but it'd make things a bit more complex: the representation of `KnownNumber` dictionaries would have to be expressions, rather than a simple constant.</div>
<div><br></div><div>I'd be inclined to leave this as is for now---let's see what we can do with the current system, before we add more functionality.</div><div><br></div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">

Declaring the function thus<br>
<br>
> addNumbers :: KnownNat (a + b) => Number a -> Number b -> Maybe (Number (a + b))<br>
<br>
only dodges the problem around.<br></blockquote><div><br></div><div>Dodging problems is good! :-)  I don't fully understand from the type what the function is supposed to do, but I'd write something like this:</div>
<div><br></div><div><font face="courier new, monospace">addNumbers :: (KnownNat a, KnownNat b)</font></div><div><font face="courier new, monospace">           => (Integer -> Integer -> Bool) -- ^ Some constraint?</font></div>
<div><font face="courier new, monospace">              Proxy a -> Proxy b -> Maybe (Proxy (a + b))</font></div><div><font face="courier new, monospace">addNumber p x y =</font></div><div><font face="courier new, monospace">  do guard (p (natVal x) (natVal y))</font></div>
<div><font face="courier new, monospace">     return Proxy</font></div><div><br></div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">

<br>
Also I am wondering where the ability to perform a type equality check<br>
went. I.e. I cannot find the relevant functionality to obtain<br>
<br>
> sameNumber :: Number a -> Number b -> Maybe (a :~: b)<br>
<br>
I guess there should be some TestEquality instance (for Proxy Nat?, is<br>
this possible at all), but I cannot find it. Same applies for Symbols.<br>
<br>
</blockquote><div><br></div><div>Ah yes, I thought that this was supposed to be added to some other library, but I guess that never happened.  It was implemented like this, if you need it right now.</div><div><br></div><div>
<div><font face="courier new, monospace">sameNumber :: (KnownNat a, KnownNat b)</font></div><div><font face="courier new, monospace">           => Proxy a -> Proxy b -> Maybe (a :~: b)</font></div><div><font face="courier new, monospace">sameNumber x y </font></div>
<div><font face="courier new, monospace">  | natVal x == natVal y = Just (unsafeCoerce Refl)</font></div><div><font face="courier new, monospace">  | otherwise            = Nothing</font></div></div><div><br></div><div>This doesn't fit the pattern for the `TestEquality` class (due to the constraints on the parameters), so perhaps I'll add it back to GHC.TypeLits.</div>
<div><br></div><div>-Iavor</div><div><br></div><div><br></div><div><br></div></div></div></div>