4 ms·

Domain-Specific Languages of Mathematics

75 points by adamnemecek 4y ago

adamnemecek 4y ago
Here's the PDF https://github.com/DSLsofMath/DSLsofMath/blob/master/L/snapshots/DSLsofMathBook_snapshot_2022-12-26.pdf https://github.com/DSLsofMath/DSLsofMath/blob/master/L/snaps...
mncharity 4y ago
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/book-Z-H-3.html https://groups.csail.mit.edu/mac/users/gjs/6946/sicm-html/bo... https://news.ycombinator.com/item?id=19765019 https://news.ycombinator.com/item?id=19765019 et al (including haskell porting) [2] https://mitp-content-server.mit.edu/books/content/sectbyfn/books_pres_0/9580/9580.pdf?dl=1 https://mitp-content-server.mit.edu/books/content/sectbyfn/b... https://news.ycombinator.com/item?id=7884551 https://news.ycombinator.com/item?id=7884551
- le-mark 4y ago
  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 https://m.youtube.com/watch?v=iqlxsSrd-M4
gexaha 4y ago
Won't it be easier to teach/use Lean?
- epgui 4y ago
  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.
  - epgui 4y ago
    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.”
  - deterministic 4y ago
    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?
davidthewatson 4y ago
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-bird-obituary https://www.theguardian.com/technology/2022/jun/03/richard-b... and the post on hacker news: https://news.ycombinator.com/item?id=31619966 https://news.ycombinator.com/item?id=31619966
Koshkin 4y ago
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.
- syngrog66 4y ago
  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...
- deterministic 4y ago
  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.
curiousgibbon 4y ago
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?
- kisonecat 4y ago
  It looks like the text uses the more natural R R a few pages later.
  - curiousgibbon 4y ago
    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.

75 points by adamnemecek 4y ago

Here's the PDF https://github.com/DSLsofMath/DSLsofMath/blob/master/L/snapshots/DSLsofMathBook_snapshot_2022-12-26.pdf https://github.com/DSLsofMath/DSLsofMath/blob/master/L/snaps...

mncharity 4y ago

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/book-Z-H-3.html https://groups.csail.mit.edu/mac/users/gjs/6946/sicm-html/bo... https://news.ycombinator.com/item?id=19765019 https://news.ycombinator.com/item?id=19765019 et al (including haskell porting) [2] https://mitp-content-server.mit.edu/books/content/sectbyfn/books_pres_0/9580/9580.pdf?dl=1 https://mitp-content-server.mit.edu/books/content/sectbyfn/b... https://news.ycombinator.com/item?id=7884551 https://news.ycombinator.com/item?id=7884551

le-mark 4y ago
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 https://m.youtube.com/watch?v=iqlxsSrd-M4

gexaha 4y ago

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

epgui 4y ago
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.
- epgui 4y ago
  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.”
- deterministic 4y ago
  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?

davidthewatson 4y ago

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-bird-obituary https://www.theguardian.com/technology/2022/jun/03/richard-b... and the post on hacker news: https://news.ycombinator.com/item?id=31619966 https://news.ycombinator.com/item?id=31619966

Koshkin 4y ago

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.

syngrog66 4y ago
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...
deterministic 4y ago
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.

curiousgibbon 4y ago

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?

kisonecat 4y ago
It looks like the text uses the more natural R R a few pages later.
- curiousgibbon 4y ago
  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.