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 diagram of the Haskell type classes 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.
The spatial prepositions in and on form part of the semantics the whatsIn
and whatsOn
predicates in the code below.
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 in the boathouse (i.e. an inhabitant)
:t whatsIn (BoatHouse (Boat People)) =t=> OK whatsIn (BoatHouse (Boat People)) :: [Boat People]
:t whatsOn (HouseBoat People) =t=> ERROR No instance for (Surfaces BoatHouse (Boat People))
Query 2 : A person can be both on and in a houseboat (a passenger and an inhabitant).
whatsOn (HouseBoat People) :: [People]
:t whatsIn (HouseBoat People) =t=> whatsIn (HouseBoat People) :: [People]
:t whatsOn (HouseBoat People) =t=> whatsOn (HouseBoat People) :: [People]
(Q3) Both these queries seem to be apptropriately accepted and rejected by Haskell. Is there a better or easier way to validate this claim?
Listing 1 shows the 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 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 PeopleClass 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, PeopleClass 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, PeopleClass p) => HouseBoats v p a b w