| I don't think you need to produce 'a=Id (Tree Int)' since that
| reduces to 'a=Tree Int'.
| In general, you don't have to produce Id applied to anything, which
| gives me some hope that it's possible to add Id and still have
| decidable (and complete) type deduction.
Yes, that's true. But I still don't know how to do inference. Consider
f :: forall m a. m a -> a -> [a]
t :: Tree Int
and consider the call
f t t
Well, this is perfectly well typed thus (I'll add the type applications to make
it totally clear):
f Id (Tree Int) t t
That is, instantiate m=Id, a=Tree Int, and voila. The trouble is, when
unifying (m a) = (Tree Int), it's very unclear what to do.
Hmm. I suppose you might defer such unifications, instead gathering them as
constraints, and solving them only when you quantify. That's the standard way
to deal with tricky unification problems.
It's certainly a nice challenge.
Simon
|
| Perhaps a good topic for a research paper?
|
| -- Lennart
|
| On Mar 20, 2007, at 12:00 , Simon Peyton-Jones wrote:
|
| > | Ganesh and I were discussing today what would happen if one adds Id
| > | as a primitive type constructor. How much did you have to change
| > the
| > | type checker? Presumably if you need to unify 'm a' with 'a' you
| > now
| > | have to set m=Id. Do you know if you can run into higher order
| > | unification problems? My gut feeling is that with just Id, you
| > | probably don't, but I would not bet on it.
| > |
| > | Having Id would be cool. If we make an instance 'Monad Id' it's now
| > | possible to get rid of map and always use mapM instead. Similarly
| > | with other monadic functions.
| >
| > I remember that I have, more than once, devoted an hour or two to
| > the question "could one add Id as a distinguished type constructor
| > to Haskell". Sadly, each time I concluded "no".
| >
| > I'm prepared to be proved wrong. But here's the difficulty.
| > Suppose we want to unify
| > (m a) with (Tree Int)
| >
| > At the moment there's no problem: m=Tree, a=Int. But with Id
| > another solution is
| > m=Id, a=Tree Int
| >
| > And there are more
| > m=Id, a=Id (Tree Int)
| >
| > We don't know which one to use until we see all the *other* uses of
| > 'm' and 'a'.
| >
| > I have no clue how to solve this problem. Maybe someone else
| > does. I agree that Id alone would be Jolly Useful, even without
| > full type-level lambdas.
| >
| > Simon
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
