. > > 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
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
