Re: [GHC] #4385: Type-level natural numbers
#4385: Type-level natural numbers +--- Reporter: diatchki | Owner: diatchki Type: feature request | Status: new Priority: normal | Milestone: 7.6.2 Component: Compiler (Type checker) | Version: Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: |Testcase: Blockedby: |Blocking: Related: | +--- Changes (by hvr): * cc: hvr@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:56 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#4385: Type-level natural numbers +--- Reporter: diatchki | Owner: diatchki Type: feature request | Status: new Priority: normal | Milestone: 7.6.1 Component: Compiler (Type checker) | Version: Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: |Testcase: Blockedby: |Blocking: Related: | +--- Comment(by dmcclean): I notice this is in the 7.6.1 RC without a constraint solver. Is there a plan to implement the constraint solver for 7.6.1? If not, it might make sense to delay implementing this at all until the solver can be implemented, to retain more flexibility for making any changes that might be informed by the solver work. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:52 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#4385: Type-level natural numbers +--- Reporter: diatchki | Owner: diatchki Type: feature request | Status: new Priority: normal | Milestone: 7.6.1 Component: Compiler (Type checker) | Version: Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: |Testcase: Blockedby: |Blocking: Related: | +--- Changes (by dmcclean): * cc: douglas.mcclean@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:53 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: |Testcase: Blockedby: |Blocking: Related: | +--- Comment(by diatchki): Hello, work on the type nats is still in progress, support for type nat literlas, generalized type type-level operators, and type-level string literals is available in the type-nats branch of GHC. There used to be a solver for type-level functions on nats as well, but it is dibaled for the moment. The current task is to decide how to integrate the evidence generated by the solver with the evidence that GHC uses. I've been a bit busy with work lately, but I am hoping to restart hacking on the solver integration in the next few weeks. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:49 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: |Testcase: Blockedby: |Blocking: Related: | +--- Comment(by bjornbm): It seems this ticket needs an update by someone in the know. I understand TypeNats didn't make it into 7.4.1 in the end so at least the milestone is inaccurate(?). Can we still expect to see TypeNats in GHC? -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:48 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by nathanhowell): * cc: nathanhowell@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:47 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by acfoltzer): * cc: acfoltzer@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:46 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by reinerp): * cc: reiner.pope@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:45 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 sjoerd_visscher): Instead of (i ~ IntType Negative 2) you get (i ~ IntType n (n + 2)). -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:44 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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
+---
Changes (by jhenahan):
* cc: jhenahan@… (added)
Comment:
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.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:40
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 sjoerd_visscher):
Replying to [comment:38 dankna]:
So that would work, except as far as I can tell, the obvious way to
define type-level integers in terms of type-level naturals isn't possible.
Have you tried defining type-level integer in terms of 2 type-level
naturals, the value being the difference between the 2 naturals:
{{{
data IntType :: Nat - Nat - *
type family Minus a b
type instance Minus (IntType a b) (IntType c d) = IntType (a + d) (b + c)
}}}
The type for f.e. -2 would then be `forall n. IntType n (n + 2)`.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:42
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 dankna): I haven't tried that, no, but I don't see how it could work - surely that loses the very nice property that type equality corresponds to numeric equality? -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:43 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 dankna):
So I've been playing around with this the past couple days. I have picked
a different toy project than everybody else's; instead of sized arrays,
I'm doing dimensioned quantities. So for example I want to be able to
have types Quantity Kilo Watt Int and Quantity Mega Second Int and know
that the product of them is Quantity Giga Joule Int. To do this I am
having one type-level int (not nat) for each of the seven SI fundamental
units length, time, etc, representing the power to which that unit is
present. So velocity would have length to power 1 and time to power -1,
and everything else to power 0. This unfortunately does not encompass
currencies, but oh well.
So that would work, except as far as I can tell, the obvious way to define
type-level integers in terms of type-level naturals isn't possible.
Here's what I'm doing:
{{{
data IntType :: * - Nat - *
data Negative
data NonNegative
class IntClass int
instance IntClass (IntType NonNegative num)
instance (1 = num) = IntClass (IntType Negative num)
}}}
So far so good, except there's no way to write a type function PlusInt. I
eventually realized that I could reduce it to writing MinusNat instead,
which makes for a clearer explanation of why it isn't possible, so that's
the example I'll give here:
{{{
type family MinusNat a b
type instance MinusNat (ab ~ a + b) b = a
}}}
or alternatively
{{{
type family MinusNat a b
type instance (ab ~ a + b) = MinusNat ab b = a
}}}
But of course neither is possible, because neither type-synonym instances
nor type contexts can be used like that. I puzzled over why that was for
a moment before people in #haskell pointed out to me that it would require
GHC to read the number's mind, effectively.
Anyway, I can think of two ways to remedy this. The more invasive way
would be to add a solver that can actually do that. The less invasive way
would be to add a kind Int which is a superkind of Nat and has minus
built-in. But I don't like that approach as much because it wouldn't let
people implement division or logarithms.
I don't know what you refer to with the evidence system above, because I
don't understand the internals of the typechecker. I'm willing to write
some code to make this happen, but I need to discuss the design first. So
I'm writing this post attached to the ticket so that everyone interested
can respond. I may also direct people in #ghc to this tomorrow morning,
but I don't know how much time they'll have to spare.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:38
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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):
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.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:39
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by Favonia): * cc: favonia@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:37 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by dankna): * cc: dankna@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:36 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by PHO): * cc: pho@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:35 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by FSalad): * cc: danlex@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:34 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by illissius): * cc: illissius@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:33 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by bjornbm): * cc: bjornbm (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:32 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 jeltsch): Replying to [comment:3 simonpj]: 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. Really nice. What GHC version can be expected to have this feature? I’d like to use it. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:31 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by ChristiaanBaaij): * cc: christiaan.baaij@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:29 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by Lemming): * cc: ghc@… (added) Comment: The llvm package highly needs something that is faster than the type level arithmetic provided by type-level. Currently compiling llvm related code can require several seconds due to the involved vector size computations. I am still curious what comes next after type level naturals. :-) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:30 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by djahandarie): * cc: djahandarie@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:28 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by jweijers): * cc: jeroen.weijers@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by conal): * cc: conal@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by basvandijk): * cc: v.dijk.bas@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by helgikrs): * cc: helgikrs@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by nwn): * cc: nonowarn@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by lerkok): * cc: erkokl@… (added) Comment: Let me briefly chime in an express great interest in this project. Iavor has been able to pull in the sbv package (http://hackage.haskell.org/package/sbv) and make it work with his type- naturals, and it looks much cleaner and usable. Great work, looking forward to the official release. (And sbv will be an early adapter of this feature as a non-trivial application of it.) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 diatchki):
Hello,
I added some support for associativity over the weekend, and now the (+++)
example works (I've pushed the changes to the git repo).
On the pattern matching issue: I also thought that using the unary
representation might be clunky, but I played around with it this weekend,
and I kind of like it. It leads to fairly natural looking definitions of
simple inductive functions, and I don't think that it is even that
inefficient---the unary number is lazily generated so it essentially
corresponds to a sequence of checks on the real integer. Here is the code
I played around with:
http://hackage.haskell.org/trac/ghc/wiki/TypeNats/InductiveDefinitions
We might even be able to add a fold to deforest the intermediate Zero
and Succ constructors.
(Previously, I was thinking that we should use type classes to do this
sort of thing, but GHC does not like type functions in instance heads, and
also we'd had to let it know that (x + 1) does not overlap with 0, etc.,
so overall this seems more complex.)
Finally a general note :-) I also think that this sort of fake dependent
types / GADT programs are neat and useful but I wouldn't want to raise
expectations too much because we really are pushing at the edges of
Haskell's type system here---these simple examples use a lot of machinery
(qualified types, type functions, GADTs, polymorphic recursion).
Another useful technique is to use type-level naturals as phantom types
to provide safe library wrappers to unsafe primitives. This is a sort of
intermediate step between the current state of Haskell and the dependent
type/GADT world because it provides safety to the users of the library but
only as long as the library is written correctly (i.e., the types do not
help the library writer, but they help the library user). Here is an
example of the technique:
{{{
newtype Vec (n :: Nat) a = Vec [a]
empty :: Vec 0 a
empty = Vec []
mapVec :: (a - b) - Vec n a - Vec n b
mapVec f (Vec xs) = Vec (map f xs)
catVec :: Vec m a - Vec n a - Vec (m + n) a
catVec (Vec xs) (Vec ys) = Vec (xs ++ ys)
-- etc..
}}}
Note that here the types express the library writer's intention, but they
do not enforce the correctness of the implementation. The benefit is that
there are no complicated constraints to solve. Of course, constraints
will arise when we use the library, but as long as the use is at concrete
types, then the constraints would be easy to solve.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:21
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 adamgundry):
Nice work! It's good to see some progress in this direction.
We should certainly think about how users can provide more information to
the constraint solver, either as explicit proofs or perhaps hints about
useful lemmas to guide the search process. I'm not convinced that changing
or removing type signatures on the whim of the compiler is a good
strategy. (Can we even infer types properly for these things?)
I have been experimenting with the version of 9th January (while I try to
figure out how to check out and build a more up to date version), so
apologies if the following is a bit out of date. Perhaps I'm missing
something, but I can't make the following classic example work:
{{{
data Vec :: Nat - * - * where
Nil :: Vec 0 a
(:) :: a - Vec n a - Vec (n+1) a
(+++) :: Vec n a - Vec m a - Vec (n+m) a
Nil +++ bs = bs
(a : as) +++ bs = a : (as +++ bs)
}}}
In the last line, the solver fails to deduce ((1 + (n1 + m)) ~ (n + m))
from the context (n ~ (n1 + 1)). One use of unsafeCoerce is enough to get
it accepted, but I can't see how two modify the type signature to make
this go through. My point is not so much that this example fails, as the
solver could presumably be extended to make it work, but that in general
such problems will occur.
My perspective is from working with dependent types and inductive families
(GADTs). I think that a lot of the interest in type-level numbers comes
from their use along with GADTs, as pumpkin's example indicates, so we
need to figure out how the interaction between the two will work.
One final thought: at the moment there doesn't seem to be any way to
pattern match on numbers, at least without using natToInteger and so
discarding statically-known information. For example, the Applicative
functor instance for vectors includes
{{{
pure :: Nat n - a - Vec n a
}}}
which makes a vector full of a single value. At the moment, the
implementation by pattern-matching and recursion on the first argument
doesn't seem to be possible in a type-safe way. One can add a unary
representation of numbers indexed by their Nat values inside the TypeNats
module abstraction barrier, but this is a bit clunky and inefficient.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:18
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by sjoerd_visscher): * cc: sjoerd@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by hesselink): * cc: hesselink@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 diatchki):
Hello,
For the moment, there is no support for ad-hoc proofs. The problem you
describe might occur when GHC encounters a type signature but it cannot
show that the context of the type signature is sufficient to justify the
function's implementation. As you say, this may be because GHC does not
know enough math. In this case, one would have to either change (or
remove) the type signature, or change the implementation (and, if the
inference seems obvious, then send an e-mail to the GHC list so that we
can teach GHC some more math :-).
{{{unsafeCoerce}}} works as usual but I've never had to use it because,
usually, there is something different one can do. For example, the array
indexes that you mentioned use type-nats as a phantom type only, so the
library could provide arbitrary coercion functions, including something
based on manual evidence construction, but I have not really thought about
that.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:16
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 pumpkin):
The main application I'm thinking about is REPA right now, which uses a
fairly complex type to describe the shape of multidimensional arrays. The
type is, however, not fully representative of the actual shape of the
array, because we don't have easy type-level naturals. There's also some
confusing overlap between the type-level shape (which mostly encodes the
number of dimensions of the array) and the value-level shape (which
actually contains the dimensions).
Using your typenats and some fancy GADT trickery, the index computations
could be made exact and proved correct at compile time, to avoid any kind
of index checking at runtime, but the computation is non-trivial, and
basically involves proving that if you have a list of dimensions and a
list of indices, then the usual multidimensional flattening computation
preserves the length requirement for the flat underlying array. I was
modeling REPA in Agda a while back and came up with this:
{{{
data Shape : ℕ → Set where
Z : Shape 1
_∷_ : ∀ {n} → (ss : Shape n) → (s : ℕ) → Shape (suc s * n)
data Index : ∀ {n} → Shape n → Set where
Z : Index Z
_∷_ : ∀ {m} {sh : Shape m} {n} → (is : Index sh) → (i : Fin (suc n)) →
Index (sh ∷ n)
flatten : ∀ {n} {sh : Shape n} → Index sh → Fin n
flatten = {- lots more stuff to prove that the flattening computation
preseves the Fin -}
}}}
Although this is dependently typed in Agda, it could be modeled in Haskell
too using GADTs that refine the type index to a typenat multiplication.
When I get the time to compile your repo, I'll try translating this to
Haskell with typenats and see if it can spot the fairly complicated
behavior that I need to prove manually in Agda. I'll be very happy if it
can!
Anyway, it's an exciting development in GHC! Now you just have to fight
off all the proof-freaks like me that it attracts :P
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:17
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by spl): * cc: leather@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 diatchki):
Hello,
since a few people have joined the ticket I thought I'd post an update. I
have been updating the documentation of how things work, and some of the
design/implementation issues that I know of. Take a look here:
http://hackage.haskell.org/trac/ghc/wiki/TypeNats
If you have the time, please try out the current implementation and send
me feedback, I usually try to keep things in a working state. To get the
code:
{{{
git clone git://code.galois.com/type-naturals/ghc.git
}}}
There are two branches in there, my work is on branch type-nats (branch
master tracks the standrad GHC development branch).
As usual, before starting a build you'd need to get the libraries used by
GHC. My work also requires some extra changes to base and template-
haskell which are available in these darcs repos:
{{{
http://code.galois.com/darcs/type-naturals/09-Jan-2011/base
http://code.galois.com/darcs/type-naturals/09-Jan-2011/template-haskell
}}}
Usually, I use {{{darcs-all}}} to get the libraries from
{{{darcs.haskell.org}}}, and then something like this:
{{{
pushd libraries/base
darcs pull http://code.galois.com/darcs/type-naturals/09-Jan-2011/base
popd
pushd libraries/template-haskell
darcs pull http://code.galois.com/darcs/type-naturals/09-Jan-2011
/template-haskell
popd
}}}
Type-level nats are enabled with extensions {{{TypeNaturals}}} (e.g.,
{{{-XTypeNaturals}}}, or pragma {{{LANGUAGE TypeNaturals}}}.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:14
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by thoughtpolice): * cc: as@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by pumpkin): * cc: pumpkingod@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by simonpj): * cc: sweir...@…, dimit...@…, byor...@…, conor.mcbr...@… (added) Comment: Good! My suggestions for progress: * Keep an up-to-date (preferably wiki) description of the users-eye view of the system. You had this before, but it may need updating eg with `DynNat`. * Keep a wiki page, as you suggest, summarising design issues. You already have these, I think, here http://hackage.haskell.org/trac/ghc/wiki/TypeNats, although the division between user manual, design issues, and implemetation notes isn't very clear. Especially important is to summarise open design and implementation issues. Email discussion belongs on cvs-ghc, I guess? Concerning evidence, as soon as I get the new typechecker settled down I'm going to work on the evidence part of FC. In particular, equality evidence is currently treated like types, and erased, in contrast to class evidence which is not erased and is passed at runtime. I have a plan to treat both uniformly, not ''erasing'' equality evidence, but rather treating it as a value like the state token of the state monad. That is, a value that can be passed around in zero bits. This will make everying much nicer and more uniform. Still the question remains of what evidence terms FC should have for numerics. Iavor, if you continue to drive this, I'll be responsive. I'm adding Stephanie, Brent, Conor, Dimitrios to the cc list. Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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): Iavor: what's your plan for this? I'd like to have it in the HEAD, but we need to resolve the design issues first. Also I'm unsure about whether you are actively developing or whether you've moved on to other things. Oh, one other thing that isn't clear to me is how all this fits in FC. If a Pressburger solver shows that (a*b = b*a), say how is that expressed as a FC proof term? Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 diatchki): Hello, I am certainly still working on it, and I think that it'd be great to merge it with HEAD. What would be the best way to work on the design issues---I feel that these ticket comments do not have enough space to discuss things properly. Perhaps I will make a page on the wiki where we (meaning whoever is interested in this feature) can list all the issues and see how to solve them best? I'll update the ticket when I get a chance to do this. Briefly, my current status is: - I've added the syntactic change to treat all symbols as type constructors, and the associated change to the module system. In the process I noticed that GHC does not really use the precedence machinery for infix predicates (classes, ~). Adding support for this is on my TODO list, so that we can write things like `(a + b ~ c)`, rather then `((a + b) ~ c)`. - I've implemented the numeric type literals, which are of a new kind (currently called) Nat. I've added a new form of type `LiteralTy TyLit`, where `TyLit` is a type for type-level literals. Currently, it has only numbers in it but later we could add other things too, if we deemed it useful. - I've added a set of operations on the type numbers, currently: comparison `(=)`, addition `(+)`, multiplication `(*)`, and exponentiation `(^)`. By using equality constraints, we also get their inverses: subtraction, division, logarithms, and roots. My solver is by no means complete although it seems to work for a number of practical examples. I am sure that we can continue to improve it for a long time though. The current implementation cheats on the proofs for the equalities and (=) because it uses unsafeCoercions. At first I had it generate proofs but then you mentioned that you were redoing the evidence mechanism based on Brent's work, and the proofs were getting quite large and difficult to read so I removed them. It would not be hard to re-add them but we should decide on the granularity of the primitive axioms (coercions) to use. The trade-off is basically RISC vs CISC, a smaller set of simpler axioms tends to result in larger proofs. There is also an issue about what evidence to pass for (=). (=) is similar to (~) (and any other class with no methods) in that it does not really need any runtime evidence. I could not see how to adopt the (~) mechanism to account for (=) so, currently, the evidence for (=) is basically a hack (the run-time evidence calls error if it is ever evaluated). It might be nice if we had a unified way to treat things without evidence (e.g., by having a special form of argument that does not emit any run-time code) but I have not looked into how hard would be to do this. Can anyone think of a better way to do this? - In the support library, I made the `DynNat` change that Simon described above. This worked out really nice because this type is basically the type of natural numbers at the value level, so I added all the usual instances for it and called it `Natural`, which mirrors `Integer`. I think that that's all. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 diatchki): Replying to [ticket:4385 diatchki]: The most recently merged version of the implementation is at: http://code.galois.com/darcs/type-naturals/09-Jan-2011/ The patches there are relative to GHC (and relevant libraries) as of 09-Jan-2011. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by adamgundry): * cc: adam.gun...@… (added) Comment: I have been doing some theoretical work on type inference for systems like this, and am interested to see how this extension progresses. It is definitely worth considering signed integers: if nothing else, solving equations tends to become easier. Of course, natural numbers can be recovered once you have inequalities, though it might make sense to have special support for such a common use case. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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
+---
Changes (by Khudyakov):
* cc: alexey.sklad...@… (added)
Comment:
I want to point out that type level signed integer numbers could be useful
too. One use which immediately springs into mind is attaching dimension to
physical values. Negative powers appears there all the time e.g. speed ~
cm·s^{-1}. It's natural to encode dimensions using integer numbers.
This is not top priority item but I think it's good to keep such
possibility in mind.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:5
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 diatchki): Replying to [comment:3 simonpj]: I wonder if you might use the GHC Trac Wiki instead?. I moved the wiki pages to the GHC wiki: http://hackage.haskell.org/trac/ghc/wiki/TypeNats * 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. Agreed. In fact, I hacked this up on the plane ride back from ICFP, but Happy pointed out that it leads to an ambiguity in imports and exports. I described the issue and a potential solution in http://hackage.haskell.org/trac/haskell- prime/wiki/InfixTypeConstructors#Issues -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 +--- Changes (by igloo): * milestone: = 7.2.1 -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #4385: Type-level natural numbers
#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 diatchki): The repos implementing this feature are now at this location: http://code.galois.com/darcs/type-naturals/ A brief explanation of the implementation and how to use it as available here: https://github.com/yav/memory-arrays/wiki -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
