<p> Can we consider a Haskell class as a loose signature-only-specification (denoting a theory) and an instance as an implementation (denoting a model)? In the example below the specification of the class $\mathcal{BUILDING}$ is textually smaller than the specification of the class $\mathcal{HOUSE}$, though in Haskell  $\mathcal{BUILDING}$ is a super class of  $\mathcal{HOUSE}$. Is there a Galois correspondence between a Haskell class hierarchy and  its instance hierarchy?
</p>

<p><p> --General Idea-- </p></p>

<p>$\small\mathcal{Theory}\subseteq\mathcal{Theory'}\iff\mathcal{Model'}\subseteq\mathcal{Model}$</p>

<p><p> --A specific  example with Haskell class-to-instance relation -- </p>
<img src="https://i.sstatic.net/lQ4Wm.png" width="160" height="100"><a href="https://i.sstatic.net/lQ4Wm.png" rel="nofollow noreferrer">1</a></p>

<p>$\small\mathcal{class(BUILDING)}\subseteq_{C}\mathcal{class(HOUSE)}\iff\mathcal{instance(HOUSE)}\subseteq_{I}\mathcal{instance(BUILDING)}$</p>

<p><p> ---------------- </p></p>

<pre><code>
data House = House deriving Show
data Building = Building  deriving Show

class BUILDING building where
 -- specify the behavior of buildings here, if any
 supportRoof :: building -> String

class BUILDING house => HOUSE house where
 -- specify additional behavior of houses here, if any
  live::house -> Bool

instance BUILDING Building where
-- specify how the type Building implements the behavior of type class BUILDING
  supportRoof b = "BUILDING.Building"
-- A particular b which is a BUILDING.Building.particular can support a roof

instance BUILDING House where 
  supportRoof h = "BUILDING.House"
-- A particular h which is a BUILDING.House.particular can support a roof

instance HOUSE House where
-- specify how the type House implements the behaviour of type class HOUSE
   live h   = if ((supportRoof h) == "BUILDING.House") then True else False
-- An particular h HOUSE.House.particular can support a roof in exactly the same way as BUILDING.House.particular can.

instance HOUSE Building where
-- specify how the type Building implements the behaviour of type class HOUSE
   live b   = if ((supportRoof b) == "BUILDING.Building") then True else False
-- An particular b HOUSE.Building.particular  can support a roof in exactly the same way as BUILDING.Building.particular can.

</code></pre>

CC BY-SA 3.0
2013-08-05T14:25:01.030Z
Before it even makes sense to answer this question you should explain what your categories are. What are the morphisms?
Andrej Bauer
CC BY-SA 3.0
2013-08-05T15:39:32.240Z
My earlier [link](http://cstheory.stackexchange.com/questions/18215/is-there-a-model-theory-for-haskell-type-classess) describes the categories and morphisms.
Pat
CC BY-SA 3.0
2013-08-05T15:46:24.347Z
The categories are signatures, sentences and models. I think the morphisms might be sub-class and sub-model. My earlier [link](http://cstheory.stackexchange.com/questions/18215/is-there-a-model-theory-for-haskell-type-classess) describes the categories and morphisms that I think might be appropriate for classes and instances.
Pat
CC BY-SA 3.0
2013-08-06T16:41:13.590Z
Sorry, this looks a bit confused to me. The question you link to does not clearly state what the objects and the morphisms are. Your best bet is to explicitly describe the category in question right here. Also, what makes you think type classes have a sensible categorical interpretation?
Andrej Bauer
CC BY-SA 3.0
2013-08-07T06:41:13.750Z
What is your definition of a Galois correspondence? Have you seen Peter Smith's notes? www.logicmatters.net/resources/pdfs/Galois.pdf‎
Vijay D
CC BY-SA 3.0
2013-08-07T14:17:32.173Z
I was wondering if there is a correspondence between the partial order defined in the class structure and 'some' order on the implementations. Apparently there is not, so I withdraw the question. Thanks for both responses.
Pat
CC BY-SA 3.0
2013-08-07T22:12:03.860Z
@Pat, that is not the conclusion I would draw. There may well be an order and mappings that constitute a Galois correspondence. The few people who have read your question do not have an answer.
Vijay D
CC BY-SA 3.0
2013-08-10T22:58:33.123Z
@Pat: you made the wrong conclusion. We cannot answer your question because it is not precise enough to make sense. I repeat, how do you define your hierarchies of type classes and instances? I can see that for type classes you could use some sort of record subtyping, but what is the preorder on the instances?
Andrej Bauer
CC BY-SA 3.0
2013-08-15T10:01:50.570Z
I do not think that I can identify a hierarchy of instances, which I think leaves the question imprecise. My research  involves comparing type classes to modules in algebraic specification languages such as CafeOBJ or Maude. In these languages there is a Galois connection between classes of models and sets of sentences. I am taking type classes to be signature only theories.
Pat
<semantics><model-theory>
Is there a Galois correspondence between a Haskell class hierarchy and its instance hierarchy?
Pat
# Is there a Galois correspondence between a Haskell class hierarchy and its instance hierarchy?

(Asked by: username_0 on 2013-08-04)

Can we consider a Haskell class as a loose signature-only-specification (denoting a theory) and an instance as an implementation (denoting a model)? In the example below the specification of the class $\mathcal{BUILDING}$ is textually smaller than the specification of the class $\mathcal{HOUSE}$, though in Haskell  $\mathcal{BUILDING}$ is a super class of  $\mathcal{HOUSE}$. Is there a Galois correspondence between a Haskell class hierarchy and  its instance hierarchy?

 --General Idea-- 
$\small\mathcal{Theory}\subseteq\mathcal{Theory'}\iff\mathcal{Model'}\subseteq\mathcal{Model}$
 --A specific  example with Haskell class-to-instance relation -- 
1
$\small\mathcal{class(BUILDING)}\subseteq_{C}\mathcal{class(HOUSE)}\iff\mathcal{instance(HOUSE)}\subseteq_{I}\mathcal{instance(BUILDING)}$
 ---------------- 

data House = House deriving Show
data Building = Building  deriving Show

class BUILDING building where
 -- specify the behavior of buildings here, if any
 supportRoof :: building -> String

class BUILDING house => HOUSE house where
 -- specify additional behavior of houses here, if any
  live::house -> Bool

instance BUILDING Building where
-- specify how the type Building implements the behavior of type class BUILDING
  supportRoof b = "BUILDING.Building"
-- A particular b which is a BUILDING.Building.particular can support a roof

instance BUILDING House where 
  supportRoof h = "BUILDING.House"
-- A particular h which is a BUILDING.House.particular can support a roof

instance HOUSE House where
-- specify how the type House implements the behaviour of type class HOUSE
   live h   = if ((supportRoof h) == "BUILDING.House") then True else False
-- An particular h HOUSE.House.particular can support a roof in exactly the same way as BUILDING.House.particular can.

instance HOUSE Building where
-- specify how the type Building implements the behaviour of type class HOUSE
   live b   = if ((supportRoof b) == "BUILDING.Building") then True else False
-- An particular b HOUSE.Building.particular  can support a roof in exactly the same way as BUILDING.Building.particular can.

**Tags:** semantics, model-theory
> **Comments:**
> **username_1**: Before it even makes sense to answer this question you should explain what your categories are. What are the morphisms?  
> **username_0**: My earlier [link](http://cstheory.stackexchange.com/questions/18215/is-there-a-model-theory-for-haskell-type-classess) describes the categories and morphisms.  
> **username_0**: The categories are signatures, sentences and models. I think the morphisms might be sub-class and sub-model. My earlier [link](http://cstheory.stackexchange.com/questions/18215/is-there-a-model-theory-for-haskell-type-classess) describes the categories and morphisms that I think might be appropriate for classes and instances.  
> **username_1**: Sorry, this looks a bit confused to me. The question you link to does not clearly state what the objects and the morphisms are. Your best bet is to explicitly describe the category in question right here. Also, what makes you think type classes have a sensible categorical interpretation?  
> **username_2**: What is your definition of a Galois correspondence? Have you seen Peter Smith's notes? www.logicmatters.net/resources/pdfs/Galois.pdf‎  
> **username_0**: I was wondering if there is a correspondence between the partial order defined in the class structure and 'some' order on the implementations. Apparently there is not, so I withdraw the question. Thanks for both responses.  
> **username_2**: @Pat, that is not the conclusion I would draw. There may well be an order and mappings that constitute a Galois correspondence. The few people who have read your question do not have an answer.  
> **username_1**: @Pat: you made the wrong conclusion. We cannot answer your question because it is not precise enough to make sense. I repeat, how do you define your hierarchies of type classes and instances? I can see that for type classes you could use some sort of record subtyping, but what is the preorder on the instances?  
> **username_0**: I do not think that I can identify a hierarchy of instances, which I think leaves the question imprecise. My research  involves comparing type classes to modules in algebraic specification languages such as CafeOBJ or Maude. In these languages there is a Galois connection between classes of models and sets of sentences. I am taking type classes to be signature only theories.  

---

## 0 answers

