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?
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.
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!)
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.
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?
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.
14 comments
[ 3.5 ms ] story [ 36.2 ms ] thread[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
https://m.youtube.com/watch?v=iqlxsSrd-M4
“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.”
"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'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...