Ravi, 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. Did you do that in the Bluespec compiler? -- Lennart On Mar 19, 2007, at 19:26 , Ravi Nanavati wrote:

On 3/19/07, Ian Lynagh wrote: I'd really like to be able to define an eta-reduced Id; I see two possibilities:

* Allow "type Id =" (I prefer this to "type Id" as I think we are more likely to want to use the latter syntax for something else later on).

* Implementations should eta-reduce all type synonyms as much as possible, e.g. type T a b c d = X a b Int c d is equivalent to type T a b = X a b Int and type Id a = a is equivalent to a type that cannot be expressed directly.

Any opinions?

A third possibility is to have "Id" be a special primitive type constructor of kind * -> * that implementations handle internally. If you wanted to give it different name you could use an eta- reduced type synonym for that, of course.

That's the approach I took when I needed an identity type function in the Bluespec compiler, and that worked out reasonably well. Part of the reason that worked out, though, is that we already had a normalization point during typechecking where certain special type constructors (related to numeric types) were cleaned out, so adding Id just extended that a little.

I don't know whether adding such a constructor would be an equally simple change for Haskell implementations. And there's the separate argument that requiring eta-reduction of all type synonyms might be an interesting new feature in its own right (since I think you can say other new things beyond type Id a = a).

- Ravi _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime

On Mon, Mar 19, 2007 at 07:55:30PM +0000, Lennart Augustsson 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.

I have actually very much wanted this on a couple occasions. the main one being the 'annotation problem'. an abstract syntax tree you might want to annotate with different types of data. the current solution is something like data Ef f = EAp (f E) (f E) | ELam Var (f E) newtype Identity x = Identity x -- annotate with nothing type E = Ef Identity -- annotate with free variables type EFV = Ef ((,) (Set.Set Var)) etc... unfortunately, it makes the base case, when there are no annotations, very verbose. if we had (Id :: * -> *) then we could make type E = Ef Id and just pretend the annotations arn't there.

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. Did you do that in the Bluespec compiler?

I don't see how declaring instances for such a type synonym would be possible. Type synonyms are fully expanded before any type checking. (they are basically just type-level macros). An unapplied 'Id' would not be able to expand to anything, so you would not be able to create an instance for it. This is a little odd in that the instance is properly kinded, yet still invalid. but I don't see that as a big issue, as there are other reasons instances can be invalid besides being improperly kinded.... John -- John Meacham - ⑆repetae.net⑆john⑈

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@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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime

| 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 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