Hacker News Reader

Comment by Myrmornis | Hacker News Reader

This book's amazing. I've only tried to understand the first few chapters so far but I found the basic idea -- reformulating the Euler-Lagrange equations in lisp, and using Spivak's alternative notation for differential calculus -- to be extremely illuminating and even inspiring when going back and trying to really make sense of (advanced) undergrad calculus.

OK, so here's my question: the scheme is great and all, but wouldn't this really benefit from a statically typed language with a rich type system? I think it would be really interesting to try to make the computations at the type level correct as well as at the runtime level. Obvious candidates I guess are Haskell/OCaml etc, or one of the theorem-proving languages (out of my depth here, but Lean/Coq etc).

I have said this before...another HN thread on SICM: https://news.ycombinator.com/item?id=21460106

View on HN

I have been interested in doing this for a long time, and have thought about doing it in Haskell. It would be a lot of work, and some of the type decisions that would be needed would probably complicate the UX of the software (the automatic differentiation of functions of various shapes would make typing the D operator interesting; I think it would force all real-valued functions of a real variable to look like they were working in a vector space of dimension 1, or the inconsistency would be maddening). SICM's software also does a lot of "lowering" of types, so 0 (zero) is kind of a universal additive identity, but in a strongly typed system you'd need zeros of many different kinds and it might be that once all this was finished there was too much "wrapping" left visible and the scientific investigations in the SICM spirit would lose some of their charm. I guess that's a long-winded way of saying that there are lots of type puns in mathematical notation that are useful affordances even if they are slightly abusive.

Thanks that was very interesting to hear your thoughts. If you do ever decide to work on this again, I'd be interested to know and probably in helping. Others in these threads have expressed interest too. But yes, it does sound like rather a lot of work for a slightly esoteric cause. My contact details are in my profile.

Making the computations type-level correct would be really neat! That'd be a huge improvement!

I don't think the language needs to be statically-typed to do that. I could easily extend Scheme or Python to support that. All you need to do is make sure that if you add 5 meters to 5 seconds, you raise an exception. There's no reason that exception has to happen at compile-time.

Going Scheme -> typed Scheme is a manageable step which I could envision taking a few weeks of hard work. Changing languages would be an incredible amount of work (especially with things like the JIT compiling MIT-Scheme does for SICM, where you can symbolically derive equations of motion, compile them, and run them as high-performance native code).

I've been using programming to teach kids math and physics, and the lack of units IS a serious pedagogical problem. I think that's doubly true here.

I think you're really onto something.

I have done the translation from Scheme to Clojure which raises the possibility that some of the typing could be done gradually with spec; I haven't worked with typed scheme. There's a lot of code in the simplifier which is designed to work with S-expressions containing symbols. Changing them to work with an enriched type carrying unit information would be a big undertaking

I have been thinking about doing it in OCaml for a while, but it will take an insane amount of work and this always put me off

Reply on news.ycombinator.com