type aliases and Id

[Jacques Carette]

There is a general solution, but it essentially involves polymorphism 
a-la-Omega (or as in Coq's Calculus of Inductive Constructions).

The most general description of (Tree Int) is as the Stream
S = [Int, Tree, Id, Id, ...]
You are now attempting to pull-off exactly 2 "terms" from that Stream.  
The solutions are:
0: Int, Tree
1: Tree Int, Id
2: Id (Tree Int), Id
3: Id (Id (Tree Int)), Id

Let T at i denote n-ary type-level application, where T is a list of types, 
and i>=0.  Consider the pair
( S!!(i+1), (take i S)@i)
This is the /closed-form/ for the n'th solution (m, a) for unifying (m 
a) with (Tree Int).  A better way to _represent_ this closed form is as
(S, i) where S = [Int,Tree, Id, Id, ...]
from which further constraints can decide what is the 'proper' value of 
i to take.  This even shows how to do defaulting: in the absence of 
further information, take the smallest i possible.  [I phrase it this 
way because there are times where constraints will force a certain 
minimum on i, but no maximum].

In other words, the above should be backwards compatible with current 
behaviour, since the 'default' solution would be m=Tree, a=Int.

Jacques

Simon Peyton-Jones wrote:
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-prime
>