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

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.

Leave a Reply