[Haskell-cafe] A model theory question

[Alexander Solla]

  On 09/26/2010 01:32 PM, Patrick Browne wrote:
> Hi,
> Below is an assumption (which could be wrong) and two questions.
>
> ASSUMPTION 1
> Only smaller models can be specified using the sub-class mechanism.
> For example if we directly make a subclass A =>  B then every instance of
> B must also be an instance of A (B implies A or B is a subset of A).
> Hence, type classes cannot be combined using sub-classing to provide
> specifications of bigger models.
I'm not sure what you mean by "models" and "subclass mechanism".  For 
example, any set is a model of the first order logic.  Presumably, we 
can "subclass" (i.e., add axioms to) from FOL into Peano Arithmetic.  
That cuts down on models that satisfy the axioms from "any set" to... 
well, the models of arithmetic (that is, the natural numbers, the class 
of ordinals less than the first uncountable ordinal, etc).  A finite set 
is a model of FOL.  But no finite set is a model of PA.
> QUESTIONS
> 1) If assumption 1 is correct, is there a mechanism whereby the module
> system can be used to construct bigger models?

Bigger how?  Under logical implication and its computational analogue?  
That is to say, do you want the model to be more SPECIFIC, describing a 
smaller class of objects more richly (i.e, with "more" logical 
implications to be made) or do you want the model to be more GENERAL, 
and contain the less specific submodels?  This is how "forcing" works.

> 2) If there is such a mechanism does it involve type classes or is it a
> module only solution?
>
>
>
> Regards,
> Pat
>
> This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe