21 Mar
2012
21 Mar
'12
10:19 a.m.
.
On a side note, if we consider typeclasses as predicates on types, then
At present we can easily express different flavors of conjunction, but expressing disjunction is hard. And that's why the Prelude can cause
(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. 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