Hi
Is it reasonable to 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 BUILDING is textually smaller than the specification of the class HOUSE,
provided we consider the operation inherited by HOUSE from BUILDING to be part of the signature of HOUSE (this may not be a valid assumption).
Is there a Galois correspondence between a Haskell class hierarchy and a given instance hierarchy for a particular type?
So more details are explained as [
1 ,
2 ].
Pat
--General Idea--
Theory subTheory Theory' <=> Model' subModel Model
--A specific example with Haskell class-to-instance relation --
class(BUILDING) subTheory class(HOUSE) <=> instance(HOUSE)} subModel 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.