21 Mar
2012
21 Mar
'12
10:19 p.m.
.
On a side note, if we consider typeclasses as predicates on types, then
(especially with the extensions enabled) the type system looks extremely like a obfuscated logic programming language.With existential types it even starts to look like a first-order thereom prover.
At present we can easily express different flavors of conjunction, but expressing disjunction is hard. And that's why the Prelude can cause problems here.
See http://www.cse.chalmers.se/~hallgren/Papers/wm01.html It gets even more fun with GADTs and, particularly, type families, which are explicitly designed with type level proofs in mind -- Don