RE: first-class polymorphism beats rank-2 polymorphism
| 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. This works because you said Generic not Generic' in the RHS of TP. If you use Generic' the program is rejected, and so it should be. | 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. It's just macro expansion. GHC expands saturated type synonyms before looking for well-formedness in types. This is indeed rather useful, and it's easy too. It's not in H98 because no one thought of it then. Simon ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: first-class polymorphism beats rank-2 polymorphism
| 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 | 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 Yes, indeed this is a bug. Thank you for finding it. It turned out that in liberalising GHC's treatment of type synonyms (which you remark is a good thing) I had failed to cover a case. Fortunately, an ASSERT caught the bug in my build, and the fix is easy. | yacomb1 :: (forall x. x -> x) | -> (forall x. x -> x) | -> (forall x. x -> x) | yacomb1 = (.) | | yacomb2 :: forall x y z. (x -> x) -> (y -> y) -> (z -> z) | yacomb2 = undefined | | Now let's try to define yacomb2 in terms of yacomb1, that is: | | yacomb2 = yacomb1 | | This works. Let us not wonder why. We should wonder why. It's plain wrong. yacomb1's type signature is more restrictive than that of yacomb2. This is a bug in the 5.03 snapshot, which fortunately I fixed a week or two ago. The compiler in the respository rejects the definition. Bottom line: you found two bugs, for which much thanks. But I stand by forall-lifting! (But note that the foralls are lifted only from *after* the arrow, not before. (forall a.a->a) -> Int is not the same as (forall a. (a->a) -> Int).) Simon ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: first-class polymorphism beats rank-2 polymorphism
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 B
RE: first-class polymorphism beats rank-2 polymorphism
| Looking at the type of sequ, | the foralls for t end up at the top. | Hence, I have no chance to define sequential | composition. 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. | Please let me know if this is a bug. No I believe it is not a bug. I would be interested to see why you needed to change your code. | I just realized that type synonyms in GHC seem to be valid | arguments even when not completely instantiated? This is | wonderful. It is not supported in hugs. How difficult is it | to cope with this? Does it make a real difference for the type system? 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? Simon ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: first-class polymorphism beats rank-2 polymorphism
Simon Peyton-Jones wrote: > In fact GHC does "forall-lifting" on type signatures to bring the > foralls to the front. But there's a bug in 5.02's forall-lifting... > ... > Perhaps you can try the 5.03 snapshot release? Certain things work there. In fact, it is fascinating. But now I did a new experiment ... It seems that forall-lifting does not work as expected for type synonyms in 5.03. Here is an example from my upcoming ICFP submission :-) Here is an innocent type synonym for generic functions with three parameters of kind * -> *: type Generic i o m = forall x. i x -> m (o x) This is a good candidate for all the parameters: type Id x = x Now I tried to define sequential composition. In fact, the following type deals with a very restricted case for simplicity: sequ :: forall t. (Generic t t Id) -> (Generic t t Id) -> (Generic t t Id) sequ f g = undefined Looking at the type of sequ, the foralls for t end up at the top. Hence, I have no chance to define sequential composition. Main> :t sequ forall t x1 x11 x. (t x1 -> Id (t x1)) -> (t x11 -> Id (t x11)) -> t x -> Id (t x) Main> Please let me know if this is a bug. Please don't fix it too soon :-) because otherwise I had to rewrite some material which is now based on first-class polymorphism and datatypes for i, o, and m. Such code will probably look better in proper rank-2 style with type synonyms for type constructor parameters. I just realized that type synonyms in GHC seem to be valid arguments even when not completely instantiated? This is wonderful. It is not supported in hugs. How difficult is it to cope with this? Does it make a real difference for the type system? Ralf ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: first-class polymorphism beats rank-2 polymorphism
| So I would claim that these two types are the same: | | forall x. Class x => (forall y. Class y => y -> y) -> x -> x | (forall y. Class y => y -> y) -> (forall x. Class x => x -> x) | | ...so you should be able to do this: | | combinator :: (forall y. Class y => y -> y) -> (forall x. | Class x => x -> x) | combinator f x = combinator' f x | | but for some reason GHC 5.02.2 complains. I think this is a bug. Indeed the two types are the same. In fact GHC does "forall-lifting" on type signatures to bring the foralls to the front. But there's a bug in 5.02's forall-lifting... it doesn't bring the constraints to the front too. I fixed this in 5.03 a while ago, but didn't back-propagate the fix to 5.02. And indeed, 5.03 is happy with the pure rank-2 program. class Class x where combinator' :: (forall y. Class y => y -> y) -> x -> x combinator :: (forall y. Class y => y -> y) -> (forall x. Class x => x -> x) combinator f = combinator' f It's quite a bit of extra work propagating fixes into the 5.02 branch, so I probably won't do so for this one, since only a small minority of people will trip over it. Perhaps you can try the 5.03 snapshot release? Simon ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: first-class polymorphism beats rank-2 polymorphism
At 2002-03-06 06:13, Ralf Laemmel wrote: >This is not a bug, Isn't it? Consider: class Class x where combinator' :: (forall y. Class y => y -> y) -> x -> x This gives: combinator' :: forall x. Class x => (forall y. Class y => y -> y) -> x -> x What happens when you pass something of type (forall y. Class y => y -> y)? s :: forall x. Class x => x -> x s = combinator' id; So I would claim that these two types are the same: forall x. Class x => (forall y. Class y => y -> y) -> x -> x (forall y. Class y => y -> y) -> (forall x. Class x => x -> x) ...so you should be able to do this: combinator :: (forall y. Class y => y -> y) -> (forall x. Class x => x -> x) combinator f x = combinator' f x but for some reason GHC 5.02.2 complains. I think this is a bug. Apparently 5.03 has rank-N polymorphism so maybe this is fixed too. -- Ashley Yakeley, Seattle WA ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
