Toot

Written by Zhixuan Yang on 2025-01-26 at 13:37

@zanzi is the datatype for your language with explicit substitution something like data P f g x = Ret x | O (f (P f g x)) | S (g (P f g (P f g x)))?

If so, they are analogous to not lists but binary trees (because we have two P's in the S constructor).

~~We do have efficient purely functional implementation of binary trees¹ with fast leaf substitution, so we can use the reinterpretation trick again to have an efficient representation of your datatype.~~

EDIT: the monadic bind for P that you want only substitutes the second P for the S contructor, so this makes things even simpler: we can just make P a recursively defined instance of free monads: P ~= Free (f + (g ∘ P)).

But I should be clear that I have not done any performance tests: this kind of complex representations are asymptotically fast but almost certainly not fast for small inputs 😅

As for de Bruijn indices, looking forward to seeing your work sometime! I have been thinking about it but capture-avoiding substitution for de-Bruijn indexed λ-terms seems tricky too because of index shifting. I am still thinking about if I can come up with some data structure to efficiently handle it but I have no conclusive idea yet. (And I am also looking at Murdoch's nominal sets tutorial in Haskell. Capture-avoiding substitution for nominal sets seems to be quite close to reckless substitution...)

¹ Binary trees are special cases of free monads, and we already know fast implementations of free monads.

=> More informations about this toot | View the thread | More toots from zyang@mathstodon.xyz

Mentions

=> View zanzi@mathstodon.xyz profile

Tags