Conversation

This Tweet was deleted by the Tweet author. Learn more

Apr 22, 2018

Heh, thanks for your help at any rate, slowly getting my head around things. I was trying to avoid direct substitution due to this post: siek.blogspot.com.au/2012/08/ration - but I then ran into this bug: github.com/brendanzab/pik

Brendan Zabarauskas

@brendanzab

Apr 22, 2018

Maybe I'm getting mixed up between 'environments' and 'contexts' too - I was attempting to use the typechecking context to do my substitutions, but it's obvious now that it that would break down in more complex examples. In HOAS you get an environment for free.

crow emoji

@glaebhoerl

Apr 22, 2018

AFAIU: context = name -> type, env = name -> value. And the diff between "normalization" and "evaluation" is more-or-less that normalization goes under binders and "fully evaluates" (to "*the* normal form"), mere 'evaluation' doesn't (necessarily).

crow emoji

@glaebhoerl

Apr 22, 2018

(Once again I'm trying to relay things I learned from András, most likely imperfectly.)

crow emoji

@glaebhoerl

Apr 22, 2018

(I'm also not -certain- HOAS couldn't work in Rust - do you _need_ to use Rc everywhere, can't you use &Fn during the normalization process? I might experiment a little...)

Brendan Zabarauskas

@brendanzab

Apr 22, 2018

Very possibly! Would love to see a quick gist!

Brendan Zabarauskas

@brendanzab

Apr 22, 2018

Here's a start on the Wikipedia example of NbE: play.rust-lang.org/?gist=e6e7d13c - note how you need to allocate the closures at some stage. I guess you could allocated them in an arena or something? 🤷‍♂️

crow emoji

@glaebhoerl

Apr 22, 2018

Heh. I haven't done very much actual coding in Rust so I started with a typechecker (because that's more obvious) just to re-familiarize myself before attempting that: play.rust-lang.org/?gist=e75c0f71

crow emoji

@glaebhoerl

Apr 22, 2018

(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:)

Replying to

and

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.

2:43 PM · Apr 22, 2018Twitter Web Client

Replying to

and

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.

Brendan Zabarauskas

@brendanzab

Apr 22, 2018

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.

Show replies