[Haskell-cafe] Are there arithmetic composition of functions?

Don Stewart dons00 at gmail.com
Wed Mar 21 15:19:52 CET 2012


.
>
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120321/31f3b8aa/attachment.htm>


More information about the Haskell-Cafe mailing list