type aliases and Id

[Lennart Augustsson]

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 <igloo at earth.li> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-prime