#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
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
