[Haskell-cafe] A model theory question
ajs at 2piix.com
Thu Oct 7 20:26:54 EDT 2010
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
> (signature/theory morphisms inducing a model morphism).
> According to  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
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 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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe