saityi

4 miesiące temudiscuss

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?

saityi

4 lata temudiscuss

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.

saityi

5 lat temudiscuss

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/

saityi

5 lat temudiscuss

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.

saityi

5 lat temudiscuss

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.

saityi

5 lat temudiscuss

I'd missed those -- thank you!

saityi

5 lat temudiscuss

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.

saityi

5 lat temudiscuss

> 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.

saityi

5 lat temudiscuss

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/

saityi

6 lat temudiscuss

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.

saityi

6 lat temudiscuss

>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.

saityi

6 lat temudiscuss

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

saityi

6 lat temudiscuss

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

saityi

6 lat temudiscuss

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.

saityi

6 lat temudiscuss

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.

saityi

6 lat temudiscuss

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.

saityi

6 lat temudiscuss

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.

saityi

6 lat temudiscuss

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

saityi

6 lat temudiscuss

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!

saityi

6 lat temudiscuss

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.

Submissions

A Tour of Standard ML

comments