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