Annotating Expressions

[Fergus Henderson]

On 16-Dec-2003, John Meacham <john at repetae.net> wrote:
> newtype Id a = Id a
> 
> type Er f = f (E f)  -- E used recursivly
> data E f = EAp (Er f) (Er f) | ELam Int (Er f) | 
>         ELetRec [(Int,Er f)] (Er f) | EVar Int
> 
> [...] problem 2 persists. If I don't want to be constantly
> casting to and from Id, I have to use both the seperate annotated and
> unannotated versions.
> 
> is this actually the case? is there a better solution I don't see? perhaps
> something using crazy GHC extensions? if not, are there any proposed
> extensions which would solve this promlem?

I think views <http://www.haskell.org/development/views.html>
would solve this problem, wouldn't they?

You could define a view of `E Id' with constructors
that skip over the conversions to/from Id

	view EId of E Id = App (E Id) (E Id) | Lam Int (E Id) |
		    LetRec [(Int,E Id)] (E Id) | Var Int
	   where
		eid (EAp (Id x) (Id y)) = Ap x y
		eid (ELam x (Id y)) = Lam x y
		eid (ELetRec (B bindings) (Id e)) = LetRec bindings' e
		   where bindings' = map (\(v,(Id x))->(v,x)) bindings
		eid (EVar v) = Var v

Then you can traverse expressions without needing to write
any explicit conversions to/from Id, e.g.

	-- "occurs v e" returns True iff v occurs somewhere in e
	occurs :: Int -> (E Id) -> Bool
	occurs v (Lam v1 e) = v == v1 || occurs v e
	occurs v (Ap x y) = occurs v x || occurs v y
	occurs v (LetRec bindings e) =
		any (\(vi,ei)->v==vi || occurs v ei) bindings || occurs v e
	occurs v (Var v1) = v == v1

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.