type aliases and Id

[Lennart Augustsson]

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