Further to recent remarks, I have now implemented a toy elaborator for Hutton’s Razor (the language of integers with addition). You can find it here. Seems to work. The elaborator itself is
tiny.
hutton :: [Value] → Blah
hutton _ =
Conc (MNode PLUS ["x", "y"] $
Bind ("x", Call hutton []) $ λx →
Bind ("y", Call hutton []) $ λy →
Solve (plus x y)) $
Conc (MNum $ λi → Solve (VC i Nothing)) $
Error "unrecognized input"
More chat about this later.