3
$\begingroup$

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:

typeclass diagram

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
$\endgroup$
5
  • 3
    $\begingroup$ So they're using Haskell type class mechanism because they never heard of prolog? $\endgroup$ – Andrej Bauer May 27 '18 at 19:38
  • 1
    $\begingroup$ 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. $\endgroup$ – Patrick Browne May 28 '18 at 6:45
  • $\begingroup$ 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? $\endgroup$ – Patrick Browne May 28 '18 at 6:53
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer May 28 '18 at 19:21
  • $\begingroup$ 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. $\endgroup$ – Patrick Browne May 28 '18 at 19:49
0
$\begingroup$

The code in Listing 1 represents my attempt to test the claim. I have simplified the classes, while retaining that ability to test the original claim, which is repeated here:

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.

Here is the simplified class hierarchy:

enter image description here

If we interpret an inhabitant as being directly in the boathouse then the claim is somewhat reasonable. This is because in Listing 1 whatsIn is not defined for type BoatHouseD, attempting to evaluate in GHCi:

whatsIn (BoatHouseDc (PeopleDc "joe")) 

will cause error. In general, if a function is not defined for a data type that function will fail to type check. Note whatsIn is defined in an instance of ContainersC class for the type BoatD and also defined in an instance of ContainersC class for the type BoatHouseD. whatsOn is defined for an instance of SurfacesC. These functions cannot be defined in the sub-classes HousesC, BoatHousesC, and HouseBoatsC of ContainersC or BoatsC, BoatHousesC, and HouseBoatC of SurfacesC.

On the other hand the semantics of the Haskell code can be used to refute the claim. The test in Listing 1 shows that if someone is on a boat and that boat is in a boathouse then they are indirectly in the boathouse.

Conclusion

Based on the Haskell code in Listing 1 we can refute the claim. Reasoning about the Haskell code there is some credibility in the claim. The sub-classes seem to be redundant, because functions can only be defined in instances of the class where they were originally declared, not in any sub-class of that original class. So the functions whatsIn and whatsOn cannot be defined for the sub-classes.

Listing 1

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-#  OPTIONS_GHC  -Wno-missing-methods #-}
 -- The suffix D=data type,Dc=constructor
 -- The data types were chosen to match the type variables in the type classes
            data PeopleD = PeopleDc [Char] deriving (Show,Eq)
            data BoatD a  = BoatDc a deriving (Show,Eq)
            data HouseBoatD a  = HouseBoatDc a  deriving (Show,Eq)
            data BoatHouseD a  = BoatHouseDc a deriving (Show,Eq)
            
             
            class ContainersC a b where -- suffix C= class
             insert :: b -> a b -> a b
             remove :: b -> a b -> a b
             whatsIn :: (a b) -> [b]
            
            class SurfacesC a b where  
             put ::  b -> a b -> a b
             takeOff :: b -> a b -> a b
             whatsOn :: (a b) -> [b] 
                           
            
            class PeopleC p
            class ContainersC h o => HousesC h o
            class (SurfacesC v o) => BoatsC v o
            class (HousesC h (v p), BoatsC v p) => BoatHousesC h v p
            class (BoatsC v p, HousesC v p, PeopleC p) => HouseBoatsC v p 
                         
           
            instance ContainersC BoatD PeopleD where
               whatsIn (BoatDc (PeopleDc x)) = [PeopleDc x]
            
            instance ContainersC BoatHouseD (BoatD PeopleD) where
                whatsIn (BoatHouseDc (BoatDc (PeopleDc x))) = [(BoatDc(PeopleDc x))]
          
            instance SurfacesC BoatD PeopleD where
               whatsOn (BoatDc (PeopleDc x)) = [PeopleDc x]
     
             test =  (head (whatsOn(head (whatsIn (BoatHouseDc (BoatDc (PeopleDc "joe"))))))) == 
                  (head (whatsOn(BoatDc (PeopleDc "joe"))))
$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.