Patrick Browne | 23 Aug 14:25 2012
Picon

model theory for type classes

{-
I am trying to apply model theoretic concepts to Haskell by considering type classes as theories and instances as models.
Then the declaration of a sub-class specifies a signature morphism from the superclass to the subclass.
In case below the theories (classes) are signature only (no default methods) so a signature morphisms can be considered as a theory morphisms.
The only purpose of the code below is to explore the concepts of model expansion[1] and model reduct [2] in Haskell
I am not trying to improve or rewrite the code itself for any particular application.
Neither am I trying to find OO style inheritance semantics in Haskell type classes.
Rather, I am wondering if the last instance of Worker (commented out) demonstrates that there is no model expansion in this case.
That is, for theory morphism the theory(Person) => theory(Worker) we do not get (model(Person) sub-model model(Worker)).

If there is no model expansion could it be because of the constructor discipline, which only allows variables, and constructors in the LHS argument patterns.

[1] http://www.informatik.uni-bremen.de/~cxl/papers/wadt04b.pdf
[2] http://en.wikipedia.org/wiki/Reduct

-}

constant::Int
constant = (1::Int)
fun1::Int -> Int
fun1 (constant::Int) = 8

class Person i n | i -> n where
 pid :: i
 name :: i -> n

-- There is a signature/theory morphism from Person to Worker
class Person i n => Worker i n s | i -> s where
 salary :: i -> s
  
-- model(Person)
instance Person Int [Char] where
 pid = (1::Int)
 name (1::Int)  = ("john"::[Char])


-- We can say that a model(Worker) can use model(Person).
instance Worker Int [Char] Int where
-- Hypothesis: pid on the RHS shows that a model(Person) is *available* in model(Person) (reduct)?
  salary i = if i == pid then 100 else 0
 
-- instance Worker Int [Char] Int where
-- Hypothesis: The model of Person cannot be expanded to a model of Worker(no model expansion)
-- pid below is not inherited from Person, it is just a local variable
--   salary pid = 100




Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
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
Brent Yorgey | 23 Aug 17:02 2012

Re: model theory for type classes

On Thu, Aug 23, 2012 at 01:25:39PM +0100, Patrick Browne wrote:
> 
>    If there is no model expansion could it be because of the constructor
>    discipline, which only allows variables, and constructors in the LHS
>    argument patterns.

Indeed, a variable name as a pattern on the LHS of a function
definition has nothing to do with any names which might be in scope.
It is simply a pattern which matches anything.  I am not sure what (if
anything) this says about model expansions.

>    constant::Int
>    constant = (1::Int)
>    fun1::Int -> Int
>    fun1 (constant::Int) = 8

fun1 returns 8 for all inputs.  The fact that fun1's definition uses
the name 'constant' which happens to have the same name as something
in scope is irrelevant.  For example, this is precisely the same as the above:

constant :: Int
constant = 1
fun1 :: Int -> Int
fun1 foo = 8

-Brent
Patrick Browne | 23 Aug 19:02 2012
Picon

Re: model theory for type classes



On 23/08/12, Brent Yorgey <byorgey <at> seas.upenn.edu> wrote:


fun1 returns 8 for all inputs.  The fact that fun1's definition uses
the name 'constant' which happens to have the same name as something
in scope is irrelevant.  For example, this is precisely the same as the above:

constant :: Int
constant = 1
fun1 :: Int -> Int
fun1 foo = 8

-Brent
Yes, I am aware the semantics of Haskell is this situation.
I also know for every model of a subclass there must exist a model of the super-class.
I am just not sure whether there is a model expansion from the super-class model to the subclass model.
I am also unsure of the morphism from type variables in the class definition to actual types in instances and to the operations in the instance.
In a intuitive way I think that I understand these things, but not in a model theoretic way.

Thanks,
Pat



Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
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
wren ng thornton | 24 Aug 04:56 2012

Re: model theory for type classes

On 8/23/12 1:02 PM, Patrick Browne wrote:
> I am just not sure whether there is a model expansion from the super-class model
> to the subclass model.

If by "model expansion from..." you mean that there is a 
canonical/unique/special mapping from every superclass model to some 
subclass model, then the answer is no.

Consider, for instance, applicative functors and monads. We have the 
(idealized) type classes:

     class Functor a where...
     class Functor a => Applicative a where...
     class Applicative a => Monad a where...

However, there are strictly more Applicative instances than there are 
Monad instances. E.g., lists support an Applicative instance based on 
zip and an Applicative instance based on the cartesian product; however, 
only the latter of these can be extended to a Monad.

Well, technically, that's only if we assume the appropriate laws are 
part of the theories defined by the type classes. Without this 
assumption every type class can be instantiated at every type (for every 
method f, define f = undefined).

--

-- 
Live well,
~wren

Gmane