type aliases and Id
carette at mcmaster.ca
Tue Mar 20 11:41:58 EDT 2007
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.
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.
> Haskell-prime mailing list
> Haskell-prime at haskell.org
More information about the Haskell-prime