headers
Carter Schonwald | 24 Aug 2012 06:41
Picon
Gravatar

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

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)

heres the gist for the version that type checks in a useless way!
and complains that it doesn't understand that (1<=2)

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
Permalink | Reply |
headers
Iavor Diatchki | 28 Aug 2012 17:27
Picon
Gravatar

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

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)

heres the gist for the version that type checks in a useless way!
and complains that it doesn't understand that (1<=2)

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


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Permalink | Reply |

Gmane