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” lang

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 https://people.inf.elte.hu/divip/AgdaTutorial/Index.html