is this a type lits/nats bug or my incorrect understanding ?

Iavor Diatchki iavor.diatchki at gmail.com
Tue Aug 28 17:27:23 CEST 2012


Hello,

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!).
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 '<='.
Both of these should work on the 'type-nats' branch though.

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.

Hope this helps, and happy hacking!
-Iavor



On Thu, Aug 23, 2012 at 9:41 PM, Carter Schonwald <
carter.schonwald at gmail.com> wrote:

> Hello,
>
> 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
> "absolute different of two natural numbers"
>
> 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)
>
>
>  here's the gist for the misleading type error version
> (it seems to indicate that SingI arity 2, rather than arity 1)
> https://gist.github.com/3445419
>
> heres the gist for the version that type checks in a useless way!
> and complains that it doesn't understand that (1<=2)
> https://gist.github.com/3445456
>
> are these bugs in type nats, or am I missing something?
>
> thanks!
> Carter Schonwald
>
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120828/3ba5fa19/attachment.htm>


More information about the Glasgow-haskell-users mailing list