[Haskell-cafe] A model theory question

[Alexander Solla]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20101007/43e1dc45/attachment.html