I thought William Dunham's Journey through Genius: The Great Theorems of Mathematics did a great job of presenting the very real people and world behind several of results from history, from 400 BC (Hippocrates' Quadrature of the Lune) to recent-ish times (Cantor's transfinites).
There's discussions of feuds between mathematicians, how they used to keep results secret and literally duel over ideas (e.g. Cardano's chapter), the historical context and lives of the people who brought theorems into being (like Newton tasting his own chemicals as part of his alchemical research!), etc.
SuccessorML[1], 1ML[2], etc. are pretty close to this in spirit. I've been trying to keep up with the publications around the future of ML, but academic research moves kinda slowly. I'm hopeful we'll see a new definition of Standard ML this decade. I'd tend to agree SML is a great choice -- SML-1997 is still ahead of many languages that came well after it in both features and usability.
Journey through Genius: The Great Theorems of Mathematics - William Dunham
How to Bake Pi - Eugenia Chang
These are all sort of 'pop-math' books -- that is, they're more intended to spark a joy & love for math than teach rigorous mathematics. Great Theorems and A History of Pi include a lot of history (edit to add: in addition to covering the math involved!) -- did you know some mathematicians in history would duel over their theorems? That theorems were a carefully guarded secret instead of something you shared?
Introduction to Graph Theory is specifically intended as an introduction to mathematics for 'the mathematically traumatized'.
In my opinion, after reading these, if you've sparked a joy for the puzzles and fun of mathematics, then I would then suggest branching out into more formal presentations of them relevant to your interests... it's much easier to slog through a book on abstract mathematics when you receive from enjoyment from the puzzles presented.
> Edit: Can someone tell me... Is it necessary to have a new type system or could this be done with dependent types?
I played around with trying to implement an effect library (via the research) in dependently typed languages (Idris, Agda) and found type inference issues to be too much to work around. I found I was having to help the type checker along at every step -- explicit signatures on everything and, in Haskell terms, type/proof applications on function calls. On the other hand, I have found Koka -- until I started pushing the type system to its limits -- to require no hand-holding to figure out how to type its set of effects.
I am curious if a dependently-typed wizard could figure out an encoding to make these issues go away, but it was beyond my capability.
How does this compare to other effect-oriented languages like Koka, Frank, and Eff?
I've been doing some work with Koka lately, but I briefly looked into the other three (including Effekt) and it mostly came down to, 'Koka seems most active in development'[1] and 'Koka had the easiest to use documentation for me'[2], which are both kind of subjective ways of choosing between them rather than an objective comparison.
Koka is very interesting I must say. It's really cool to see how far they managed to make a functional language look imperative superficially, while being entirely functional under the hood and managing semantics via effects.
However, I believe they aren't really able to present a full imperative API to write programs in (or maybe they just haven't fully implemented the needed parts in the stdlib).
For example IIRC, the use of mut variables (internal mutability within a function and implicitly handled effect) and the related explicit heap effect don't seem to be able to share functions? And while they seem to work with entire objects the functions for mutations within arrays seemed limited the last time I tried Koka out. And everything being exposed only through the API presented some things were not possible to work around. I believe I was unable to write functions that mutated an array in place.
If anyone has had experience with Koka I would love to be proven wrong!
That said my initial point still stands - I think its an amazingly cool language and clearly a lot of interesting ideas are in it for sure.
So I would say this echoes my experience with it so far -- it is definitely a work in progress! However, I tend to approach Koka as if it were Standard ML with an effect system (up to a point), so the lack of a full imperative API hasn't been felt too much. I am more missing ad-hoc polymorphism than imperative tooling.
I am not sure I understand your comment about mut variables; my understanding is there are two types of mutable variables in Koka -- 'local' and 'ref'. 'local' is a locally mutable variable, and 'refs' are globally shareable. A 'ref' can be shared between functions, 'local' is just to give an imperative API using mutable variables. How 'local' works kind of confuses me so I tend to avoid it altogether in favour of local names (i.e. 'val' rather than 'var') and tail recursion (instead of loops with mutation). 'ref' seems quite usable to me and seems to reflect the SML usage of it.
I have felt the pain of a lack of an array, but I ported over an Okasaki data structure which has served well for a random-update, sequential data structure. Their data structures in the stdlib just have comments that say 'TODO': https://github.com/koka-lang/koka/blob/master/lib/std/data/m... that I am hoping are open to pull requests.
I'll just hijack this thread to ask a question about effect systems:
It seems to me that effects primarily have 2 uses:
1. Provide a controlled form of dynamic scoping (decouple usage and handling - allowing functions to be generic in their effects)
2. Create custom control flow with multiple resumes etc at the effect callsite
It feels to me that these are largely orthogonal ideas, but are always conflated in effect systems. Is there a reason for this? Are there examples of one without the other?
I think it goes back to the neverending quest to find ways of representing computation that allows of ease of composition, changing implementation details, eliminating classes of errors by construction, etc. Monads have had some success in this arena, but they have notable issues with composition; monad transformers help, but can become unwieldy in their own ways.
An alternative are effects, hypothetically allowing for ease in building programs as separate but composeable components which can then be freely mixed in or swapped out. In practice I have found working with effect systems in Haskell via libraries stresses the type system so much you end up with scoped type variables and type applications everywhere. My understanding is that the theory behind using effects to structure computations comes from category theory's Lawvere theories (see e.g. Pretnar's 2010 dissertation on https://github.com/yallop/effects-bibliography). Lawvere theories give rise to many monads (see Bartosz Milewski's article on it -- https://bartoszmilewski.com/2017/08/26/lawvere-theories/), but with nicer compositional properties.
This is where languages like Effekt, Eff, Frank, and Koka come in -- by writing the entire language and type system to support the theories, a lot of the pain of expressing it in Haskell can be avoided.
Their section on development tasks mentions fleshing out std and improving array/mutable reference programming, so I think it just hasn't been redone yet. It seems like they spent a lot of development time recently (with great success) working on foundational stuff like perceus/fbip and doing a major version bump, so std is pretty bare.
My backyard this year is an experiment in doing my best to encourage something that takes care of itself and is more supportive of local fauna. I laid down clover and what the local university's agriculture dept recommends for native-friendly grass seed. I've used no weed killer back there. I'm growing some ornamental grasses and flowers native to the area for decoration.
I feel like it's been nice. I think the clover is pretty, and I feel like we have many more butterflies this year than any of the previous years. The grass has been thriving. Dandelions don't seem to enjoy growing with clover very much, so there's less of them this year, although goosefoots seem more than happy to coexist with clover.
The clover has held up well to dogs, too, which has been a nice bonus.
I think I'd like to add some creeping thyme next year.
Nice.
We haven’t done as well as you with planting but took a different rack. A crowd near me was letting you rent beehives. They managed them and we got a lot of honey. This made a striking difference to trees and plants in our garden and our neighbours. I was cutting unripe fruit off trees to stop their branches snapping.
>Are you not also absorbed by your phone in other ways?
Honestly, no, and I feel very disconnected from modern culture as a result. I use my phone like a hitchhiker's guide to the galaxy: to have access to everything we know as humans at my fingertips, in my pockets, at all times.
Otherwise, I don't use it. That said, I have nothing against people using their phone for enjoyment, and there's nothing wrong with people smiling, laughing, and dancing. It's just not easy to relate to the obsession with applications like Instagram, Vine, TikTok, and so on.
I'm a fan of the "Digital Wellbeing" features that ship with newer phones.
I have a social media account which I check approximately biweekly and definitely considered myself someone who wasn't falling into the attention trap in my pocket. I only read HN, a few news sites, send texts, and play chess on my phone.
I was amazed to see just how much time I spent doing these things. Even if in some way how I'm using the phone is more virtuous or less problematic ("this hour-long article about the architecture of the classic XBox gratifies my curiosity, is informative and gives me more context with which to understand my field!"), that time and attention sink still comes at the cost of everything else in life.
In Standard ML, it would be a type error to do that specifically:
- if true then "abc" else 2.01;
stdIn:1.2-1.30 Error: types of if branches do not agree [tycon mismatch]
then branch: string
else branch: real
in expression:
if true then "abc" else 2.01
You would need to define a new data type to wrap them:
- datatype string_or_real = r of real | s of string;
- if true then s "abc" else r 2.01;
val it = s "abc" : string_or_real
Jan Corazza has some really great write-ups about writing bindings to SDL and writing a video game in Idris using them. The source is available on Github
There's discussions of feuds between mathematicians, how they used to keep results secret and literally duel over ideas (e.g. Cardano's chapter), the historical context and lives of the people who brought theorems into being (like Newton tasting his own chemicals as part of his alchemical research!), etc.