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.diatc...@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.hil...@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@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
