Move away from using Moniker for variable binding about pikelet HOT 7 CLOSED

Oooh thanks! I've heard of hypergraphs before! Both from @sashaboyd and @robrix https://twitter.com/rob_rix/status/1224461727678509057. One of the issues I'm running into with the way I'm doing NbE in #197 is that it's hard to check the equivalence of dependent record types using this representation:

pub enum Value {
    ⋮
    /// Record type extension.
    RecordTypeExtend(String, Arc<Value>, Closure),
    /// Empty record types.
    RecordTypeEmpty,
    ⋮

from pikelet.

Updated the description with a link to this example: https://github.com/jozefg/nbe-for-mltt/

from pikelet.

I haven't tried to understand them very much, but some recent work in Haskell on nominal stuff, in case it might come in helpful:

https://github.com/ekmett/name

https://hackage.haskell.org/package/nominal

from pikelet.

Thanks for linking those @glaebhoerl, much appreciated! 👍

from pikelet.

I have a Rust port of Nbe using semantic type checking up at brendanzab/rust-nbe-for-mltt. I think this is the approach I am going to go with, but it will be a bit tricky to make!

from pikelet.

@AndrasKovacs has put together a nice approach in smalltt. I don't really understand it yet though (the implementation is a little tricky to understand), so I might persist with the nbe-for-mltt approach for now, which seems more approachable. I think we'll be able to adapt smalltt easier by that stage though, if we wanted to.

from pikelet.

While i haven't tried it yet, another thing worth looking into

Similar to the graph approach is using hypergraphs, Ueda has a number of papers on name binding and lambda terms as hypergraphs Name Binding is Easy with Hypergraphs

Not aware of any rust libraries for dealing with hypergraphs being available yet though.

from pikelet.