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/
Sorry for the delay in responding.
-Alex
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
