The actual maths is so much simpler. It's underappreciated how much of the mindboggling type-fu you see around is a waste-product of trying to jam CT into Haskell
Conversation
I wonder how it would look in Idris or Agda. 🤔
1
Me too.
1
Replying to
Although I kind of wish Agda libs had better ergonomics - they often seem needlessly creative notation wise 🙄 - but being able to forgo all the kind and constraint weirdness would be handy.