A paper uses Haskell type classes to represent ontological categories. A type class hierarchy is used to represent "concept hierarchies" where "functions are the units of inheritance". Here is a class diagram based on the paper:
With respect to the code below the following claim is made:
The Haskell code given so far is complete and type checked, explaining the entire refined concept hierarchies. With instantiations for types of boathouses and houseboats, values can be declared and axioms stated and evaluated to demonstrate semantic properties and differences. For example, it can be shown that a passenger on a boat in a boathouse cannot be said to be an inhabitant, while a passenger on a houseboat can.
(note spatial prepositions "in" and "on")
I have a three questions:
(Q1) Is the claim true?
(Q2) How would go about validating such a claim.
As regards Q2, I have create 72 instances with appropriately kinded data types as advised by the GHCI compiler (not supplied in this post). Then I checked the types with the following type level queries
Query 1 : A passenger on a boat in a boathouse cannot be said to be an in the boathouse (i.e. an inhabitant)
:t whatsIn (BoatHouse (Boat Person)) ==> OK whatsIn (BoatHouse (Boat Person)) :: [Boat Person]
:t whatsOn (HouseBoat Person) ==> ERROR No instance for (Surfaces BoatHouse (Boat Person))
Query 2 : A person can be both on and in a houseboat (a passenger and an inhabitant).
whatsOn (HouseBoat Person) :: [Person]
:t whatsIn (HouseBoat Person) ==> whatsIn (HouseBoat Person) :: [Person]
:t whatsOn (HouseBoat Person) ==> whatsOn (HouseBoat Person) :: [Person]
(Q3) Both these queries seem to be appropriately accepted and rejected by Haskell. Is there a better or easier way to validate this claim?
Source code from paper.
class Containers a b where
insert :: b -> a b -> a b
remove :: b -> a b -> a b
whatsIn :: a b -> [b]
class Surfaces a b where
put :: b -> a b -> a b
takeOff :: b -> a b -> a b
whatsOn :: a b -> [b]
class Contacts a b where
attach :: b -> a b -> a b
detach :: b -> a b -> a b
whatsAt :: a b -> [b]
class Paths a b c where
move :: c -> a b c -> a b c
origin, destination :: a b c -> b
whereIs :: a b c -> c -> b
class People p
class HeavyLoads l
class Surfaces w o => WaterBodies w o
class Containers h o => Houses h o
class (Surfaces v o, Paths a b (v o)) => Vehicles v o a b
class (Vehicles v o a b, WaterBodies w (v o)) => Vessels v o a b w
class (Vessels v p a b w, People p) => Boats v p a b w
class (Boats v p a b w, HeavyLoads p) => Barges v p a b w
class (Houses h (v p), Boats v p a b w, Contacts w (h (v p))) => BoatHouses h v p a b w
class (Barges v p a b w, Houses v p, People p) => HouseBoats v p a b w