# Haskell type classes as ontological categories

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 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

• So they're using Haskell type class mechanism because they never heard of prolog? – Andrej Bauer May 27 '18 at 19:38
• There is a large body of GIS-literature that believes that Haskell is broadly similar to an algebraic specification language. According to Kuhn Haskell can be seen as an ontology development and testing environment with unique advantages: it is typed, algebraic, higher-order, executable, lean, and freely available. But I am not so sure. – Patrick Browne May 28 '18 at 6:45
• The crux of the problem is that it appears that I have to add 72 instances to validate the claim. Maybe there is a better way? – Patrick Browne May 28 '18 at 6:53
• Well, it's more or less prolog, so you could write auxiliary type classes that will let you automate bits and pieces. But in the end you're going to have 72 things. – Andrej Bauer May 28 '18 at 19:21
• Yes, the type level logic is prolog like, but the instances result in a set of typed checked methods. Which I think is the main justification for the type class approach. – Patrick Browne May 28 '18 at 19:49