Domain-Specific Languages of Mathematics | Hacker News Reader

Domain-Specific Languages of Mathematics

github.com

75 pointsadamnemecek14 comments

Reminds me of Structure and Interpretation of Classical Mechanics[1] and Functional Differential Geometry[2] using Scheme.

[1] https://groups.csail.mit.edu/mac/users/gjs/6946/sicm-html/bo... https://news.ycombinator.com/item?id=19765019 et al (including haskell porting) [2] https://mitp-content-server.mit.edu/books/content/sectbyfn/b... https://news.ycombinator.com/item?id=7884551

I really love this presentation about the ideas around these by Sussman, I need to rewatch it;

https://m.youtube.com/watch?v=iqlxsSrd-M4

Here's the PDF https://github.com/DSLsofMath/DSLsofMath/blob/master/L/snaps...

I haven't read much of the book but find the early material defining complex numbers as a sum type that's either R R I or R I R where R is some type representing the reals and I is some sort of unit type with one inhabitant rather strange. As someone who knows a little math and a little Haskell, this example seems contrived, misleading and weird from both angles. Should I read on or give up?

It looks like the text uses the more natural R R a few pages later.

Yes, but I'm dubious of the value of a learning resource this indirect. I waded through about 5 versions of the complex numbers, each more natural than the last and gave up on the book because it didn't seem like any reason for the tumultuous journey though weird models of the complex numbers would be elucidated. I'm now trying to crowdsource motivation to continue.

I'm out of my depth here, but it's worth noting:

"The poet laureate of functional programming" from the guardian:

https://www.theguardian.com/technology/2022/jun/03/richard-b...

and the post on hacker news:

https://news.ycombinator.com/item?id=31619966

I find Lisp more than any other programming language suited to be the host language for a DSL. It is also easy to represent hierarchical and flat data formats with it.

reasonable

I've used Python a few times as the raw material out of which I craft a DSL-like thing. esp if I need a Frankenstein mix of executable code and data, blurring line with an API

I mean, yes, ostensibly I use Lisp. but at the last minute I just bang it out in Python (the Perl of 2023? ha!)

obligatory XKCD...

In this case LEAN/Agda/Coq/Idris would be better choices since it allows you to prove mathematical theories. And those languages all have support for sum types, arguably more useful than S-expressions IMHO.

Won't it be easier to teach/use Lean?

Why Lean? I know Lean is interesting, but there's also Coq, Idris, Agda... And as others have pointed out, this would probably be a good use case for a lisp too.

Update: I just received my copy of the book, and at the bottom of page 4 the authors write:

“It would be an interesting endeavour to port the code from Haskell to a language with an even stronger type system, like Agda, Idris or Lean. The authors would welcome contributions in this direction.”

LEAN/Coq/Idris/Agda allow you to prove mathematical theories out of the box. Lisp not so much. Unless there is a Lisp library that gives you the power of Dependent Types and/or Refinement Types?

Reply on news.ycombinator.com