Simon Peyton-Jones wrote:
Peter
Yes, this is the kind of thing you should be able to do. But
a) I'm boggled by your code -- I didn't understand it at all. Doubtless
there are supporting definitions that you didn't give. It looks very
> Oleg-like; definitely worth asking hin. For example, when you write
> class ( NaturalT n, zero ~ (n :==: D0) )
> => TestIter n zero where
> testIter :: n -> zero -> Prelude.String
I don't know why you didn't use the simpler formulation
> class ( NaturalT n )
> => TestIter n where
> testIter :: n -> (n :==: D0) -> Prelude.String
Hi Simon,
Thanks for the reply.
If I were to use the simpler definition for TestIter that you wrote, I wouldn't
be able to implement different cases for when (n :==: D0) and otherwise. That
is, I'd have to do
> instance ( NaturalT n, (n :==: D0) ~ True )
> => TestIter n where
> ...
>
> instance ( NaturalT n, (n :==: D0) ~ False )
> => TestIter n where
> ...
which is a duplicate instance declaration. (The real problem is that the
compiler cannot know that (n :==: D0) will be either True or False, but not
both.) So I have to parameterize the whole class on the result of (n :==: D0)
and define the instances accordingly.
b) You are using an equality predicate as a superclass. This is an important
> thing to be able to do, but GHC just does not support it properly at the
> moment. It's the last big piece of the type-function puzzle. I can't tell
> whether that's the reason your program doesn't work at the moment.
Ok, I'll keep that in mind. Equalities in the constraints for instances are
fully supported, though, is that right?
I actually think the equality as a superclass is what made the code fail to
compile, because when I removed it, the compilation completed successfully.
Thanks again,
Pete
Sorry not to be more help.
Simon
-----Original Message-----
| From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On
| Behalf Of Peter Gavin
| Sent: 21 October 2008 14:57
| To: [email protected]
| Subject: type families & type-level recursion
|
| 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
_______________________________________________
Cvs-ghc mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/cvs-ghc
