Ancestors

Written by Zhixuan Yang on 2025-01-26 at 00:56

Can I ask a question as an absolutely novice language implementor? Suppose I want to implement a substitution-based evaluator of some language. After parsing a term into a syntax tree, can I just rename binders in the program to make sure no binders use the same variable name, and then

just forget about capture avoidance when substituting?

(As for why I am doing this: I am playing with a representation of free monads that has amortised constant-time-per-variable substitution and constant-time case analysis, so I'd like to see how fast a stupid evaluator can be if the underlying data structure is clever)

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

Written by Zanzi @ Monoidal Cafe on 2025-01-26 at 11:57

@zyang huh that's interesting, how did you get your free monads to do that?

=> More informations about this toot | More toots from zanzi@mathstodon.xyz

Written by Zhixuan Yang on 2025-01-26 at 12:18

@zanzi By noticing many algorithms in Okasaki's book type check in linear languages — of course, why would you duplicate or discard data payloads when implementing a data structure, so we can reinterpret these algorithms in suitable monoidal categories, such as endofunctors with Day tensor or endofunctor with composition.

Here are my manual translation from Okasaki's concatenable lists (Section 10.2.1 in his book) to free applicatives and free monadds: https://gist.github.com/yangzhixuan/07c2b3abf676b797cdfa0e77aa7700e8

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

Written by Zanzi @ Monoidal Cafe on 2025-01-26 at 13:05

@zyang wow! this is really cool! I'm working on a language that has an explicit substitution operation whose semantics is a free monad (ie see the paper Explicit Substitutions and Higher-Order Syntax by Neil Ghani), do you think your technique would be applicable to it?

for technical reasons I'm forced to use small-step operational semantics rather than nbe, so if substitution could be made more efficient I would be extremely interested!

=> More informations about this toot | More toots from zanzi@mathstodon.xyz

Written by Zanzi @ Monoidal Cafe on 2025-01-26 at 13:08

@zyang oh, btw, to answer your original question - I'd use de-bruijn in this case to avoid dealing with names altogether. Lambda terms with debruijn indeces form a relative monad, so your technique should be applicable to it. I have some unpublished work on implementing well-typed and well-scoped languages using free relative monads, so it seems like there's an avenue for collaboration here :D

=> More informations about this toot | More toots from zanzi@mathstodon.xyz

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 | More toots from zyang@mathstodon.xyz

Toot

Written by Zanzi @ Monoidal Cafe on 2025-01-26 at 14:17

@zyang yes, good catch, these are binary trees!

so the important thing with de bruijn shifts is that going under binders is functorial. in the simplest case, it means that you can define renaming as a functor, and your substitution will be given by a monad relative to that functor.

but this is incredibly inefficient - you now need to traverse the term twice to perform substitution - one to perform renaming under a binder, and one to do the actual substitution.

a better trick is explained in the papers on "Modules over monads", because there is a module involved, it's possible to define the lifting operation (mbind) mutually with the substitution operation. this simplifies the implementation considerably (now you don't even need renamings).

(the really cool thing is that this generalises to polymorphic calculi, the language i'm working on has parametric polymorphism and uses a term-level substitution that's indexed by a type-level substitution)

the code in the screenshot is representing debruijn indeces using Maybe, ie "Just" is "Succ", but there's a very easy way to generalise it to proper de bruijn terms implemented using Fin.

So if you can apply your technique to the code-below, I can translate it to proper de bruijn terms :D

=> View attached media

=> More informations about this toot | More toots from zanzi@mathstodon.xyz

Descendants

Written by Zhixuan Yang on 2025-01-26 at 14:44

@zanzi Thanks for the explanation! The Maybe part in Abs does create some challenge, but as you may know, in [Fin, Set], F (Succ -) ≅ V => F (where V n = {1 ... n}), so there might be a way. I will let you know if I figure it out!

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

Written by Zanzi @ Monoidal Cafe on 2025-01-26 at 14:47

@zyang I think there should be, yes! Do you have some inkling for why the Maybe poses a challenge? I may be able to help. Is it to do with folds for nested data types?

=> More informations about this toot | More toots from zanzi@mathstodon.xyz

Written by Zhixuan Yang on 2025-01-26 at 14:53

@zanzi That Maybe and the clause Abs x >>= f = Abs (x mbind f) makes LC not a direct instance of the usual free monads (and the corresponding >>=), so we need to come up with a totally new data type, I think...

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

Written by Zanzi @ Monoidal Cafe on 2025-01-26 at 14:57

@zyang Ah, yeah. I have wondered if there's a version of "free module over a free monad" that would do the trick. I suspect that FreeT or some variation of it could work, something capturing a similar idea as Kmett's bound:

https://hackage.haskell.org/package/bound-2.0.7/docs/Bound-Class.html

=> More informations about this toot | More toots from zanzi@mathstodon.xyz