Language.TDPE
Contents
- Demo first
- bbf1 and bbf2 are imported from the _compiled_ module ToTDPE
- It would be great to have a function a -> repr a
- Deriving reify_t :: t -> repr t
- Why the name
reify? - Start with reify_aa :: (a -> a) -> repr (a -> a)
- Deriving reify_aabb :: (a->a)->(b->b) -> repr ((a->a)->(b->b))
- We need reflect_aa :: repr (a->a) -> (repr a -> repr a)
- We build reify_t and reflect_t together and inductively.
- The base of induction (reify/reflect for base types)
- The inductive case
- Examples
- Duality of reify/reflect
- reflect . reify = eq_meta
- reify . reflect = eq_obj
- reify gives the object term representing the normal form of meta
- cf Normalization-by-evaluation
Description
Type-directed partial evaluation, Olivier Danvy, POPL96 * http://www.brics.dk/~danvy/tdpe-ln.pdf