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 [EMAIL PROTECTED] 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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
