I spent a couple hours procrastinating something with that book just a while ago, but couldn’t really stay focused for long enough to get to anything interesting and started tinkering with Idris instead. I should probably go back to it at some point, maybe after I can grok Reasoned and Kanren.

I think pausing a book because it made you want to do something practical with the knowledge is perfectly valid. full disclosure I’ve never gotten past the 1/3rd point in The Little Typer, but every time I’ve tried I’ve internalized more of dependent types and brought that knowledge into my other work.

The Reasoned Schemer is awesome too! I’ve always wanted to use Kanren in a real project. weirdly, what I learned from that book came in handy when I tried my hand at game dev with an ECS, which works a lot like a high-performance inference engine with a couple of limitations on how queries are structured.

I made it sound cooler than it is. By “implemented” I mean I grew a horrid pile of nested match statements in Rust to recreate eval from the venerable MacCarthy paper. It doesn’t even have a parser yet, unless Cons(Atom(format!("quote")).into(), Cons(Atom(format!("foo")).into(), Nil.into()).into()); passes for syntax nowadays.

hey, the first lisp eval used punched cards made by a guy named Slug over McCarthy’s objections. the best bits of lisp aren’t the substrate, they’re the language you build on top of it.

now I want to start that Lisp keyboard firmware project