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
A followup: in the end I got a working evaluator and normaliser of λ-calculus using my fast free monad and HOAS in the form of
data Lam = Var String | App Lam Lam | Abs (String -> Lam)
In this way, capture-avoiding substitution can still be just reckless substitution as along as we always concretize a binder String -> Lam with free variables. I believe this is also the algorithmic content of Jamie Gabbay's haskell implementation of nominal sets.
The code is still in this gist: https://gist.github.com/yangzhixuan/07c2b3abf676b797cdfa0e77aa7700e8
The code can be improved in a lot of ways, but next I hope I can understand better how it works algorithmically and show that it is asymptotically as efficient as NbE (well, when you bind a closure in the environment in NbE, it is sort of a lazy substitution, right?)
=> More informations about this toot | More toots from zyang@mathstodon.xyz
@zyang I'd say not unless your language enforces linear or affine usage of variables.
As soon as a variable is used twice, substitution will not respect the intended invariant that no two binders use the same variable name.
=> More informations about this toot | More toots from anuytstt@fosstodon.org
@anuytstt ah right 😂 silly me.
=> More informations about this toot | More toots from zyang@mathstodon.xyz
@anuytstt @zyang Do you have an example?
=> More informations about this toot | More toots from dannypsnl@g0v.social
@dannypsnl @anuytstt Good question! To actually construct an example of normalising an all-binder-distinct λ-term using reckless substitution goes wrong, we need to construct a λ-term t such that t has no binders sharing the same variable, and by a sequence of reckless β-reduction t ->* λy. ... (λx. ... λ y. ... x ...) y), which looks like a good Sunday puzzle for me.
=> More informations about this toot | More toots from zyang@mathstodon.xyz
@zyang @anuytstt For free variables occurs at initial term, I already see it can fail, e.g.
(\x. \y. x) y = \y. y (oops)
so if we disallow free variables (all are bound now), then?
=> More informations about this toot | More toots from dannypsnl@g0v.social
@dannypsnl yep, I haven't got an example yet. (But mostly because I have been only watching youtube today 😅 )
=> More informations about this toot | More toots from zyang@mathstodon.xyz
@zyang @dannypsnl
(\f. f f) (\x y. x y)
->
(\x y. x y) (\x y. x y)
->
(\y. (\x y. x y) y)
->
(\y. (\y. y y))
=> More informations about this toot | More toots from LordQuaggan@hachyderm.io
@LordQuaggan @dannypsnl Amazing, thanks!
=> More informations about this toot | More toots from zyang@mathstodon.xyz
@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
@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
@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
@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
@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
@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
=> More informations about this toot | More toots from zanzi@mathstodon.xyz
@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
@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
@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
@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
@zyang Cool! I dont have a good intuition for hoas, but looks great! I'd be super interested if this is as efficient as Nbe! (Or if you can figure out how to apply it to debruijn!)
=> More informations about this toot | More toots from zanzi@mathstodon.xyz This content has been proxied by September (3851b).Proxy Information
text/gemini
