Stroscot devlog 4

The parser’s kind of working, besides features like EBNF, scannerless parsing, etc. that will be useful later but aren’t strictly necessary. So now I am writing the middle parts for the Stroscot programming language.

I started out by wanting to implement universes with dependent types, in particular experimenting with the New Foundations idea. I also wanted to add subtyping a la Dolan. Then I remembered insane and that it had to suspend most of the “check” calls in order to check recursive types successfully, so I needed an evaluation model. I wondered if type inference was any more complicated, so I looked at Roy and saw the unify function and concluded that implementing type inference was going to involve adding type variables and type solving (unification) to an existing type checker, but wouldn’t change much about the type checker structure, so starting with a dependent type checker would be best.

Then I looked for dependent type checker tutorials and found this; it starts out by presenting an evaluator for the untyped lambda calculus and then extends it gradually. LambdaPi takes a similar approach. They both use environments and closures, but with optimal reduction there are duplicators rather than closures and the environments are stored in the graph, so the implementation is quite different.

So I figured I’d start with to the optimal lambda calculus implementation in macro lambda calculus. But the first thing it does is a pseudo-alpha-renaming pass that identifies all the free variables and replaces them with wires. The code is complicated quite a bit by the separation into a separate inet-lib library which takes a custom-syntax interaction net description and uses JavaScript’s eval features to implement the interaction rules. I went and read “Optimality and inefficiency” and they show poor behavior on C_n = \x -> (2 (2 (2 (2 x)))) where 2 = \s z -> s(s z), when applied to \x y -> x y and \x y -> y x. I still like optimality though; the issues they present are unrelated to interaction nets and can be worked around with the garbage collection in Asperti/BOHM.

I looked for more implementations of LambdaScope and it seems that Jan Rochel’s graph-rewriting-lambdascope package (Haskell) is the only one. There is MaiaVictor’s optlam / absal (JS) and Vizaxo’s optal (Haskell) but they use Lamping’s algorithm which has brackets/croissants and more overhead. They’re still worth looking at for ideas on how to implement interaction nets though.

I was thinking that perhaps Kernel/Fexprs had an interesting solution to variable lookup, as the environment is passed explicitly, so I was reading through the thesis and got lost. I tried reading the paper and it also seems very long and full of Scheme-isms with not much on lambdas. The primitives are wrap and vau, somewhere in there we can insert optimal evaluation but I didn’t get to environments yet.