justified-containers 0.1.2.0 → 0.2.0.0

raw patch · 6 files changed

+335/−15 lines, 6 filesdep +QuickCheckdep +ghc-primdep +hspecPVP ok

version bump matches the API change (PVP)

Dependencies added: QuickCheck, ghc-prim, hspec, justified-containers, roles, should-not-typecheck

API changes (from Hackage documentation)

Files

• README.md +110/−0
• justified-containers.cabal +24/−5
• src/Data/Map/Justified.hs +36/−7
• src/Data/Map/Justified/Tutorial.hs +5/−3
• test/Data/Map/JustifiedSpec.hs +159/−0
• test/Spec.hs +1/−0

@@ -1,6 +1,15 @@ # justified-containers Keyed container types with type-checked proofs of key presence. +# Table of contents++  * [Description](#description)+    * [A simple example](#example)+  * [Motivation](#motivation)+  * [How it works](#how-it-works)+    * [Phantom evidence](#phantom-evidence)++ # Description  Have you ever *known* that a key could be found in a certain map? Were you tempted to@@ -127,3 +136,104 @@ `Data.Map.Justified` uses the same rank-2 polymorphism trick used in the `Control.Monad.ST` monad to ensure that the `ph` phantom type can not be extracted; in effect, the proof that a key is present can't leak to contexts where the proof would no longer be valid.++## Phantom evidence++You can interpret the `ph` phantom type as a concrete *set of keys*; under this interpretation,+a value of type `Key ph k` is a key of type `k`, belonging to the subset described by `ph`.+Similarly, a `Map ph k v` is a map whose keys are exactly the subset of `k` described by `ph`.+From this perspective, the maps behave as if they were total, leading to their `Maybe`-free behavior.++## Why all the continuations?++Many of the functions in `justified-containers` make use of continuations, but why? As a case-study,+consider the basic function `withMap` that promotes a standard `Data.Map.Map` to a `Data.Map.Justified.Map':++```haskell+import Data.Map.Justified+import qualified Data.Map as M+withMap :: M.Map k v -> (forall ph. Map ph k v -> t) -> t+```++The last `(forall ph. Map ph k v -> t) -> t` part is the continuation.++The idea is that we know there is *some* set of keys `ph` belonging to this particular map, but+at compile-time we may not know exactly what it is. But it does exist, after all, so we should be+able to write++```haskell+withMap :: M.Map k v -> exists ph. Map ph k v+```++Similarly, the `inserting` function could look like++```haskell+inserting :: k -> v -> Map ph k v -> exists ph'. Map ph' k v+```++which can be read as "after inserting a key/value pair, we get a (possibly) different set of keys `ph'`".+But in this case, we actually know a bit more: first, the inserted key will be found in the new map. And+second, every key in `ph` can also be found in `ph'`. We+can encode that knowledge by giving an explicit inclusion of `ph` into `ph'`, encoded as a function of+type `Key ph k -> Key ph' k`. So we could re-write `inserting` with the type++```haskell+inserting :: k -> v -> Map ph k v -> exists ph'. (Key ph' k, Key ph k -> Key ph' k, Map ph' k v)+--                                                \_______/  \___________________/  \_________/+--                                   the new key______|                |                 |+--                                                      the inclusion__|                 |+--                                                                       the new map_____|+```++Likewise, when deleting a key from a map with keys `ph`, we get a new map with keys `ph'` along+with a guarantee that `ph'` is a subset of `ph`. Compared to `inserting`, the inclusion goes the+other way: there is an inclusion of `ph'` in `ph`, encoded as a function of type `Key ph' k -> Key ph l`.+Altogether, we could give `deleting` the type++```haskell+deleting :: k -> Map ph k v -> exists ph'. (Key ph' k -> Key ph k, Map ph' k v)+--                                          \___________________/  \_________/+--                                                    |                 |+--                            the reversed inclusion__|                 |+--                                                      the new map_____|+```++A similar pattern works for other map operations like `union`, `intersection`, `difference`, and+`filter`.++## But what about the continuations?++In the last section, we argued that `deleting` should have a type like++```haskell+deleting :: k -> Map ph k v -> exists ph'. (Key ph' k -> Key ph k, Map ph' k v)+--                             ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+```++But if you check the documentation, you'll see the type++```haskell+deleting :: k -> Map ph k v -> (forall ph'. (Key ph' k -> Key ph k, Map ph' k v) -> t) -> t+--                             ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+```++What happened to the underlined part of the type?++The problem is that Haskell doesn't support existential types directly: the `exists` part of+the type we wrote out is just wishful thinking. Instead, we have to go about things a little+indirectly: we'll *encode* existentially-quantified types, via *rank-2 universally-quantified types*.+++The idea can be understood via the Curry-Howard correspondence:+In classical logic, we have an equivalence between the propositions `∃X.P(X)`+and `∀T. ((∀X.F(X) => T) => T)`.  It turns out that this equivalence remains valid+in constructive logic, so we can transport it via the Curry-Howard correspondence to get+an isomorphism between types:++```haskell+exists ph.  Map ph k v ~ (forall ph. Map ph k v -> t) -> t+```++In other words, instead of returning the existentially-quantified type directly+we say "tell me what you wanted to do with that existentially-quantified type,+and I'll do it for you". 

@@ -1,5 +1,5 @@ name:                justified-containers-version:             0.1.2.0+version:             0.2.0.0 synopsis:            Keyed container types with type-checked proofs of key presence. description:         This package contains wrappers around standard container types,                      that provide guarantees about the presence of keys within the@@ -15,15 +15,34 @@ extra-source-files:  README.md cabal-version:       >=1.10 ++source-repository head+  type:     git+  location: https://github.com/matt-noonan/justified-containers++ library   hs-source-dirs:      src   exposed-modules:     Data.Map.Justified                      , Data.Map.Justified.Tutorial   ghc-options:         -O2 -Wall   build-depends:       base >= 4.7 && < 5-                     , containers                     +                     , containers+                     , roles >= 0.2   default-language:    Haskell2010 -source-repository head-  type:     git-  location: https://github.com/matt-noonan/justified-containers++test-suite justified-containers-spec+  type:              exitcode-stdio-1.0+  main-is:           Spec.hs+  hs-source-dirs:    test+  ghc-options:       -Wall -Wno-deferred-type-errors+  build-depends:     base >= 4.7 && < 5+                   , hspec+                   , justified-containers+                   , containers+                   , QuickCheck+                   , should-not-typecheck+                   , ghc-prim+  other-modules:     Data.Map.JustifiedSpec+  default-language:  Haskell2010

@@ -1,4 +1,4 @@-{-# LANGUAGE RankNTypes, DeriveTraversable #-}+{-# LANGUAGE RankNTypes, DeriveTraversable, ScopedTypeVariables, RoleAnnotations #-} -- | -- Module      :  Data.Map.Justified -- Copyright   :  (c) Matt Noonan 2017@@ -21,7 +21,7 @@ -- None of the functions in this module can cause a run-time error, and very few -- of the operations return a @'Maybe'@ value. ----- See the 'Data.Map.Justified.Tutorial' module for usage examples.+-- See the "Data.Map.Justified.Tutorial" module for usage examples. -- -- === Example -- @@@ -141,6 +141,7 @@     -- * Gathering evidence     , member     , keys+    , lookupMay     , lookupLT     , lookupLE     , lookupGT@@ -206,6 +207,9 @@ import Data.List (partition) import Control.Arrow ((&&&)) +import Data.Roles+import Data.Type.Coercion+ {--------------------------------------------------------------------   Map and Key types --------------------------------------------------------------------}@@ -219,6 +223,7 @@ -- @'Map'@ allows you to shift the burden of proof that a key exists -- in a map from "prove at every lookup" to "prove once per key". newtype Map ph k v = Map (M.Map k v) deriving (Eq, Ord, Show, Functor, Foldable, Traversable)+type role Map phantom nominal representational  -- | A key that knows it can be found in certain @'Map'@s. -- @@ -227,6 +232,7 @@ -- operations such as lookup will only type-check if the @'Key'@ -- and the @'Map'@ have the same phantom type parameter. newtype Key ph k = Key k deriving (Eq, Ord, Show)+type role Key phantom representational  -- | Get a bare key out of a key-plus-evidence by forgetting -- what map the key can be found in.@@ -302,18 +308,35 @@ -- > withRecMap memory2 (const ()) -- Left [(1, Cons (2,Present) (3,Missing))] -- -- See @'Data.Map.Justified.Tutorial.example5'@ for more usage examples.-withRecMap :: (Ord k, Traversable f)++withRecMap :: forall k f t . (Ord k, Traversable f, Representational f)            => M.Map k (f k) -- ^ A map with key references            -> (forall ph. Map ph k (f (Key ph k)) -> t) -- ^ The checked continuation            -> Either [MissingReference k f] t -- ^ Resulting value, or failure report.+ withRecMap m cont =-  case bad of-    [] -> Right $ cont (Map $ M.map (fmap Key) $ M.fromList ok)-    _  -> Left (map (\(k,v) -> (k, fmap (id &&& locate) v)) bad)+  +  case snd (partition (allKeysPresent . snd) $ M.toList m) of+    +    -- All referenced keys are found in the map; coerce the map's type.+    []   -> Right $ cont (Map $ (coerceWith mapCoercion) m)++    -- There were some dangling key references; report them.+    bads -> Left (map (\(k,v) -> (k, fmap (id &&& locate) v)) bads)+   where-    (ok, bad) = partition (all ((== Present) . locate) . snd) (M.toList m)++    allKeysPresent = all ((== Present) . locate)+     locate k = if M.member k m then Present else Missing+    +    nestedValueCoercion :: Coercion (f k) (f (Key ph0 k))+    nestedValueCoercion = rep Coercion+    +    mapCoercion :: Coercion (M.Map k (f k)) (M.Map k (f (Key ph0 k)))+    mapCoercion = rep nestedValueCoercion + {--------------------------------------------------------------------   Gathering evidence --------------------------------------------------------------------}@@ -360,6 +383,12 @@ lookup (Key k) (Map m) = case M.lookup k m of   Just value -> value   Nothing    -> error "Data.Map.Justified has been subverted!"++-- | /O(log n)/. Lookup the value at a key that is /not/ already known+-- to be in the map. Return @Just@ the value /and/ the key-with-evidence+-- if the key was present, or @Nothing@ otherwise.+lookupMay :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)+lookupMay k (Map m) = fmap (\v -> (Key k, v)) (M.lookup k m)  -- | /O(log n)/. Find the largest key smaller than the given one -- and return the corresponding (key,value) pair, with evidence for the key.

@@ -36,6 +36,8 @@ import Data.Char (toUpper) import Control.Monad (forM_) +import Data.Type.Coercion+ -- | A simple "Data.Map" value used in several examples below. -- -- @@@ -220,9 +222,9 @@ -- "new key" data. -- -- @---  example4 = withMap test_table $ \table -> do---    inserting 3 "NEW" table $ \(newKey, upgrade, table') -> do---      forM_ (keys table) $ \key -> do+--  example4 = withMap test_table $ \\table -> do+--    inserting 3 "NEW" table $ \\(newKey, upgrade, table') -> do+--      forM_ (keys table) $ \\key -> do --        putStrLn (show key ++ " maps to " ++ table  ! key ++ " in the old table.") --        putStrLn (show key ++ " maps to " ++ table' ! (upgrade key) ++ " in the new table.") --      putStrLn ("Also, the new table maps " ++ show newKey ++ " to " ++ table' ! newKey)

@@ -0,0 +1,159 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE MagicHash #-}+{-# OPTIONS_GHC -fdefer-type-errors #-}++module Data.Map.JustifiedSpec (main, spec) where++import Prelude hiding (lookup)++import Test.Hspec+import Test.QuickCheck+import Test.ShouldNotTypecheck++import Data.Map.Justified+import qualified Data.Map as M+import Data.Maybe++import GHC.Prim+import GHC.Int+import System.Mem (performGC)+import System.IO.Unsafe (unsafePerformIO)++import Data.Map.Justified.Tutorial (adjacencies)++import Data.Type.Coercion++main :: IO ()+main = hspec spec++letters :: M.Map Char Int+letters = M.fromList (Prelude.zip ['a'..'z'] [1..])++newtype AlphaNum = AlphaNum Char deriving Show+instance Arbitrary AlphaNum where+  arbitrary = elements (map AlphaNum $ ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'])+  +spec :: Spec+spec = do++  describe "using Data.Map.Justified.Map" $ do++    it "wraps the underlying Data.Map.Map without modification" $ do+      withMap letters theMap == letters++    it "can create singleton maps" $ property $ do+      \(k :: Int, v :: Int) -> withSingleton k v (uncurry lookup) == v+      \(k :: Int, v :: Int) -> withSingleton k v (theMap . snd)   == M.fromList [(k,v)]+      +  describe "validated keys" $ do+    +    it "can be obtained iff a key is present" $ property $+      \(AlphaNum c) -> isJust (M.lookup c letters) == withMap letters (isJust . member c)++    it "will access the expected value" $ do+      map (\k -> fromJust $ M.lookup k letters) (M.keys letters)+      `shouldBe`+      withMap letters (\m -> map (`lookup` m) (keys m))+      +    it "can degrade to the original key" $ do+      M.keys letters `shouldBe` withMap letters (map theKey . keys)++    it "can still be used in an adjusted map" $ do+      withMap letters (\m -> let (k:k':_) = keys m in+                                 (lookup k (reinsert k 17 m),+                                  lookup k (reinsert k' 17 m),+                                  lookup k (adjust (+1) k m),+                                  lookup k (adjustWithKey+                                              (\k v -> v + fromEnum (theKey k)) k m)))+      `shouldBe` (17,1,2,98)+      +    it "can not escape `withMap`" $ shouldNotTypecheck $+      withMap letters (head keys)++    it "can not be used in unrelated maps" $ shouldNotTypecheck $+      withMap letters (\m ->+         let k = head (keys m) in withMap letters (lookup k))++    it  "can not be directly created" $ shouldNotTypecheck $+      let k = Key 'a' in withMap letters (lookup k)++  describe "when adding keys" $ do++    it "can translate old keys to new map" $ property $+      \(AlphaNum c, AlphaNum c') -> withMap letters $+        \m -> inserting c' 100 m $+              \(_, upgrade, m') ->+              let k  = member c m+                  k' = member c m'+              in c /= c' ==> fmap upgrade k == k'+  +    it "does not let a new key be used in the old map without translation" $+      shouldNotTypecheck $+        withMap letters $ \m -> inserting 'X' 100 m $+          \(_, _, m') -> map (`lookup` m) (keys m')+    +  describe "when removing keys" $ do++    it "can translate new keys to old map" $ property $+      \(AlphaNum c, AlphaNum c') -> withMap letters $+         \m -> deleting c' m $+               \(downgrade, m') ->+               let k  = member c m+                   k' = member c m'+               in c /= c' ==> k == fmap downgrade k'++    it "does not let an old key be used in the new map without translation" $+      shouldNotTypecheck $+        withMap letters $ \m -> deleting 'X' m $+          \(_, _, m') -> map (`lookup` m') (keys m)+    +  describe "at runtime" $ do++    it "does not allocate map copies when gathering evidence" $ do+      withMap letters $ \m -> m `isLiterally` letters++    it "does not allocate map copies when forgetting evidence" $ do+      withMap letters $ \m -> theMap m `isLiterally` letters+        +    it "does not allocate key copies when gathering key evidence" $ do+      withMap letters $ \m ->+        each (M.keys letters) $ \k -> fromJust (k `member` m) `isLiterally` k++    it "does not allocate key copies when forgetting evidence" $ do+      withMap letters $ \m ->+        let ks = keys m+              -- This depends on the Prelude rewrite rule "map coerce/coerce" firing, I think.+        in map theKey ks `isLiterally` ks++    it "does not allocate keys during evidence conversion for insertion" $ do+      withMap letters $ \m ->+        inserting 'X' 100 m $ \(_, upgraded, _) ->+          each (keys m) $ \k -> upgraded k `isLiterally` k++    it "does not allocate keys during evidence conversion for deletion" $ do+      withMap letters $ \m ->+        deleting 'X' m $ \(downgraded, m') ->+          each (keys m') $ \k -> downgraded k `isLiterally` k+                                                     +    it "does not allocate values when performing lookup with a verified key" $ do+      withMap letters $ \m ->+        each (keys m) $ \k ->+          (k `lookup` m) `isLiterally` fromJust (theKey k `M.lookup` letters)++    it "does not allocate when verifying a recursive map" $ fromRight $ do+      withRecMap adjacencies $ \m -> m `isLiterally` adjacencies+      +-- | Test if two values occupy the same location in memory.+--   This is almost certainly flaky, especially if a GC occurs+--   during evaluation of ans!+isLiterally :: a -> b -> Bool+isLiterally x y = unsafePerformIO $ do+  let x' = unsafeCoerce# y+  x `seq` x' `seq` performGC+  return $ I64# (reallyUnsafePtrEquality# x x') == 1++each :: Traversable t => t a -> (a -> Bool) -> Bool+each = flip all++fromRight :: Either a b -> b+fromRight = either (error "expected Right, got Left") id

@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}