Recursion on TypeNats

[Richard Eisenberg]

I don't think we'll need notation to differentiate: just use overloaded literals, like we do in terms. Something that would operate vaguely like this:

> type family 3 :: k where
>   3 :: Nat = ... -- 3 as a Nat
>   3 :: Integer = ... -- 3 as an Integer

I'm not at all suggesting it be implemented this way, but we already have the ability to branch in type families based on result kind, so the mechanism is already around. Unfortunately, this would be unhelpful if the user asked for (3 :: Bool), which would kind-check but be stuck.

Richard

On Oct 28, 2014, at 8:24 PM, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:

> Hello,
> 
> actually type-level integers are easier to work with than type-level naturals (e.g., one can cancel things by subtracting at will).   I agree that ideally we want to have both integers and naturals (probably as separate kinds).  I just don't know what notation to use to distinguish the two. 
> 
> -Iavor
> 
> 
> 
> On Mon, Oct 27, 2014 at 2:13 PM, Barney Hilken <b.hilken at ntlworld.com> wrote:
> Ok, I've created a ticket https://ghc.haskell.org/trac/ghc/ticket/9731
> 
> Unfortunately I don't know enough about ghc internals to try implementing it.
> 
> _______________________________________________
> 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/20141029/bd07228d/attachment.html>