alt Hacker NewsI would argue that it's pretty damn far from the Agda/Coq/lean world.
You really have to wrap your head around dependent types and _≡_. In my experience it was far more mind blowing than just FP.
I would argue that it's pretty damn far from the Agda/Coq/lean world.
You really have to wrap your head around dependent types and _≡_. In my experience it was far more mind blowing than just FP.
GADTs and a few of the wilder Haskell extensions sort-of go a bit in that direction.
But yes, you have to wrap your head around dependent types.