type aliases and Id

[Simon Peyton-Jones]

| 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