type aliases and Id
Simon PeytonJones
simonpj at microsoft.com
Wed Mar 21 04:36:30 EDT 2007
 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.
Yes, that's true. But I still don't know how to do inference. Consider
f :: forall m a. m a > a > [a]
t :: Tree Int
and consider the call
f t t
Well, this is perfectly well typed thus (I'll add the type applications to make it totally clear):
f Id (Tree Int) t t
That is, instantiate m=Id, a=Tree Int, and voila. The trouble is, when unifying (m a) = (Tree Int), it's very unclear what to do.
Hmm. I suppose you might defer such unifications, instead gathering them as constraints, and solving them only when you quantify. That's the standard way to deal with tricky unification problems.
It's certainly a nice challenge.
Simon

 Perhaps a good topic for a research paper?

  Lennart

 On Mar 20, 2007, at 12:00 , Simon PeytonJones 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 typelevel lambdas.
 >
 > Simon
More information about the Haskellprime
mailing list