@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 | View the thread | More toots from zanzi@mathstodon.xyz
=> View zyang@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).