(incidentally, if you know how to make the ugly parts of that (e.g. (*foo).clone()) less ugly, i'd be curious)
(haven't looked at yours in detail yet because bbiab:)
Conversation
I just use Rcs for all the nodes. Might switch to an arena at some stage though. Feel free to check out Pikelet if you like - it does get a little icky at times, alas.
1
Here's some cleanups I would make at least - strategically choosing match vs if let can make things cleaner: play.rust-lang.org/?gist=45361c3a - also tend to fully qualify variants. That way I don't need to do things like TFunction etc.
1
Also the direct approach of matching and using ? looks cleaner in Rust and formats better than using monadic combinators. Sometimes they do help, but I just tend to use them more sparingly these days.
1
Thanks! The bit w.r.t. using `match` to avoid `**` is nice. W.r.t. some of the others I started writing it that way then thought better of it, or couldn't resist golfing :)
1
1
(W.r.t. variants I think fully-qualified is definitely better for a serious codebase, but for gists like this it's just noise. Either that or I'm too used to Haskell atm.)
1
Ah, I found another way: writing e.g. `Term::clone(&term)` and then it's both clear which thing I'm expecting to clone, and deref coercions can kick in so I don't need to count out the *s.
1
2
So I finished it up: play.rust-lang.org/?gist=a4561e78 (did not attempt to make it super-pretty)
Started with Box<Fn> just to get the shape of the code right before I start messing with lifetimes, then changed to Rc just so I could clone, and then... it... just... worked?
2
1
Or your concern was RC cycles rather than whether it'd compile at all? I'd conjecture there'd only be cycles if the object code itself has cyclic references. If you need to support those, what about pulling in Manish's Gc<T>? 👼
2
1
(BTW, wrt NBE itself, I _suspect_ the approach is ~uniquely determined from the constraint: thou shalt never ever traverse a term for to substitute or rename its variables. -Everything- happens through lookup-in-environment.)
1
Replying to
Then the issue might also be how closely it would ultimately match the formalization. HOAS is hard (sometimes impossible) to use in dependent types.
Replying to
(Yeah... if you're getting into hardcore things like that it'd probably really be best to message András. He wrote his thesis about it, knows this stuff inside and out by now: github.com/AndrasKovacs/s)