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