23 Aug 14:25 2012

## model theory for type classes

Patrick Browne <patrick.browne <at> dit.ie>

2012-08-23 12:25:39 GMT

2012-08-23 12:25:39 GMT

{-

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

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