[chamomeal]

Super interesting! Thanks for the link.

Would you say Lean is a somewhat learnable language for somebody who only has cursory exposure to functional programming and static types? I’ve almost exclusively used typescript for the last few years, except for some clojure in the last few months.

Sometimes I find a neat language, but my very TS-oriented brain has a hard time getting into it.

[jonlong]

I would say dependent types are going into the deep end; unless you have a real need to prove things, it may be hard to see the motivation to learn such abstractions.

In between ad hoc types like TypeScript and dependently-typed languages like Agda, Coq/Rocq, and Lean are well-typed, polymorphic (but not dependent) languages like OCaml, F#, or Haskell ("ML family" or "Hindley-Milner" are related terms). Those are what I'd suggest checking out first!

[nxobject]

If you’d like to dive into the deep end and learn a “we tried to make as much type system power available as conceptually simply and elegantly as possible” language, Agda [1] is a very fun language to fool around with. It’s superficially a Haskell-like, but you’ll likely only really learn it as a toy that nevertheless blows your mind… like Prolog etc.

The first thing I tried to do after learning all the basic syntax is write a function f: Nat —> Set (from numbers to types), and then stick it in a function signature (i.e. g: f (3).)

[1] https://people.inf.elte.hu/divip/AgdaTutorial/Index.html