Skip to content

Conversation

@elegios
Copy link
Contributor

@elegios elegios commented Nov 11, 2025

This PR adds a very simple version of higher-order abstract syntax, intended to make the construction of lean, easy-to-read ASTs simpler. The idea is to add a new term that semantically is the same as TmLam, except it's represented by an actual function. This function is allowed to do whatever it wants whenever it's given an argument, with two (necessarily unenforced) restrictions:

  • The expression it builds should be semantically equivalent no matter its input.
  • The argument expression (or it's sub-expressions) must not be duplicated in the returned function.

The PR also contains a simple inlining pass built on these terms, that simply finds all let-bindings that are referred exactly once and inlines them.

However, there are a number of design questions to consider before merging (hence draft):

  • The TempLam and TempFix nodes currently only store their functions. This is enough to construct ASTs, but not to, e.g., call tyTm, infoTm, or any of the related setters. We could implement them by actually calling the functions with fabricated arguments, which is how pretty printing works, but it might mess with the intuition that tyTm and infoTm are cheap functions.
  • Should we design these nodes to construct type annotated ASTs?
    • If so, what happens to polymorphism? Our type system does not allow polymorphic lambdas, only let-bound values may be polymorphic.
  • Should we make them carry a string version of the name, so the pretty printing doesn't always use some variant of x?

@elegios elegios force-pushed the hoas-inline-single-use branch from 352fe64 to 5cf006f Compare November 27, 2025 14:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant