[sourceless]

Fantastic. First time I saw something similar to this was Edwin Brady’s recent demo of Idris 2. It’s quite amazing just how much of a program can be machine-written when the types are strict enough.

I hope holes & case-splitting get into many more languages.

[klysm]

I want my sum types damnit. Nothing like writing a case match over a sum type instead of fighting inheritance.

[carlmr]

Yes, once I got to know sum-types with match destructuring in F#, every other programming language that doesn't have them feels inferior. It's just such a practical idiom.