saityi

Even if open source operating systems comply and add such a feature, what's to stop individual people from removing this and blocking the API requests before they install the OS? Or providing dummy responses? They're open source, after all.

Is the government going to require some sort of automated checks that verify every person who connects to the internet has this API on their OS and go after individuals that aren't in compliance?

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.

[1] https://github.com/SMLFamily/Successor-ML

[2] https://people.mpi-sws.org/~rossberg/1ml/

Introduction to Graph Theory - Richard J. Trudeau

A History of Pi - Petr Beckmann

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.

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.

I'd missed those -- thank you!

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.

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.

[1] E.g. https://github.com/effekt-lang/effekt had its last commit back in June; https://github.com/frank-lang/frank last commit last year; but https://github.com/koka-lang/koka last update was Oct 15. Effekt seems semi-active, at least, compared to Frank. While stability is good, I wouldn't expect it in a language actively being used for research.

[2] Comparing https://koka-lang.github.io/koka/doc/book.html and https://effekt-lang.org/docs/ and https://www.eff-lang.org/learn/

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.

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.

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

    - 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

https://flowing.systems/2020/01/13/a-game-in-a-pure-language...

https://flowing.systems/2020/04/13/a-game-in-a-pure-language...

https://github.com/corazza/game-idris

There's even a page in the Idris 2 docs with updates to the book for Idris 2 -- https://idris2.readthedocs.io/en/latest/typedd/typedd.html

The book is otherwise still totally relevant for Idris 2 and is a great read & introduction to dependent types.

My take: sum and product types exist in various type theories (enums with their elimination rule being pattern matching). Some of the first type theories to feature them were for the lambda calculus, which functional programming is based on. As a result, they've been ubiquitous in functional programming, and have become associated with it heavily.

In case anyone is curious about [1], there is a paper called Lightweight higher-kinded polymorphism -- http://ocamllabs.io/higher/lightweight-higher-kinded-polymor... -- that goes into some of the possible encodings.

Unfortunately, on the Canadian JustWatch, I find the answer is frequently 'this is totally unavailable for you to legally view or purchase digitally in Canada', at which point I end up pirating it.

Now complete -- thanks again for the suggestion! I never liked having to include that bit of JS.

No reason at all; I think I will go look into doing that now. I think it should be a quick fix :)

Thank you for the idea!

I tried to apply the philosophy of keeping things as simple as possible while writing https://saityi.github.io/sml-tour

Initially, I wanted no JS and for it to look good in a text-based browser like links, too, but I've strayed from that a bit. Syntax highlighting of the code examples was easiest with a javascript include, and the TOC is a mess hidden by CSS, so it looks particularly egregious in text-based browsers.

The website is still functional without JS and text-only, though, and without the favicon and syntax highlighting it comes in at ~4kb to load a page, which I'm happy with; with them it's closer to 40kb, which isn't the worst.

The first article that comes to mind for me is Programming Sucks, although it's not quite the same as your description.

https://www.stilldrinking.org/programming-sucks

It works best if you follow up the compiler assistance with a human-readability pass. Use the techniques in this post to guide you to a solution, which I find immeasurably helpful, then rewrite it by pulling it out piece by piece to make it readable with let/where blocks that describe the various steps.

Paul Snively (the author of the linked reddit post) also gave a great talk entitled 'Typed FP on the Job - Why Bother?' at LambdaConf a couple years back, that spoke strongly to me:

https://www.youtube.com/watch?v=8_HsFrXhZlA

And now you can do the most important thing you can do with any piece of code... stop thinking about it! Go home! Pet the cat! Watch House with the wife! ... I love Friday deployments ... you know why? Because I know what my code is going to do before it runs!

TIL. Pretty neat to check out:

https://github.com/clojure/clojure/blob/89fc0caa43811c7dfcb4...

The last time I gave Mill a shot, I couldn't find a way to authenticate into private artifactory repositories, which made it kind of a nonstarter. Do you know if this has since been added?

Scala is interesting in this sense; I'd consider it to be an ML-like language. It attempts to unify object systems and module systems, and they are fairly first class in Scala. Modules (objects) can be used as normal values; you can encode functors as functions or classes as needed; signatures (traits) are usable as values to some degree, too.

Furthermore, path-dependent types allow Scala to unify modules and objects, so that the same language constructs can be used to specify the overall structure of a program as well as its implementation details. The unification of the module and term languages is witnessed by the following comparison with the ML module system: Scala objects correspond to ML modules, classes to functors, and interfaces to signatures [Odersky and Zenger 2005].

https://arxiv.org/pdf/1904.07298.pdf

The only thing I find clunky about SML syntax are infix operators, since fixity specifications aren't exported.

http://mlton.org/InfixingOperators

Otherwise, I love SML syntax, and would be curious to see the answer to this, too. I find it refreshingly simple and consistent. Is it that it uses 'let ... in ... end' and such rather than whitespace or brackets?

I like to use SML/NJ for development and experimentation, and MLton for final compilation.

SML/NJ is a really nice development environment, and using a different compiler like MLton or Poly/ML for the final compilation forces you to use the more common, standard subset of ML rather than implementation-specific features.

It is, and it still exists... it's also a brand new compiler, instead of one with nearly 30 years of development on it, and a brand new ecosystem, instead of having the massive amount of hours that Haskell has in it. Idris is really nice imo, but Haskell+Dependent Types will likely be usable sooner.

There is an 'Idris 2' being developed, too (https://github.com/edwinb/Idris2), which is an entirely new compiler with a new type theory (although not entirely dissimilar), which just makes it even harder to use for real things (again, IMO).

You are correct, and I will fix it. The goal here was to encourage recursion and assuage fears of recursion coming from other languages: if I remember correctly, Standard ML does define semantics around 'expansive expressions' which make them /safer/ than I think most imperative programmers (my targeted audience) would expect, but this particular example would throw an exception.

To fix it, I will rewrite this section to say that the standard requires optimising /tail-recursive/ calls away, and modify the example to be iteratively recursive, but I'd still like to assuage fears of recursion in the tour. The 'while' loop in SML is actually just a derived form, and is rewritten to recursion; there is no looping in the language. Do you have any suggestions for rewording?

This is a work in progress that I was looking for feedback on :) Thank you! If you see anything else fishy, please let me know.