Any sophisticated enough type system contains an ad-hoc, informally-specified, bug-ridden, slow implementation of half of Prolog.
Seems to not be very bug-ridden either. But maybe somebody should code a non-backtracking operator extension for GHC. This way, next time he could claim Haskell is a dynamically typed, interpreted, lazy and not-pure language.
Haha, that's a good one. Haskell, unlike SML, is _not_ formally specified. If only, if only... sobs
I do think datalog semantics composes way nicer than prolog though.
I think some of the type class stuff was formalized in the papers on HM(X) , though the combination of extensions in this post hasn't. But perhaps should be on the table for formalization.