is shadowing allowed in CoreSyn?
megacz at cs.berkeley.edu
Mon Feb 7 20:46:28 CET 2011
Hello! I'm currently attempting to reconstruct natural deduction proofs
(with explicit contraction/exchange/weakening) in System FC from
CoreSyn.Expr's in order to carry out a transformation which is defined
by induction on proofs (rather than terms). I have it working for
simple examples, and now I need to clean up the corner cases. I have a
few questions about the exact rules for what is/isn't legal in
Is shadowing allowed in CoreSyn? For example:
(Lam x (Lam x e))
If it is okay, I assume it creates a situation where you may shadow, but
only if the variables have the same type. In other words, you can't
represent this term without doing some \alpha-renaming:
\lambda x:Int . \lambda x:Char . e
... since in CoreSyn the type annotation on the lambda is actually part
of the Var, not the Expr production for Lam.
Also, I noticed -- to my surprise -- that Let can be used to bind type
variables. Can recursive-Let be used for type variables? If so, it
would seem to step well outside of System F (or FC)...
I assume that (Case (Type t) v t' alts) is illegal; could somebody
More information about the Cvs-ghc