Haskell is not really dependently typed. You can mimic it a bit, but you owe it to yourself to try reading through something in Coq or Agda (and maybe eventuall

Haskell is not really dependently typed. You can mimic it a bit, but you owe it to yourself to try reading through something in Coq or Agda (and maybe eventually Idris).