Dear GHC developers,
I've been working with type families to design a framework for type-level
numerical computations (I'm sure everyone here is familiar with the idea). I
made a library implementing most of the basic stuff[1], and I've been using it
to try to build functions that use type-level induction (I'll explain exactly
what I mean further down). I succeeded in getting this to work in an older
version of GHC HEAD, but somethings changed in the last month or so that broke
my old code, so naturally, I'm trying to get it working again. Here's a simple
example of what I'm trying to do. The library I wrote has types True & False,
and types for the integers (D0, D1, D2, etc.). There are also type families
:+:, :*:, etc. that construct the type for the given operation that corresponds
to the arguments. Finally, there are also relational operators :==:, :<:, etc.
that produce the type True when the given relation holds, otherwise False.
So this is some code that illustrates what I'm trying to do. The parameter `n'
in the TestIter class is the type variable under iteration, and the `zero'
parameter represents the termination condition.
> class ( NaturalT n, zero ~ (n :==: D0) )
> => TestIter n zero where
> testIter :: n -> zero -> Prelude.String
>
> instance ( NaturalT n
> , zero ~ (n :==: D0)
> , zero ~ True )
> => TestIter n True where
> testIter _ _ = ""
>
> instance forall n n' zero zero' .
> ( NaturalT n
> , zero ~ (n :==: D0)
> , zero ~ False
> , n' ~ Pred n
> , zero' ~ (n' :==: D0)
> , TestIter n' zero' )
> => TestIter n False where
> testIter n _ =
> intToDigit (fromIntegerT n) : testIter (_T :: n') (_T :: zero')
(_T is just another name for undefined here.) I want a call to e.g.
> testIter (_T :: D9) (_T :: False)
to produce the string "987654321". Basically, I'm trying to use recursion to
span the types D9, D8, D7, .. , D1, after which the recursion terminates at D0.
When I compile this code, I get:
Test.hs:175:9:
Couldn't match expected type `IsEQ (Compare n (Dec DecN))'
against inferred type `True'
In the instance declaration for `TestIter n True'
Test.hs:181:9:
Couldn't match expected type `IsEQ (Compare n (Dec DecN))'
against inferred type `False'
In the instance declaration for `TestIter n False'
Test.hs:181:9:
Couldn't match expected type `Compare n' (Dec DecN)'
against inferred type `t'
In the instance declaration for `TestIter n False'
For reference, (IsEQ (Compare n (Dec DecN))) is what the type (n :==: D0)
expands to, and should eventually expand to True or False. (Dec DecN) is the
actual underlying type of D0.
Now, I'm not sure that this is exactly the code that used to compile, but it's
close. I don't quite understand why I'm getting these errors, either. For the
first one, (the instance for `TestIter n True'), I've included the constraints
(zero ~ (n :==: D0), zero ~ True), so the compiler should know that (n :==: D0)
and True are the same type, right? The same kind of reasoning goes for the
other instances.
So my question is, can anyone see anything I'm doing wrong? Am I barking up the
wrong tree altogether? Is this sort of thing not really allowed by type
families? I really need to be able to do things like this, because a project
I'm working on depends on compile time verification of the size of certain data
structures which are parameterized by one of these type-level integers, and I
really don't want to change to run-time verification.
Any ideas?
Thanks in advance,
Peter Gavin
<[EMAIL PROTECTED]>
Links:
[1] http://hackage.haskell.org/cgi-bin/hackage-scripts/package/tfp
_______________________________________________
Cvs-ghc mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/cvs-ghc
