This period I did the course Advanced Functional Programming and I had to choose a subject from a set list of subjects to present. I chose typed transformations of typed abstract syntax (TTTAS). (See this webpage for the technical report and associated library by Arthur Baars, Doaitse Swierstra and Marcos Viera.)
I already expected the subject to be one of the harder ones and I also had a restriction for the presentation due to practical issues, namely we could only use handouts (or your own laptop) and not a beamer because of multiple presenters.
Thus I made some handouts in a tutorial like fashion. It might save you some typing of the code found in the paper and hopefully get you interested in the subject. You might also find it useful to get some motivation for the use of GADTs and transformations of EDSLs in general.
The handouts:
The PDF file is here.
The lhs can be found here.
Subscribe to:
Post Comments (Atom)
It should be enough to change the type signature of eval4 to
ReplyDeleteeval4 :: Expr a env -> (Env Expr env env) -> a
The interesting change is requiring use and def to be the same. We see from the type of lookupEnv
lookupEnv :: Ref a def -> Env t use def -> t a use
that the ref types index into the sequence "def" of types, but the terms expect to be run in an environment that defines the sequence of things in "use" - so if eval4 hopes to use the same environment to evaluate the terms it looks up, it had better require them to be the same.
Fixing the "env" parameter of the Expr application, and making the "t" parameter of Env more specific is also required, but pretty straightforward.
Okay cool :). Thanks. I think I tried something similar before, but then lacked the time before the day of the presentation itself to figure the rest out.
ReplyDelete