Simon Peyton-Jones wrote: > Indeed the foralls are at the top, but I claim that wherever > you could use the composition function you were expecting, > you can also use the one GHC gives you. The two types > are isomorphic. > ... > Let me know if you find a situation where this isn't true. > ... > No I believe it is not a bug. I would be interested to see why you > needed to change your code.
It is all not that simple. Let me try to explain. For some deeper background I refer to my draft. One more week to finish. http://www.cwi.nl/~ralf/rank2/ Maybe, we should do that offline. But maybe it is interesting for people how like rank-2 stuff. Let's consult the following code with the ghc 5.03 snapshot. It is basically the same kind of example as in my last posting but I point out a few things more clearly, and the example is simpler. --------------------------------------------------------------------- type Generic i o = forall x. i x -> o x type Id x = x comb :: (Generic Id Id) -> (Generic Id Id) -> (Generic Id Id) comb = undefined comb' :: forall x1 x11 x. (Id x1 -> Id x1) -> (Id x11 -> Id x11) -> Id x -> Id x comb' = undefined yacomb :: (forall x. x -> x) -> (forall x. x -> x) -> (forall x. x -> x) yacomb = (.) yacomb' :: forall x y z. (x -> x) -> (y -> y) -> (z -> z) yacomb' = undefined --------------------------------------------------------------------- I explain the code per def./decl.: 1. The type synonym Generic captures a parameterized function type where we can still plug in type constructors of kind *->* to derive domain and codomain from the explicitly quantified x. The type Generic suggests that we deal parametric polymorphism but in my real code I have class constraints on x. This immediately resolves Simon's concern about the usefulness of defining sequential composition in some new way. I had chosen seq. comp. as an example to play with types. If we go beyond parametric polymorphism, several binary combinators using Generic for arguments and result make sense (see my draft; feedback appreciated). 2. The type constructor Id of kind * -> * is the identity type constructor. That is, given a type, it returns the very same type. There are plenty of useful type constructors like Id but let's restrict our discussion to Id for simplicity. As an aside, I like it very much that ghc allows me to compose type synoyms like I do with Generic and Id. hugs doesn't allow me that, and this implies that I have to use datatypes instead for things like Id, and this in turn implies that I have quite some wrapping / unwrapping going on in my hugs expression code. 3. Let's suppose we want to define SOME binary function combinator comb. It takes two polymorphic functions of a certain type as for i and o and returns another polymorphic function with potentially some other i and o for the domain and codomain. In fact, I have chosen Id for all i and o parameters for the above comb for simplicity. Let's us ignore parametricity for a moment and pretend we know how to define many combinators like this. In the example above, I left comb undefined since I only want to play with the ghc type system. As I said, in my true code I define interesting combinators with such type schemes but with extra class constraints. This is the reason that I can do more things than parametricity allows me. So let us really not think of ordinary (say, parametric polymorphic) sequential composition as my last email maybe suggested. 4. So now let's ask for the type of comb in ghc. It turns out to be the rank-1 (!!!) type I captured as explicit type annotation for comb'. I would have expected a rank-2 type because the forall is scoped by the type synonym Generic. So why should I like to see the forall going to the top? I still would say that THIS IS A BUG. Here is why the types are different: The rank-1 type allows me to combine functions on say integers (by using Int for x x1 and x11). The rank-2 type that I am asking for rules out monomorphic functions to be composed. So the type with the foralls at the top, and the foralls scoped in a rank-2 discipline are NOT isomorphic. Also, keep the possibility of class constraints in mind. Simon, is it maybe possible that you confused the type of (.), that is, forall b c a. (b -> c) -> (a -> b) -> a -> c with the type forall z y x. (x -> x) -> (y -> y) -> z -> z. The b c a in (.) types deal with the possibly different result types. The z y x in my rank-1 comb (messed up by ghc) deal were originally meant to display insistance on polymorphic function arguments. So the the foralls should not be at the top. 5. The type that I wrote down for yacomb is precisely the rank-2 type I would have favoured to see for comb instead of the actual type suggested by ghci. It is a rank-2 type. A minor issue: I expanded the occurrences of Id for readability (ghc keeps them at all costs because it seems to assume that I like to get reminded of them which is not the case BTW). So everything (the two arguments and the result) are of type forall x. x -> x (which should be equal to Generic Id Id). As an example, I define yacomb to be equal to (.). But note yacomb is a very much restricted (.), not just that it composes type-preserving functions but it insists on polymorphic functions. 6. Now let us see what happens if we take all the foralls to the top. This function would be of the type as shown for yacomb', that is, forall x y z., ... This is precisely the type ghci suggests instead of the rank-2 type except that I applied away Id. Now let's try to define yacomb' in terms of yacomb, that is: yacomb' = yacomb This works. Let us not wonder why. Now let's try to define yacomb' in terms of (.) instead, that is: yacomb' = (.) You get a nice type error in ghci 5.03: test.hs:17: Inferred type is less polymorphic than expected Quantified type variable `x' is unified with another quantified type variabl e `z' Quantified type variable `y' is unified with another quantified type variabl e `z' Signature type: forall z y x. (x -> x) -> (y -> y) -> z -> z Type to generalise: (x -> x) -> (x -> x) -> x -> x When checking the type signature for `yacomb'' When generalising the type(s) for `yacomb'' module `Prelude' is not interpreted Whatever this means, it at least shows that the two types are not isomorphic in the sense that ghci very well separates them even in the case of parametric polymorphism. Or is this (another) bug? Simon Peyton-Jones also wrote: > No, GHC does not support partially applied type synonyms, > except in the RHS of other type synonyms. It is a VERY BIG thing to > allow this, because it amounts to allowing lambdas at the type level > and that messes up inference cruelly. > > Why do you think GHC does? Ok, that's what I meant: in RHSs of other type synonyms. BTW, it also works when passing parameters to parameterized datatypes. Here is a variation on defining Generic as a datatypes as opposed to the earlier type synonym. Id is still the same type synonym as before. data Generic' i o = G (forall x. i x -> o x) type TP = Generic Id Id Yes, I was surprised to see that it works to this extent. In fact, it is already quite expressive in this form because it allows us to have type constructors as type synonyms but of course not arbitrary lambdas as Girard's system would ask for. So I revise my question: Does the current support for partially applied type synonyms pose any challenges or is it basically just like macro expansion? That is, is the type system maybe not even affected by it? If it is easy, why is not in Haskell 98 and in hugs? It is terribly useful. Ralf _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
