On Sep 30, 2010, at 1:39 AM, Patrick Browne wrote:

I think my original question can be rephrased as:
Can type classes preserve satisfaction under the the expansion sentences
(signature/theory morphisms inducing a model morphism).

According to [1] expansion requires further measures (programming?)
which you demonstrated. But this raises are further question. Does
Haskell’s multiple inheritance represent a model expansion where the
classes in the context of an instance are combined in the new bigger model?

In principle, the answer is yes (I think). But I kept running into walls when I tried. It is almost as if there is "too big" a gap to be filled between compile-time and run-time. At least for the approaches I tried.

I have two suggestions though. First, monadism is a great way to approach this problem from a run-time level. Indeed, a monad is an interpreter, which comes with the associated notions of a free algebra/model and the like. Injecting a new axiom amounts to creating a new monadic action. Monad transformers can do lifting and lowering in a fairly straight forward way.

Another suggestion is to check out the OOHaskell paper. I know they use type level forcing to get stuff done, but I guess they used a different cluster of extensions than I tried. http://homepages.cwi.nl/~ralf/OOHaskell/