#4385: Type-level natural numbers
----------------------------------------+-----------------------------------
Reporter: diatchki | Owner: diatchki
Type: feature request | Status: new
Priority: normal | Milestone: 7.2.1
Component: Compiler (Type checker) | Version:
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
----------------------------------------+-----------------------------------
Comment(by simonpj):
Great stuff. Here are some design issues I'd like to discuss. Probably
email and your wiki is the place to discuss. (We can't edit your wiki...
I wonder if you might use the GHC Trac Wiki instead?). But laying out the
points for discussion here seems good:
* I really, really want to make operators into type '''constructors'''
rather than (as at present) type '''variables'''. So that we can write a
type `(a + b)` rather than `(a :+ b)`. See
http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors.
Doing this is, I think, straightforward, but it still needs doing.
* I found `integerToNat` hard to grok. Could we use an existential
instead?
{{{
data DynNat where
DN :: forall (n::Nat). Nat n -> DynNat
integerToNat :: Integer -> DynNat
}}}
Of course it's equivalent, but still.
* We need to think systematically about syntax. You have
* A kind `Nat`
* A type `Nat :: Nat -> *`.
* A type class `TypeNat`
And that's without thinking about a type-level equivalent of the kind
`Nat`. At the type level we have `2 :: Nat`. It's be much nicer if at
the term level we also had `2 :: Nat` (via the Num type class). But then
the singleton type would have to be something different, `Nat1`, or
`SingleNat`, or `Single`...?
The SHE notation (http://personal.cis.strath.ac.uk/~conor/pub/she/) uses
the "braces of upward mobility" to promote values to types, and types to
kinds. I wonder if we could use that somehow.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4385#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
