#4385: Type-level natural numbers
----------------------------------------+-----------------------------------
Reporter: diatchki | Owner: diatchki
Type: feature request | Status: new
Priority: normal | Milestone: 7.4.1
Component: Compiler (Type checker) | Version:
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
----------------------------------------+-----------------------------------
Comment(by jeltsch):
Replying to [comment:40 jhenahan]:
> Replying to [comment:39 jeltsch]:
> > Would it be possible to name the new kind {{{Natural}}} instead of
{{{Nat}}}? That way, the naming would be consistent with the naming of
integer types, where {{{Int}}} only refers to a subset of the integers,
while {{{Integer}}} refers to the complete set.
>
> Cf. Agda.
Hmm, the type of natural numbers is called ℕ in Agda. Well, the module
it’s defined in is called {{{Data.Nat}}}. But why should Haskell be
consistent with Agda, but not consistent with itself?
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4385#comment:41>
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
