type aliases and Id

[John Meacham]

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⑈