I saw a project for implementing an Elm repl in the browser on elm/projects. Evan recommended to build an repl for a simple lambda calculus first so I gave it a shot. Here’s how it looks:
I would love your feedback on the UI, design, and functionalities of the repl. My main question is how to implement the call by name evaluation strategy? Here’s my current attempt.
Looks beautiful! What do you do about UI hangs from long-running programs/nontermination? It seems like you have a 10k step limit. My approach is much less attractive, but it won’t freeze the UI when a computation runs too long (or diverges). Maybe we could combine forces… use your UI and my evaluator? I’ll be ready to publish the first version of my API in the next few days, I think.
CBN should work the same as CBV, except you never bother to evaluate arguments. That is, the isValue t2 on L243 shouldn’t need to happen at all.
Your implementation seems to use explicit substitutions, which is the clearest way to go and most obviously tied to the theory. Abstract machines tend to be much more efficient, though, and their “step”-based approach works well with my approach to suspending computation.
The Krivine machine is a very nice way to implement CBN. Call-by-need is a little bit trickier: you need to be careful to only evaluate things once. Olivier Danvy’s 2003 paper A Rational Deconstruction of Landin’s SECD Machine offers abstract machine models of a variety of evaluation strategies.
Thanks. Your approach is definitely more practical. I literally pulled my implementation out of the Types and Programming Languages book… I will be happy to work with you to combine the UI and the evaluator. It seems that you have a typed lambda calculus so I’m thinking about providing different flavors.
Sounds great. I’ll round out my STLC example with one more implementation (using the Fueled monad), and then we can work out how to integrate the suspendable computations into your excellent REPL interface.
As for the typed vs. untyped question: the evaluators will be identical, but it probably makes sense to just use plain untyped lambda calculus. I probably shouldn’t have used STLC as my demo program, since every STLC program terminates! (Take that, halting problem.) It should be easy enough to offer some kind of switch to turn off the type checker… but for simplicity’s sake, we should just use untyped LC to start.
Since I’m using it as a learning tool myself, I’m trying to implement type support and potentially extensions like sum and product types. But it won’t be an issue because we can just create a new branch or fork of the repl for experimenting with the integration with your engine.
Sounds good. I’m mostly interested in the suspendable computations, but I’m happy to help with whatever PL implementation questions you might run into.
I tried looking for type theory learning resources for beginners but TAPL is the only one that suits my level. I did find a good collection fo resources on learn-tt but most of them are papers and in-depth books. Do you know any online classes, video lectures, course notes, or any similar resources for beginners? Ideally they should be at or below TAPL level with a focus on practice. Thanks.
You might like my course notes from CS 131, the PL course I’ve taught a few times now. It doesn’t go past the STLC and is pretty implementation focused. I’d rate it as decidedly less difficult than TAPL, which I assign as an optional, supplementary textbook.
Shriram Krishnamurthi’s PLAI book is another nice approach. It’s not written from quite the same formalist perspective as Benjamin Pierce’s TAPL. (Disclosure: Shriram was my undergraduate advisor, and Benjamin was my PhD advisor.)
Matthias Felleisen and Matthew Flatt’s Programming Languages and Lambda Calculi is another well grounded, theory-based approach, with an emphasis on abstract machines.
Just wanted to say thank you to @mgree for these resources as well. I’ve been out of college for some time but am really interested in PL topics. It’s been hard to find resources that are both thorough and written for someone, like myself, who isn’t familiar with all of the terms or symbols that are taught in college.
Quick update: I released my mgree/trampoline package. I don’t have time just now to try adapting your nifty REPL, but would be game to consult if you wanted to give it a whack. I wrote up a monadic evaluator that’s probably the closest to the style you’ve been writing in.
