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 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. 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
