Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

I'd like to see a sample of this if it would be possible. Through the years I've been tinkering with new odd Lisp dialects based on ideas I've picked up along the way, and this might be another thing to test out.

Haskell-like languages can look vaguely Lisp-like when fully parenthesized due to juxtaposition meaning function application, like in lambda calculus. They also tend to have "$" to open a group that self-closes at the end of the expression (implemented as a very low precedence right-associative operator), which can greatly clean things up. It sounds like your "|". Haskell itself has a little-used "literate comments" mode where everything not prefixed with > is a comment: https://www.haskell.org/onlinereport/literate.html

Mathematica leaves something to be desired when it comes to being a tree rewrite language. I do find it to be very useful for some of the knot theoretic calculations I'm interested in (for example, the language makes it fairly straightforward to work with the braided monoidal category of tangles up to the HOMFLY relations! and display morphisms as linear combinations of pictorial representations of basic tangles!) But... I'd like to be able to more easily compose different tree languages together without worrying that my rewrite rules will conflict with the standard library in unexpected ways.

Recently I've been learning Lean, which has been pleasantly ergonomic (yet still frustrating -- proof assistants are still in their adolescence). It's been making me think that languages of the future really need a built-in system that let you prove the correctness of your programs. This can help with basic things like subtypes, array bounds checking, and so on, that compilers can struggle with because they get little help from the user. Also, all the infix notation actually seems to improve legibility and ergonomics, though this would not be the case if Lean did not have an LSP server that lets you query for the definition of pretty much anything, including bespoke notation. It would be interesting to have a Lisp built on maybe dependent type theory where you can make sure your programs satisfy any property you might want, adding types and proofs to your program in an incremental way.

Another interesting thing about Lean is how it embraces a certain kind of metaprogramming, but in the form of a semi-inscrutable write-only language of "tactics". The UI presents the objects that you have and the objects that you want to have, and the various tactics help you perform steps to close the gap. This is more useful for proofs than programs (yes, proofs are programs, too, but they have some minor differences due to the propext axiom), but it makes me wonder if there is something in here that could be useful for writing programs in general.

(By the way, Macaulay 2 has been helpful to have around every once in a while when I need to do some basic calculations with modules. I was impressed how the language seemed to be designed to appear mathematician-friendly.)



Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: