{-# OPTIONS_GHC -Wall #-}
{- The SimpleTypetermChecker.hs is a prototype ghci-script for the
typechecker. It is meant only for explaining how it works.
This file is not meant to be included in Ampersand.
-}
{- Thanks to one of the reviewers, you can also experiment with the listings in the paper.
Here are some ways you can call the type checker:
printTypes False listing_1_1
printTypes False listing_1_2
printTypes False listing_8_1
printTypes False listing_8_2
printTypes False listing_8_4
printTypes False listing_8_4
The reviewers' changes are at the end of this code and have been marked with comments
-}
module SimpleTypetermChecker where
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Data.Graph as Graph
import qualified Data.Tree as Tree
import Data.List
data Concept = Concept String deriving (Eq, Ord, Show)
data Relation = Rel String deriving (Eq, Ord, Show)
data Term = Term := Term -- equivalence/RULE
| Term :/\ Term -- intersection
| Term :* Term -- apply / compose
| Term :- Term -- set-difference
| F Term -- flip / converse
| R Relation -- declared relation
| I Concept -- identity element
| V Concept Concept -- full
deriving (Show)
(.<) :: Term -> Term -> Term
a .< b = a := a :/\ b
subTerms :: [Term] -> [Term]
subTerms (x:rst)
= x: (case x of
(a := b) -> subTerms [a,b]
(a :/\ b)-> subTerms [a,b]
(a :* b) -> subTerms [a,b]
(a :- b) -> subTerms [a,b]
(F a) -> subTerms [a]
_ -> []) ++ subTerms rst
subTerms [] = []
data Typeterm = Dom Term
| Inter Term Term deriving (Eq,Ord)
cod :: Term -> Typeterm
pop :: Concept -> Typeterm
cod x = Dom (flp x)
pop x = Dom (I x)
instance Show Typeterm where
showsPrec _ (Dom (F x)) str = "cod " ++ showsPrec 11 x str -- we never need outer parentheses due to where this is used in this example
showsPrec _ (Dom (I x)) str = "pop " ++ showsPrec 11 x str
showsPrec _ (Dom x) str = "Dom " ++ showsPrec 11 x str
showsPrec _ (Inter a b) str = "Inter("++showsPrec 0 a (","++showsPrec 0 b (")" ++ str))
instance Eq Term where
(==) a b = compare a b == EQ
instance Ord Term where
compare (a := b) (c := d) = compare (a,b) (c,d)
compare (_ := _) _ = GT
compare _ (_ := _) = LT
compare (a :/\ b) (c :/\ d) = compare (min a b,max a b) (min c d,max c d)
compare (_ :/\ _) _ = GT
compare _ (_ :/\ _) = LT
compare (a :* b) (c :* d) = compare (a,b) (c,d)
compare (_ :* _) _ = GT
compare _ (_ :* _) = LT
compare (a :- b) (c :- d) = compare (a,b) (c,d)
compare (_ :- _) _ = GT
compare _ (_ :- _) = LT
compare (F a) (F c) = compare a c
compare (F _) _ = GT
compare _ (F _) = LT
compare (R a) (R c) = compare a c
compare (R _) _ = GT
compare _ (R _) = LT
compare (I a) (I c) = compare a c
compare (I _) _ = GT
compare _ (I _) = LT
compare (V a b) (V c d) = compare (a,b) (c,d)
flp :: Term -> Term
flp (F x) = x
flp o@(I _) = o
flp (V a b) = V b a
flp (a :/\ b) = flp a :/\ flp b
flp (a :* b) = flp b :* flp a
flp x = F x
-- ‘typing ’ results in subtypes (.. is subtype of ..)
typing :: [Term] -> Set.Set (Typeterm, Typeterm)
typing exprs
= (Set.fromList . concat . map uTypeterm . subTerms) exprs
where
uTypeterm (a := b) = [ (Dom a,Dom b), (Dom b,Dom a), (cod a,cod b), (cod b,cod a)]
uTypeterm o@(a :/\ b) = [ (Dom o,Dom a), (Dom o,Dom b), (cod o,cod a), (cod o,cod b)]
uTypeterm o@(a :* b) = [ (Dom o,Dom a), (cod o,cod b), (Inter a b,cod a),(Inter a b,Dom b)]
uTypeterm o@(a :- _) = [ (Dom a,Dom o), (cod a,cod o)]
uTypeterm o@(F a) = [ (Dom o,cod a), (cod o,Dom a), (Dom a,cod o), (cod a,Dom o)]
uTypeterm o@(I c) = [ (Dom o,pop c), (cod o,pop c)]
uTypeterm o@(V a b) = [ (Dom o,pop a), (cod o,pop b)]
uTypeterm (R _) = []
calcTypeterms :: [Term]
-> ([String],[String],[String],String)
calcTypeterms sentences
= (typeErrors ,conceptTree ,typedRels ,accounting)
where
accounting = disp "eq" (Set.toList eq) ++ disp "eqClasses" eqClasses ++ disp "st" (Set.toList st) ++ disp "stClasses" stClasses ++ disp "eqVerts" eqVerts ++ disp "stVerts" stVerts
disp what lst
= "\n"++what++":\n "++intercalate "\n " (map show lst)
st,eq :: Set.Set (Typeterm, Typeterm)
st = typing sentences
eq = Set.filter (\(a,b) -> a < b) (Set.intersection (Set.map swap st) st)
where swap (a,b) = (b,a)
eqGraph = makegraph eqVerts eq
eqVerts = zip [0..] (Set.toAscList (Set.union (Set.map fst eq) (Set.map snd eq)))
eqClasses = forestToClasses eqVerts (Graph.components eqGraph)
getEqClass vert = head ([a | ((_,a),as)<-eqClasses, Set.member vert as]++[vert])
stVerts :: [(Int,Typeterm)]
stVerts
= zip [0..] $ Set.toAscList $ Set.map getEqClass $
(Set.union (Set.union (Set.map fst st) (Set.map snd st)) (Set.fromList (map (\((_,x),_) -> x) eqClasses)))
byEqClass = Set.map (\(x,y) -> (getEqClass x,getEqClass y))
stGraph = makegraph stVerts (byEqClass st)
stClasses = forestToClasses stVerts (Graph.scc stGraph)
conceptTree
= [ src ++ " ISA " ++
intercalate ", "
[tn | Dom (I (Concept tn)) <- Set.toList (stVertVals (Graph.reachable stGraph i)) ]
| (i,Dom (I (Concept src))) <- stVerts
]
typedRels
= [ relname++"[ "++srcnames++" * "++trgnames++" ]"
| (Rel relname) <- Set.toList $ rels sentences
, let srcnames = intercalate " /\\ " (typetree (Dom (R (Rel relname))))
, let trgnames = intercalate " /\\ " (typetree (cod (R (Rel relname))))
]
typetree :: Typeterm -> [String]
typetree e
= concat [ concat$ map getTypeterms [i | (i, tp)<-stVerts, tp==getEqClass e ] ]
getTypeterms :: Graph.Vertex -> [String]
getTypeterms vert
= [c | Dom (I (Concept c)) <- Set.toList (firstTyp Map.! vert)]
where reachMap,nonRefl :: Map.Map Graph.Vertex (Set.Set Graph.Vertex)
reachMap = Map.fromList (map (\v -> (v, Set.fromList$ Graph.reachable stGraph v)) (Graph.vertices stGraph))
nonRefl = Map.mapWithKey (\k vs -> Set.filter (\v -> not (Set.member k (reachMap Map.! v))) vs) reachMap
allTyps,firstTyp :: Map.Map Graph.Vertex (Set.Set Typeterm)
allTyps = Map.map (\vs -> Set.filter isPop (stVertVals (Set.toList vs))) nonRefl
firstTyp = Map.map (\vs -> Set.difference vs (Set.unions [allTypsFromTyp Map.! v | v <- Set.toList vs])) allTyps
allTypsFromTyp = Map.fromList [(k',v) | (k,v) <- Map.toList allTyps, k' <- Set.toList (stVertVals [k]), isPop k']
stVertVals :: [Graph.Vertex] -> Set.Set Typeterm
stVertVals verts
= Set.unions [ case [tps | (_,tps) <- eqClasses, Set.member tp tps] of
[tps] -> tps
_ -> Set.singleton tp
| v<-verts, let (_,tp) = stVerts !! v ]
isPop (Dom (I _)) = True
isPop _ = False
rels x = Set.fromList [r | R r <- subTerms x]
-- type errors come in three kinds:
-- 1. Two named types are equal.
-- This is usuallyunintended:
-- User could give equal types equal names.
-- 2. The type of a relation cannot be determined.
-- This means that the relation is not declared.
-- 3. The type of a term has no name
-- Occurences of type 1. may imply those of type 2. and 3., so we hide type 2./3. when type 1. occurs
-- Occurences of type 2. always imply those of 3., so we hide 3. when 2. occurs
typeErrors
= [ "1. These concepts are trivially equal (may be intended): " ++
intercalate ", " (map show concs)
| (_,as)<-eqClasses , let concs = [c|(Dom (I c)) <- Set.toList as]
, length concs >1]
++
[ "1. These concepts are derived to be equal (probably not intended): " ++
intercalate ", " (map show concs)
| (_,as)<-stClasses , let concs = [c|(Dom (I c)) <- Set.toList as]
, length concs >1]
/:
(
[ err
| (Rel relname) <- Set.toList $ rels sentences, let srcs = typetree (Dom (R (Rel relname))), let trgs = typetree (cod (R (Rel relname)))
, err <- if length srcs > 0 && length trgs > 0 then
(if length srcs > 1 || length trgs > 1 then
["2. The type of this relation is ambiguous (please use a more specific type): " ++ relname]
else [])
else ["2. The type this relation cannot be determined (please declare it): " ++ relname]
]
++
[ "3. This type is ambiguous:\n "
++ show as ++ "\n Possible types (maybe add ;I[.] with the intersection of these types):"
++ concat (map ("\n " ++) possible)
| (_,as)<-stVerts
, not (isPop as)
, let possible = typetree as -- make sure we do not count open types
, length possible > 1 -- more than one type: ambigueous
]
)
infix 3 :=, .<
infixl 5 :/\, :-
infixl 7 :*
(/:) :: [a] -> [a] -> [a]
(/:) [] b = b
(/:) a _ = a
infixr 4 /:
makegraph :: Eq a => [(Graph.Vertex, a)] -> Set.Set (a, a) -> Graph.Graph
makegraph verts tuples
= Graph.buildG (0,length verts - 1)
[(i,j) | (k,l)<-Set.toAscList tuples, (i,n)<-verts , k==n
, (j,m)<-verts,l==m]
forestToClasses :: Ord a1 => [(a, a1)] -> [Tree.Tree Int] -> [((a, a1), Set.Set a1)]
forestToClasses verts forest
= map (treeToClasses verts) forest
treeToClasses :: Ord a1 => [(a, a1)] -> Tree.Tree Int -> ((a, a1), Set.Set a1)
treeToClasses verts tree
= ( verts !! (foldr1 min x)
, Set.fromList $ map vertVal x)
where x = Tree.flatten tree
vertVal x' = snd (verts !! x')
-- Original example by the Authors of the paper
sampleInput :: [Term]
sampleInput
= [ idC "Judge" .< idC "Person" -- an ISA rule:
, idC "Person" .< idC "Judge" -- Person is a judge
-- declaring a relation:
, idC "Judge" :* rel "presides" :* idC "Session":= rel "presides"
-- declaringanother:
, idC "Session" :* rel "chamber" :* idC "Chamber" := rel "chamber"
-- typicalrule:
, rel "presides" :* rel "chamber" := rel "resides in chamber"
-- now some typeerrors:
, rel "sleeps on" .<
(idC "Guy Fawkes night" :/\ idC "Sleeper" :* idC "Home owner")
:* F (rel "sleeps on")
-- relation "given" cannot be typed; it is not declared:
, rel "chamber" .< rel "given"
]
-- Reviewer change: Parameterised for flexibility
printTypes :: Bool -> [Term] -> IO ()
printTypes verbose input = mapM_ putStrLn lnes
where
(typeErrors ,conceptTree ,typedRels ,accounting)
= calcTypeterms input
lnes = ["Typeterm errors:"]++typeErrors
++["","Concept tree:"]++conceptTree
++["","Relations:"]++typedRels
++ if verbose then [accounting] else [] -- to see intermediate results...
-- Reviewer change: ``where r = ... ; i = ...'' from sampleInput
-- turned into top-level definitions and renamed.
rel :: String -> Term
rel a = R (Rel a)
idC :: String -> Term
idC a = I (Concept a)
full :: String -> String -> Term
full a b = V (Concept a) (Concept b)
-- Reviewer change: Added encodings of the listings contained in the paper.
listing_1_1 :: [Term]
listing_1_1 =
[ idC "A" :* rel "r" :* idC "C" := rel "r"
, idC "A" :* rel "s" :* idC "B" := rel "s"
, idC "B" :* rel "t" :* idC "C" := rel "t"
, rel "s" :* rel "t" .< rel "r"
]
listing_1_2 :: [Term]
listing_1_2 =
[ idC "A" :* rel "r" :* idC "C" := rel "r"
, idC "B" :* rel "s" :* idC "A" := rel "s"
, idC "B" :* rel "t" :* idC "C" := rel "t"
, rel "s" :* rel "t" .< rel "r"
]
listing_8_1 :: [Term]
listing_8_1 =
[ idC "A" :* rel "r" :* idC "B" := rel "r"
, idC "C" :* rel "s" :* idC "D" := rel "s"
, idC "E" := idC "B" :/\ idC "C"
, rel "r" :* rel "s" := full "A" "D"
]
listing_8_2 :: [Term]
listing_8_2 =
[ idC "A" :* rel "r" :* idC "B" := rel "r"
, idC "C" :* rel "s" :* idC "D" := rel "s"
, idC "E" := idC "B" :/\ idC "C"
, rel "r" :* idC "E" :* rel "s" := full "A" "D"
]
listing_8_3 :: [Term] -- end of section 8
listing_8_3 =
[ rel "r" :/\ full "B" "A" := rel "r"
, rel "r" :* rel "r" :/\ idC "A" := idC "A"
]
listing_8_4 :: [Term] -- end of section 8, with added A .< B
listing_8_4 =
[ rel "r" :/\ full "B" "A" := rel "r"
, rel "r" :* rel "r" :/\ idC "A" := idC "A"
, idC "B" .< idC "A"
]