From 3e193125ef48ca7eb4bd93be32d61e1d544df651 Mon Sep 17 00:00:00 2001 From: Diego Marcilio Date: Wed, 29 Nov 2017 20:59:58 -0200 Subject: [PATCH 1/6] First naive impl. of Subtype checking with operator (<:) - Adding Top (TTop) as a Type. --- 05.simpleExtensions/code/STLCExtensions.hs | 18 +++++++++++- 05.simpleExtensions/code/SubTypeTests.hs | 33 ++++++++++++++++++++++ 2 files changed, 50 insertions(+), 1 deletion(-) create mode 100644 05.simpleExtensions/code/SubTypeTests.hs diff --git a/05.simpleExtensions/code/STLCExtensions.hs b/05.simpleExtensions/code/STLCExtensions.hs index da5f562..00ee9be 100644 --- a/05.simpleExtensions/code/STLCExtensions.hs +++ b/05.simpleExtensions/code/STLCExtensions.hs @@ -19,6 +19,8 @@ Contributors: module STLCExtensions where import Prelude hiding (lookup) +import qualified Data.Set as Set +import qualified Data.Map.Lazy as Map type Id = String @@ -30,7 +32,8 @@ type RItem = (Label, Term) type TItem = (Term) -data Type = TBool +data Type = TTop + | TBool | TInt | TString | TUnit @@ -184,6 +187,19 @@ sure :: Maybe Type -> Type sure (Just x) = x sure Nothing = error "'Nothing' detected" +(<:) :: Type -> Type -> Bool +s <: TTop = True +(TArrow s1 s2) <: (TArrow t1 t2) = t1 <: s1 && s2 <: t2 +(TRecord s) <: (TRecord t) = isRecSubType s t +s <: t = s == t + +isRecSubType sub super = do + let subLabels = Set.fromList $ map fst sub + let superLabels = Set.fromList $ map fst super + + Set.isSubsetOf superLabels subLabels + + -- | A lookup function. It searches for a specific -- mapping involving an identifier and a type. lookup :: Id -> Gamma -> Maybe Type diff --git a/05.simpleExtensions/code/SubTypeTests.hs b/05.simpleExtensions/code/SubTypeTests.hs new file mode 100644 index 0000000..8b73c3e --- /dev/null +++ b/05.simpleExtensions/code/SubTypeTests.hs @@ -0,0 +1,33 @@ +module SubTypeTests where + +import STLCExtensions +import Test.HUnit + +-- run the test suite: runTestTT testSuite + +testSuite = TestList [ + TestLabel "Record: r1 <: r3" rec1, + TestLabel "Record: r1 <: r2" rec2, + TestLabel "Record: RecWidth - r2 <: r1" rec3, + TestLabel "Record: r1 <: r2" rec4, + TestLabel "Record: RecPerm - r2 <: r2perm" rec5, + TestLabel "Record: RecPerm - r2perm <: r2" rec6 + ] + +r1 = TRecord [("x", TInt)] +r2 = TRecord [("x", TInt), ("y", TString)] +r2perm = TRecord [("y", TString), ("x", TInt)] +r3 = TRecord [("x", TTop)] + + +rec1 = TestCase $ assertBool "TInt should be subtype of TTop" $ r1 <: r3 + +rec2 = TestCase $ assertEqual "TTop should not be subtype of TInt" (r3 <: r1) False + +rec3 = TestCase $ assertBool "Record with at least all elements of super type should be a subtype" $ r2 <: r3 + +rec4 = TestCase $ assertEqual "Record that doesn't have all elements of super type should not be a subtype" (r1 <: r2) False + +rec5 = TestCase $ assertBool "Order of elements should not matter in a subtype relation for records" $ r2 <: r2perm + +rec6 = TestCase $ assertBool "Order of elements should not matter in a subtype relation for records" $ r2perm <: r2 \ No newline at end of file From 27af833c43deb18dd2e6f85591778b60f3d658e1 Mon Sep 17 00:00:00 2001 From: Diego Marcilio Date: Wed, 29 Nov 2017 20:59:58 -0200 Subject: [PATCH 2/6] Width, Depth and Perm from S-Rcd using operations from Map data structure. --- 05.simpleExtensions/code/STLCExtensions.hs | 26 +++++++++++++--------- 05.simpleExtensions/code/SubTypeTests.hs | 25 ++++++++++++++------- 2 files changed, 32 insertions(+), 19 deletions(-) diff --git a/05.simpleExtensions/code/STLCExtensions.hs b/05.simpleExtensions/code/STLCExtensions.hs index 00ee9be..f89b580 100644 --- a/05.simpleExtensions/code/STLCExtensions.hs +++ b/05.simpleExtensions/code/STLCExtensions.hs @@ -19,8 +19,7 @@ Contributors: module STLCExtensions where import Prelude hiding (lookup) -import qualified Data.Set as Set -import qualified Data.Map.Lazy as Map +import qualified Data.Map as Map type Id = String @@ -187,19 +186,24 @@ sure :: Maybe Type -> Type sure (Just x) = x sure Nothing = error "'Nothing' detected" +-- | Subtyping checker. Returns a Bool indicating if the first argument +-- is a subtype of the second. (<:) :: Type -> Type -> Bool -s <: TTop = True +_ <: TTop = True (TArrow s1 s2) <: (TArrow t1 t2) = t1 <: s1 && s2 <: t2 (TRecord s) <: (TRecord t) = isRecSubType s t -s <: t = s == t - -isRecSubType sub super = do - let subLabels = Set.fromList $ map fst sub - let superLabels = Set.fromList $ map fst super - - Set.isSubsetOf superLabels subLabels +s <: t = s == t + +-- | Turn Records into maps and checks for: +-- Width, Permutation and Depth +-- Map.lookup takes care of Width and Permutation. +-- Depth is taken care by the subtyping 'typ2 <: typ'. +isRecSubType :: [(Label,Type)] -> [(Label,Type)] -> Bool +isRecSubType sub super = all sRcd super + where sRcd (label, typ) = case Map.lookup label (Map.fromList sub) of + Just typ2 -> typ2 <: typ + Nothing -> False - -- | A lookup function. It searches for a specific -- mapping involving an identifier and a type. lookup :: Id -> Gamma -> Maybe Type diff --git a/05.simpleExtensions/code/SubTypeTests.hs b/05.simpleExtensions/code/SubTypeTests.hs index 8b73c3e..104aa43 100644 --- a/05.simpleExtensions/code/SubTypeTests.hs +++ b/05.simpleExtensions/code/SubTypeTests.hs @@ -8,26 +8,35 @@ import Test.HUnit testSuite = TestList [ TestLabel "Record: r1 <: r3" rec1, TestLabel "Record: r1 <: r2" rec2, - TestLabel "Record: RecWidth - r2 <: r1" rec3, + TestLabel "Record: RcdWidth - r2 <: r1" rec3, TestLabel "Record: r1 <: r2" rec4, - TestLabel "Record: RecPerm - r2 <: r2perm" rec5, - TestLabel "Record: RecPerm - r2perm <: r2" rec6 + TestLabel "Record: RcdPerm - r2 <: r2perm" rec5, + TestLabel "Record: RcdPerm - r2perm <: r2" rec6, + TestLabel "Record: RcdDepth - r4 <: r5" rec7, + TestLabel "Record: RcdDepth - r5 <: r4" rec8 ] r1 = TRecord [("x", TInt)] r2 = TRecord [("x", TInt), ("y", TString)] r2perm = TRecord [("y", TString), ("x", TInt)] r3 = TRecord [("x", TTop)] - +innerRecX = TRecord [("a", TInt), ("b", TInt)] +innerRecY = TRecord [("m", TInt), ("n", TInt)] +r4 = TRecord [("x", innerRecX), ("y", innerRecY)] +r5 = TRecord [("x", TRecord [("a", TInt)]), ("y", TRecord [("n", TInt)]) ] rec1 = TestCase $ assertBool "TInt should be subtype of TTop" $ r1 <: r3 rec2 = TestCase $ assertEqual "TTop should not be subtype of TInt" (r3 <: r1) False -rec3 = TestCase $ assertBool "Record with at least all elements of super type should be a subtype" $ r2 <: r3 +rec3 = TestCase $ assertBool "Record with at least all fields of super type should be a subtype" $ r2 <: r3 + +rec4 = TestCase $ assertEqual "Record that doesn't have all fields of super type should not be a subtype" (r1 <: r2) False + +rec5 = TestCase $ assertBool "Order of fields should not matter in a subtype relation for records" $ r2 <: r2perm -rec4 = TestCase $ assertEqual "Record that doesn't have all elements of super type should not be a subtype" (r1 <: r2) False +rec6 = TestCase $ assertBool "Order of fields should not matter in a subtype relation for records" $ r2perm <: r2 -rec5 = TestCase $ assertBool "Order of elements should not matter in a subtype relation for records" $ r2 <: r2perm +rec7 = TestCase $ assertBool "Corresponding fields should keep a subtype relation" $ r4 <: r5 -rec6 = TestCase $ assertBool "Order of elements should not matter in a subtype relation for records" $ r2perm <: r2 \ No newline at end of file +rec8 = TestCase $ assertEqual "Corresponding fields should keep a subtype relation" (r5 <: r4) False \ No newline at end of file From fe0bc78bafc31935d25a799e40e680054a025f1f Mon Sep 17 00:00:00 2001 From: Diego Marcilio Date: Wed, 29 Nov 2017 20:59:58 -0200 Subject: [PATCH 3/6] Adding more test cases, specially for TArrow. - Changing all assertions to assertEqual -- Output is clearer. (shows expected value) --- 05.simpleExtensions/code/SubTypeTests.hs | 48 +++++++++++++++++++----- 1 file changed, 39 insertions(+), 9 deletions(-) diff --git a/05.simpleExtensions/code/SubTypeTests.hs b/05.simpleExtensions/code/SubTypeTests.hs index 104aa43..6b9cebd 100644 --- a/05.simpleExtensions/code/SubTypeTests.hs +++ b/05.simpleExtensions/code/SubTypeTests.hs @@ -6,6 +6,7 @@ import Test.HUnit -- run the test suite: runTestTT testSuite testSuite = TestList [ + TestLabel "Record: r2 <: r" recc, TestLabel "Record: r1 <: r3" rec1, TestLabel "Record: r1 <: r2" rec2, TestLabel "Record: RcdWidth - r2 <: r1" rec3, @@ -13,9 +14,17 @@ testSuite = TestList [ TestLabel "Record: RcdPerm - r2 <: r2perm" rec5, TestLabel "Record: RcdPerm - r2perm <: r2" rec6, TestLabel "Record: RcdDepth - r4 <: r5" rec7, - TestLabel "Record: RcdDepth - r5 <: r4" rec8 + TestLabel "Record: RcdDepth - r5 <: r4" rec8, + TestLabel "TBool <: TBool" reflTBool, + TestLabel "TInt <: TInt" reflTInt, + TestLabel "TString <: TString" reflTString, + TestLabel "arr <: arr" reflArr, + TestLabel "Arrow: arr1 <: arr" arrow1, + TestLabel "Arrow: arr2 <: arr" arrow2, + TestLabel "Arrow: arr3 <: arr " arrow3 ] +r = TRecord [("y", TString)] r1 = TRecord [("x", TInt)] r2 = TRecord [("x", TInt), ("y", TString)] r2perm = TRecord [("y", TString), ("x", TInt)] @@ -24,19 +33,40 @@ innerRecX = TRecord [("a", TInt), ("b", TInt)] innerRecY = TRecord [("m", TInt), ("n", TInt)] r4 = TRecord [("x", innerRecX), ("y", innerRecY)] r5 = TRecord [("x", TRecord [("a", TInt)]), ("y", TRecord [("n", TInt)]) ] + +-- T3 <: T1 T2 <: T4 +-- ---------------------- +-- T1 -> T2 <: T3 -> T4 +arr = TArrow (TRecord [("x", TInt), ("y", TInt), ("z", TInt)]) (TRecord [("x", TInt), ("y", TInt)]) +arr1 = TArrow (TRecord [("x", TInt), ("y", TInt)]) (TRecord [("x", TInt), ("y", TInt), ("w", TBool)]) +arr2 = TArrow (TRecord [("y", TInt)]) (TRecord [("w", TBool)]) +arr3 = TArrow (TRecord [("w", TInt)]) (TRecord [("x", TInt), ("y", TInt)]) + +-- Test cases + +recc = TestCase $ assertEqual "{x: Int, y: String} should be subtype of {y: String}" True (r2 <: r) -rec1 = TestCase $ assertBool "TInt should be subtype of TTop" $ r1 <: r3 +rec1 = TestCase $ assertEqual "{x: Top} should not be subtype of {x: Int}" True (r1 <: r3) + +rec2 = TestCase $ assertEqual "{x: Int} should be subtype of {x: Top}" False (r3 <: r1) + +rec3 = TestCase $ assertEqual "Record with at least all fields of super type should be a subtype" True (r2 <: r3) -rec2 = TestCase $ assertEqual "TTop should not be subtype of TInt" (r3 <: r1) False +rec4 = TestCase $ assertEqual "Record that doesn't have all fields of super type should not be a subtype" False (r1 <: r2) -rec3 = TestCase $ assertBool "Record with at least all fields of super type should be a subtype" $ r2 <: r3 +rec5 = TestCase $ assertEqual "Order of fields should not matter in a subtype relation for records" True (r2 <: r2perm) -rec4 = TestCase $ assertEqual "Record that doesn't have all fields of super type should not be a subtype" (r1 <: r2) False +rec6 = TestCase $ assertEqual "Order of fields should not matter in a subtype relation for records" True (r2perm <: r2) -rec5 = TestCase $ assertBool "Order of fields should not matter in a subtype relation for records" $ r2 <: r2perm +rec7 = TestCase $ assertEqual "Corresponding fields should keep a subtype relation" True (r4 <: r5) -rec6 = TestCase $ assertBool "Order of fields should not matter in a subtype relation for records" $ r2perm <: r2 +rec8 = TestCase $ assertEqual "Corresponding fields should keep a subtype relation" False (r5 <: r4) -rec7 = TestCase $ assertBool "Corresponding fields should keep a subtype relation" $ r4 <: r5 +reflTInt = TestCase $ assertEqual "TInt should be subtype of itself" True (TInt <: TInt) +reflTBool = TestCase $ assertEqual "TInt should be subtype of itself" True (TBool <: TBool) +reflTString = TestCase $ assertEqual "TInt should be subtype of itself" True (TString <: TString) -rec8 = TestCase $ assertEqual "Corresponding fields should keep a subtype relation" (r5 <: r4) False \ No newline at end of file +reflArr = TestCase $ assertEqual "arr should be subtype of itself" True (arr <: arr) +arrow1 = TestCase $ assertEqual "Should be subtype" True (arr1 <: arr) +arrow2 = TestCase $ assertEqual "Should not be subtype" False (arr2 <: arr) +arrow3 = TestCase $ assertEqual "Should not be subtype" False (arr3 <: arr) From d87b1d8a6dc9a259c8b48fd8ed0b4e702d4ca461 Mon Sep 17 00:00:00 2001 From: Diego Marcilio Date: Fri, 1 Dec 2017 10:51:55 -0200 Subject: [PATCH 4/6] Test case expressing Transitivity with Records. --- 05.simpleExtensions/code/SubTypeTests.hs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/05.simpleExtensions/code/SubTypeTests.hs b/05.simpleExtensions/code/SubTypeTests.hs index 6b9cebd..b523034 100644 --- a/05.simpleExtensions/code/SubTypeTests.hs +++ b/05.simpleExtensions/code/SubTypeTests.hs @@ -15,6 +15,7 @@ testSuite = TestList [ TestLabel "Record: RcdPerm - r2perm <: r2" rec6, TestLabel "Record: RcdDepth - r4 <: r5" rec7, TestLabel "Record: RcdDepth - r5 <: r4" rec8, + TestLabel "Record: Transitivity - recA <: recB, recB <: recC, recA <: recC" recTrans, TestLabel "TBool <: TBool" reflTBool, TestLabel "TInt <: TInt" reflTInt, TestLabel "TString <: TString" reflTString, @@ -34,6 +35,11 @@ innerRecY = TRecord [("m", TInt), ("n", TInt)] r4 = TRecord [("x", innerRecX), ("y", innerRecY)] r5 = TRecord [("x", TRecord [("a", TInt)]), ("y", TRecord [("n", TInt)]) ] +-- Transitivity on Records +recA = TRecord [("v1", TInt), ("v2", TString), ("v3", TBool)] +recB = TRecord [("v3", TBool), ("v2", TString)] +recC = TRecord [("v2", TString)] + -- T3 <: T1 T2 <: T4 -- ---------------------- -- T1 -> T2 <: T3 -> T4 @@ -62,6 +68,10 @@ rec7 = TestCase $ assertEqual "Corresponding fields should keep a subtype relati rec8 = TestCase $ assertEqual "Corresponding fields should keep a subtype relation" False (r5 <: r4) +recTrans = TestCase $ do assertEqual "recA should be subtype of recB" True (recA <: recB) + assertEqual "recB should be subtype of recC" True (recB <: recC) + assertEqual "recA should be subtype of recC" True (recA <: recC) + reflTInt = TestCase $ assertEqual "TInt should be subtype of itself" True (TInt <: TInt) reflTBool = TestCase $ assertEqual "TInt should be subtype of itself" True (TBool <: TBool) reflTString = TestCase $ assertEqual "TInt should be subtype of itself" True (TString <: TString) From 8f830e6c4e43f5039c9ddf91b04b55061beffdc4 Mon Sep 17 00:00:00 2001 From: Diego Marcilio Date: Fri, 1 Dec 2017 11:15:00 -0200 Subject: [PATCH 5/6] Test case expressing Reflexivity on Records --- 05.simpleExtensions/code/SubTypeTests.hs | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/05.simpleExtensions/code/SubTypeTests.hs b/05.simpleExtensions/code/SubTypeTests.hs index b523034..5b1c1bf 100644 --- a/05.simpleExtensions/code/SubTypeTests.hs +++ b/05.simpleExtensions/code/SubTypeTests.hs @@ -16,6 +16,7 @@ testSuite = TestList [ TestLabel "Record: RcdDepth - r4 <: r5" rec7, TestLabel "Record: RcdDepth - r5 <: r4" rec8, TestLabel "Record: Transitivity - recA <: recB, recB <: recC, recA <: recC" recTrans, + TestLabel "Record: Reflexivity" recRefl, TestLabel "TBool <: TBool" reflTBool, TestLabel "TInt <: TInt" reflTInt, TestLabel "TString <: TString" reflTString, @@ -71,7 +72,17 @@ rec8 = TestCase $ assertEqual "Corresponding fields should keep a subtype relati recTrans = TestCase $ do assertEqual "recA should be subtype of recB" True (recA <: recB) assertEqual "recB should be subtype of recC" True (recB <: recC) assertEqual "recA should be subtype of recC" True (recA <: recC) - + +recRefl = TestCase $ do assertEqual "A record should be subtype/supertype of itself" True (recA <: recA) + assertEqual "A record should be subtype/supertype of itself" True (recB <: recB) + assertEqual "A record should be subtype/supertype of itself" True (recC <: recC) + assertEqual "A record should be subtype/supertype of itself" True (r <: r) + assertEqual "A record should be subtype/supertype of itself" True (r1 <: r1) + assertEqual "A record should be subtype/supertype of itself" True (r2 <: r2) + assertEqual "A record should be subtype/supertype of itself" True (r3 <: r3) + assertEqual "A record should be subtype/supertype of itself" True (r4 <: r4) + assertEqual "A record should be subtype/supertype of itself" True (r5 <: r5) + reflTInt = TestCase $ assertEqual "TInt should be subtype of itself" True (TInt <: TInt) reflTBool = TestCase $ assertEqual "TInt should be subtype of itself" True (TBool <: TBool) reflTString = TestCase $ assertEqual "TInt should be subtype of itself" True (TString <: TString) From 07f87b7a6a5f060ff08153600dc244a80bf16885 Mon Sep 17 00:00:00 2001 From: Diego Marcilio Date: Thu, 7 Dec 2017 17:07:29 -0200 Subject: [PATCH 6/6] Subtype transitivity with primitive types --- 05.simpleExtensions/code/STLCExtensions.hs | 19 ++++++++++++++++++- 05.simpleExtensions/code/SubTypeTests.hs | 8 +++++++- 2 files changed, 25 insertions(+), 2 deletions(-) diff --git a/05.simpleExtensions/code/STLCExtensions.hs b/05.simpleExtensions/code/STLCExtensions.hs index f89b580..18bee83 100644 --- a/05.simpleExtensions/code/STLCExtensions.hs +++ b/05.simpleExtensions/code/STLCExtensions.hs @@ -31,8 +31,15 @@ type RItem = (Label, Term) type TItem = (Term) +type SubRel = [(Type, Type)] + +-- | List of tuples representing subtype relations. +-- Subtype should be the first element, supertype should be the second. +sub_sup = [(TBool,TInt),(TInt,TNumber)] + data Type = TTop | TBool + | TNumber -- For subtyping transitivity purposes | TInt | TString | TUnit @@ -192,7 +199,7 @@ sure Nothing = error "'Nothing' detected" _ <: TTop = True (TArrow s1 s2) <: (TArrow t1 t2) = t1 <: s1 && s2 <: t2 (TRecord s) <: (TRecord t) = isRecSubType s t -s <: t = s == t +s <: t = if s == t then True else lookup_subtype s t sub_sup -- | Turn Records into maps and checks for: -- Width, Permutation and Depth @@ -203,6 +210,16 @@ isRecSubType sub super = all sRcd super where sRcd (label, typ) = case Map.lookup label (Map.fromList sub) of Just typ2 -> typ2 <: typ Nothing -> False + +-- | Lookup function for transitivity +lookup_subtype :: Type -> Type -> SubRel -> Bool +lookup_subtype sub sup [] = False +lookup_subtype sub sup ((v, t):tail) + | sub == v && sup == t = True + | sub == v && sup /= t = lookup_subtype t sup tail + | sub /= v && sup /= t = lookup_subtype sub sup tail + | sub /= v && sup == t = lookup_subtype sub sup tail + | otherwise = False -- | A lookup function. It searches for a specific -- mapping involving an identifier and a type. diff --git a/05.simpleExtensions/code/SubTypeTests.hs b/05.simpleExtensions/code/SubTypeTests.hs index 5b1c1bf..4b2533b 100644 --- a/05.simpleExtensions/code/SubTypeTests.hs +++ b/05.simpleExtensions/code/SubTypeTests.hs @@ -4,6 +4,7 @@ import STLCExtensions import Test.HUnit -- run the test suite: runTestTT testSuite +runTests = runTestTT testSuite testSuite = TestList [ TestLabel "Record: r2 <: r" recc, @@ -23,7 +24,8 @@ testSuite = TestList [ TestLabel "arr <: arr" reflArr, TestLabel "Arrow: arr1 <: arr" arrow1, TestLabel "Arrow: arr2 <: arr" arrow2, - TestLabel "Arrow: arr3 <: arr " arrow3 + TestLabel "Arrow: arr3 <: arr " arrow3, + TestLabel "Transitivity with Primitive Types" trans ] r = TRecord [("y", TString)] @@ -91,3 +93,7 @@ reflArr = TestCase $ assertEqual "arr should be subtype of itself" True (arr <: arrow1 = TestCase $ assertEqual "Should be subtype" True (arr1 <: arr) arrow2 = TestCase $ assertEqual "Should not be subtype" False (arr2 <: arr) arrow3 = TestCase $ assertEqual "Should not be subtype" False (arr3 <: arr) + +trans = TestCase $ do assertEqual "TBool <: TInt should return true (sub_sup list of tuples)" True (TBool <: TInt) + assertEqual "TInt <: TNumber should return true (sub_sup list of tuples)" True (TInt <: TNumber) + assertEqual "TBool <: TNumber should return true (TRANSITIVITY)" True (TBool <: TNumber)