Hello,<div><br></div><div>the functions on type literals on the master branch are not yet implemented. If you want to play around with these kinds of things, please use the "type-nats" branch (please note that this is a development branch so things may occasionally break!).</div>
<div>In the first example, GHC is saying that it can't solve "SingI (d :: Nat)", which is because the master branch cannot see that "d" must be 1. Similarly, in the second one it does not know about '<='.
</div><div>Both of these should work on the 'type-nats' branch though.
</div><div><br></div><div>The confusing arity issue in the first example is because of kind a polymorphism---SingI has one kind argument (e.g., Nat) and one type argument. (e.g., d) but---at present---GHC renders these in the same way.</div>
<div><br></div><div>Hope this helps, and happy hacking!</div><div>-Iavor</div><div> </div><div><br><br><div class="gmail_quote">On Thu, Aug 23, 2012 at 9:41 PM, Carter Schonwald <span dir="ltr"><<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello, <div><br></div><div>I'm trying to understand how much i can build on top of type literals, so as an exercise, i've been trying to see if I can define a type level</div>
<div>"absolute different of two natural numbers"</div>
<div><br></div><div>i have a minimal example that either type checks in a useless way, or gives a misleading type errors! (or perhaps i am fundamentally not understanding someting)</div><div><br></div><div><br></div><div>
here's the gist for the misleading type error version </div><div>(it seems to indicate that SingI arity 2, rather than arity 1)</div><div><a href="https://gist.github.com/3445419" target="_blank">https://gist.github.com/3445419</a></div>
<div><br></div><div>heres the gist for the version that type checks in a useless way!</div><div>and complains that it doesn't understand that (1<=2)</div><div><a href="https://gist.github.com/3445456" target="_blank">https://gist.github.com/3445456</a></div>
<div><br></div><div>are these bugs in type nats, or am I missing something?</div><div><br></div><div>thanks!</div><span class="HOEnZb"><font color="#888888"><div>Carter Schonwald</div><div><br></div><div><br></div>
</font></span><br>_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><br>
<br></blockquote></div><br></div>