tag:blogger.com,1999:blog-8387731529560364137.post6456941282743189956..comments2023-10-30T15:17:54.112+01:00Comments on A dose of logic: A small handout on TTTAS (Typed Transformations of Typed Abstract Syntax)Nebasukehttp://www.blogger.com/profile/00690086652715846121noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-8387731529560364137.post-87816487162784454152010-04-21T00:23:13.174+02:002010-04-21T00:23:13.174+02:00Okay cool :). Thanks. I think I tried something si...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.Nebasukehttps://www.blogger.com/profile/00690086652715846121noreply@blogger.comtag:blogger.com,1999:blog-8387731529560364137.post-90353868855154554452010-04-20T23:18:37.723+02:002010-04-20T23:18:37.723+02:00It should be enough to change the type signature o...It should be enough to change the type signature of eval4 to<br /><br />eval4 :: Expr a env -> (Env Expr env env) -> a<br /><br />The interesting change is requiring use and def to be the same. We see from the type of lookupEnv<br /><br />lookupEnv :: Ref a def -> Env t use def -> t a use<br /><br />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.<br /><br />Fixing the "env" parameter of the Expr application, and making the "t" parameter of Env more specific is also required, but pretty straightforward.Anonymousnoreply@blogger.com