Lambda the Ultimate

Andrei Alexandrescu describes (PDF) how to get safe functional programming in the otherwise imperative language D.

vs., say, monads.

Steven Kieffer, Jeremy Avigad, Harvey Friedman (2008). A language for mathematical knowledge management. Carnegie-Mellon tech. report CMU-PHIL-181.

The authors present a compact language for articulating mathematics, PST, which is syntactic sugar for an extension of Zermelo-Frankel set theory, DZFC, previously proposed by Harvey Friedman, which allows the naming of partially defined functions. The article gives some examples which show how for some mathematics, PST allows rather straightfoward expression. The article also gives some statistics gathered from an encoding of Suppes' Set Theory and Munkres' Topology, showing how PST allows a drastic compression compared to plain first-order ZFC.

Hello LtU. I've been lurking for a while, but this is my first post. I'm not really sure where it ranks on the scale from "how did you get through undergrad without reading X" to "do your own research, dude". I've tried googling everything I can think of, and reading breadth first from Glynn, Stuckey, and Sulzmann's paper "Type classes and constraint
handling rules", but I haven't gotten anywhere. Here goes:

In a Haskell-esque language with Haskell type classes, imagine a type generator, Set. This type generator requires that its argument be an instance of the Equality type class (because otherwise, how could it ensure that its elements are distinct). Set is also an instance of the Haskell Functor type class, because we can map over sets.

With theSet having type Set integer, and a map function with the usual type (namely, (Functor f) => (a -> b) -> F a -> F b), everything seems good. But here's my problem:

map (+) theSet

appears to have the type Set (integer -> integer).

KA-BOOM! Functions aren't in the Equality type class, and so we can't specialize Set at integer -> integer.

Does anyone know how to build a type inference / type checking algorithm that reports this error (statically)? If so, could you point me in the right direction?