5
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Before it even makes sense to answer this question you should explain what your categories are. What are the morphisms? $\endgroup$ – Andrej Bauer Aug 5 '13 at 14:25
  • $\begingroup$ My earlier link describes the categories and morphisms. $\endgroup$ – Pat Aug 5 '13 at 15:39
  • $\begingroup$ 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. $\endgroup$ – Pat Aug 5 '13 at 15:46
  • $\begingroup$ 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? $\endgroup$ – Andrej Bauer Aug 6 '13 at 16:41
  • $\begingroup$ What is your definition of a Galois correspondence? Have you seen Peter Smith's notes? www.logicmatters.net/resources/pdfs/Galois.pdf‎ $\endgroup$ – Vijay D Aug 7 '13 at 6:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.