# Is there a Galois correspondence between a Haskell class hierarchy and its instance hierarchy?

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.


• Before it even makes sense to answer this question you should explain what your categories are. What are the morphisms? – Andrej Bauer Aug 5 '13 at 14:25
• My earlier link describes the categories and morphisms. – Pat Aug 5 '13 at 15:39
• The categories are signatures, sentences and models. I think the morphisms might be sub-class and sub-model. My earlier link describes the categories and morphisms that I think might be appropriate for classes and instances. – Pat Aug 5 '13 at 15:46
• 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 Aug 6 '13 at 16:41
• What is your definition of a Galois correspondence? Have you seen Peter Smith's notes? www.logicmatters.net/resources/pdfs/Galois.pdf‎ – Vijay D Aug 7 '13 at 6:41