bluefin-internal 0.2.0.0 → 0.2.1.0

raw patch · 4 files changed

+154/−65 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +16/−0
• bluefin-internal.cabal +1/−1
• src/Bluefin/Internal.hs +114/−42
• src/Bluefin/Internal/Examples.hs +23/−22

@@ -1,3 +1,19 @@+## 0.2.1.0++* Add `handleImpl`, `HandleD` and `handleMapHandle`++* Add type role for `Exception`. This is technically a breaking change+  but it seems extremely unlikely to break working code, so we are not+  imposing a major version bump.++* Internal details of proof terms++  * Add proof terms for `:>~ instances.++  * Use `ZW` as the argument instead of `(# #)`.++  * Add `unsafeAxiom`+ ## 0.2.0.0  * Choose different incoherent instance for `:>` for better type

@@ -1,6 +1,6 @@ cabal-version:      3.0 name:               bluefin-internal-version:            0.2.0.0+version:            0.2.1.0 license:            MIT license-file:       LICENSE author:             Tom Ellis

@@ -1,6 +1,7 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE MagicHash #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UnboxedTuples #-}@@ -264,7 +265,7 @@ weakenEff _ = unsafeCoerceEff  insertFirst :: Eff b r -> Eff (c1 :& b) r-insertFirst = weakenEff (drop (eq (# #)))+insertFirst = weakenEff (drop (eq ZW))  insertSecond :: Eff (c1 :& b) r -> Eff (c1 :& (c2 :& b)) r insertSecond = insertManySecond@@ -273,13 +274,13 @@ insertManySecond = weakenEff (bimap has has)  assoc1Eff :: Eff ((a :& b) :& c) r -> Eff (a :& (b :& c)) r-assoc1Eff = weakenEff (assoc1 (# #))+assoc1Eff = weakenEff (assoc1 ZW)  pushFirst :: Eff a r -> Eff (a :& b) r-pushFirst = weakenEff (fstI (# #))+pushFirst = weakenEff (fstI ZW)  mergeEff :: Eff (a :& a) r -> Eff a r-mergeEff = weakenEff (merge (# #))+mergeEff = weakenEff (merge ZW)  inContext :: (e2 :> e1) => Eff (e1 :& e2) r -> Eff e1 r inContext = weakenEff (subsume1 has)@@ -327,6 +328,8 @@ newtype Exception exn (e :: Effects)   = MkException (forall a. exn -> Eff e a) +type role Exception representational nominal+ -- | A handle to a strict mutable state of type @s@ newtype State s (e :: Effects) = UnsafeMkState (IORef s) @@ -367,60 +370,112 @@ -- -- @ -- instance Handle Application where---   mapHandle---     MkApplication---       { queryDatabase = q,---         applicationState = a,---         logger = l---       } =---       MkApplication---         { queryDatabase = \\s i -> useImplUnder (q s i),---           applicationState = mapHandle a,---           logger = mapHandle l---         }+--   'handleImpl' =+--     'handleMapHandle' $+--       \\MkApplication+--          { queryDatabase = q,+--            applicationState = a,+--            logger = l+--          } ->+--           MkApplication+--             { queryDatabase = \\s i -> 'useImplUnder' (q s i),+--               applicationState = 'mapHandle' a,+--               logger = mapHandle l+--             } -- @ class Handle (h :: Effects -> Type) where+  {-# MINIMAL handleImpl | mapHandle #-}+  -- | Define @handleImpl@ using 'handleMapHandle'.+  handleImpl :: HandleD h+  handleImpl = MkHandleD mapHandle+   -- | Used to create compound effects, i.e. handles that contain   -- other handles.+  --+  -- You should not define this method in your type classes. Instead+  -- define @handleImpl@.  In a future version of Bluefin, @mapHandle@+  -- will no longer be a method.  If you previously had a definition+  -- of @mapHandle@, for example like this:+  --+  -- @+  -- instance Handle MyHandle where+  --   mapHandle h = \<definition\>+  -- @+  --+  -- you should change it to+  --+  -- @+  -- instance Handle MyHandle where+  --   handleImpl = handleMapHandle $ \\h -> \<definition\>+  -- @   mapHandle :: (e :> es) => h e -> h es+  mapHandle = case handleImpl of MkHandleD f -> f +-- | The type of the 'handleImpl' method of the 'Handle' class.+-- Create a @HandleD@ using 'handleMapHandle'.+newtype HandleD h = MkHandleD (forall e es. (e :> es) => h e -> h es)++-- | For defining the 'handleImpl' method of the 'Handle' class.+handleMapHandle ::+  (forall e es. (e :> es) => h e -> h es) ->+  -- | ͘+  HandleD h+handleMapHandle = MkHandleD+ instance Handle (State s) where-  mapHandle (UnsafeMkState s) = UnsafeMkState s+  handleImpl = handleMapHandle $ \(UnsafeMkState s) -> UnsafeMkState s  instance Handle (Exception s) where-  mapHandle (MkException s) = MkException (weakenEff has . s)+  handleImpl = handleMapHandle $ \(MkException s) ->+    MkException (weakenEff has . s)  instance Handle (Coroutine a b) where-  mapHandle (MkCoroutine f) = MkCoroutine (fmap useImpl f)+  handleImpl = handleMapHandle $ \(MkCoroutine f) ->+    MkCoroutine (fmap useImpl f)  instance Handle (Writer w) where-  mapHandle (Writer wr) = Writer (mapHandle wr)+  handleImpl = handleMapHandle $ \(Writer wr) -> Writer (mapHandle wr)  instance Handle IOE where-  mapHandle MkIOE = MkIOE+  handleImpl = handleMapHandle $ \MkIOE -> MkIOE +-- | A convenience type whose only purpose is to avoid writing @(# #)@+-- as an argument to functions which are only function because+-- top-level definitions of unlifted kind are forbidden.+newtype ZW = MkZW (# #)++pattern ZW :: ZW+pattern ZW <- MkZW (# #)+  where+    ZW = MkZW (# #)++{-# COMPLETE ZW #-}+ newtype In (a :: Effects) (b :: Effects) = In# (# #) -merge :: (# #) -> (a :& a) `In` a-merge (# #) = In# (# #)+unsafeInAxiom :: ZW -> e1 `In` e2+unsafeInAxiom ZW = In# (# #) -eq :: (# #) -> a `In` a-eq (# #) = In# (# #)+merge :: ZW -> (a :& a) `In` a+merge ZW = In# (# #) -fstI :: (# #) -> a `In` (a :& b)-fstI (# #) = In# (# #)+eq :: ZW -> a `In` a+eq ZW = unsafeInAxiom ZW -sndI :: (# #) -> a `In` (b :& a)-sndI (# #) = In# (# #)+fstI :: ZW -> a `In` (a :& b)+fstI ZW = unsafeInAxiom ZW +sndI :: ZW -> a `In` (b :& a)+sndI ZW = unsafeInAxiom ZW+ cmp :: a `In` b -> b `In` c -> a `In` c-cmp (In# (# #)) (In# (# #)) = In# (# #)+cmp (In# (# #)) (In# (# #)) = unsafeInAxiom ZW  bimap :: a `In` b -> c `In` d -> (a :& c) `In` (b :& d)-bimap (In# (# #)) (In# (# #)) = In# (# #)+bimap (In# (# #)) (In# (# #)) = unsafeInAxiom ZW -assoc1 :: (# #) -> ((a :& b) :& c) `In` (a :& (b :& c))-assoc1 (# #) = In# (# #)+assoc1 :: ZW -> ((a :& b) :& c) `In` (a :& (b :& c))+assoc1 ZW = unsafeInAxiom ZW  drop :: a `In` b -> a `In` (c :& b) drop h = w2 (b h)@@ -429,22 +484,22 @@ here h = w (b2 h)  w :: (a :& b) `In` c -> (a `In` c)-w = cmp (fstI (# #))+w = cmp (fstI ZW)  w2 :: (b :& a) `In` c -> (a `In` c)-w2 = cmp (sndI (# #))+w2 = cmp (sndI ZW)  b2 :: (a `In` b) -> ((a :& c) `In` (b :& c))-b2 h = bimap h (eq (# #))+b2 h = bimap h (eq ZW)  b :: (a `In` b) -> (c :& a) `In` (c :& b)-b = bimap (eq (# #))+b = bimap (eq ZW)  subsume1 :: (e2 `In` e1) -> (e1 :& e2) `In` e1-subsume1 i = cmp (bimap (eq (# #)) i) (merge (# #))+subsume1 i = cmp (bimap (eq ZW) i) (merge ZW)  subsume2 :: (e1 `In` e2) -> (e1 :& e2) `In` e2-subsume2 i = cmp (bimap i (eq (# #))) (merge (# #))+subsume2 i = cmp (bimap i (eq ZW)) (merge ZW)  -- | Effect subset constraint class (es1 :: Effects) :> (es2 :: Effects)@@ -452,10 +507,16 @@ -- | A set of effects @e@ is a subset of itself instance e :> e +instanceProof1 :: ZW -> e `In` e+instanceProof1 ZW = eq ZW+ -- | If @e@ is subset of @es@ then @e@ is a subset of a larger set, @x -- :& es@ instance {-# INCOHERENT #-} (e :> es) => e :> (x :& es) +instanceProof2 :: e `In` es -> e `In` (x :& es)+instanceProof2 = drop+ -- Do we want this? -- instance {-# incoherent #-} (e :> es) => (e' :& e) :> (e' :> es) @@ -464,13 +525,19 @@ -- | @e@ is a subset of a larger set @e :& es@ instance e :> (e :& es) +instanceProof3 :: ZW -> e `In` (e :& es)+instanceProof3 ZW = fstI ZW+ subset ::   forall e1 es m.   (Monad m) =>   (e1 :> es) =>   m ()-subset = pure ()+subset = satisfied @(e1 :> es) +satisfied :: forall c m. (Monad m, c) => m ()+satisfied = pure ()+ effTag :: Eff es (Proxy es) effTag = pure Proxy @@ -499,7 +566,9 @@ throw h = case mapHandle h of MkException throw_ -> throw_  has :: forall a b. (a :> b) => a `In` b-has = In# (# #)+-- This is safe because, as shown by instanceProof1/2/3, the only way+-- to construct `a :> b` is if `a `In` b`.+has = unsafeInAxiom ZW  data Dict c where   Dict :: forall c. (c) => Dict c@@ -1398,6 +1467,8 @@   Eff es a asks (MkReader st) f = fmap f (get st) +-- | Locally override the value in the @Reader@. It will be restored+-- when the @local@ block ends. local ::   (e1 :> es) =>   Reader r e1 ->@@ -1476,7 +1547,8 @@      useImplIn k h' -instance (Handle h) => Handle (HandleReader h) where mapHandle = mapHandleReader+instance (Handle h) => Handle (HandleReader h) where+  handleImpl = handleMapHandle mapHandleReader  newtype ConstEffect r (e :: Effects) = MkConstEffect r @@ -1488,4 +1560,4 @@ runConstEffect r k = useImplIn k (MkConstEffect r)  instance Handle (ConstEffect r) where-  mapHandle = coerce+  handleImpl = handleMapHandle coerce

@@ -668,7 +668,7 @@   }  instance Handle Counter5 where-  mapHandle c =+  handleImpl = handleMapHandle $ \c ->     MkCounter5       { incCounter5Impl = useImplUnder (incCounter5Impl c),         getCounter5Impl = \msg -> useImplUnder (getCounter5Impl c msg)@@ -729,7 +729,7 @@   }  instance Handle Counter6 where-  mapHandle c =+  handleImpl = handleMapHandle $ \c ->     MkCounter6       { incCounter6Impl = useImplUnder (incCounter6Impl c),         counter6State = mapHandle (counter6State c),@@ -792,7 +792,7 @@   }  instance Handle Counter7 where-  mapHandle c =+  handleImpl = handleMapHandle $ \c ->     MkCounter7       { incCounter7Impl = \ex -> useImplUnder (incCounter7Impl c ex),         counter7State = mapHandle (counter7State c),@@ -865,7 +865,7 @@   }  instance Handle FileSystem where-  mapHandle fs =+  handleImpl = handleMapHandle $ \fs ->     MkFileSystem       { readFileImpl = \fp -> useImplUnder (readFileImpl fs fp),         writeFileImpl = \fp s -> useImplUnder (writeFileImpl fs fp s)@@ -954,17 +954,18 @@   }  instance Handle Application where-  mapHandle-    MkApplication-      { queryDatabase = q,-        applicationState = a,-        logger = l-      } =-      MkApplication-        { queryDatabase = \s i -> useImplUnder (q s i),-          applicationState = mapHandle a,-          logger = mapHandle l-        }+  handleImpl =+    handleMapHandle $+      \MkApplication+         { queryDatabase = q,+           applicationState = a,+           logger = l+         } ->+          MkApplication+            { queryDatabase = \s i -> useImplUnder (q s i),+              applicationState = mapHandle a,+              logger = mapHandle l+            }  -- This example shows a case where we can use @bracket@ polymorphically -- in order to perform correct cleanup if @es@ is instantiated to a@@ -1051,7 +1052,7 @@   }  instance Handle (DynamicReader r) where-  mapHandle h =+  handleImpl = handleMapHandle $ \h ->     DynamicReader       { askLRImpl = useImplUnder (askLRImpl h),         localLRImpl = \f k -> useImplUnder (localLRImpl h f k)@@ -1091,14 +1092,14 @@   evalState () $ \st1 ->     evalState () $ \st2 -> do       Proxy :: Proxy es <- effTag-      subset @es @es+      satisfied @(es :> es)        Proxy :: Proxy e1 <- handleTag st1       Proxy :: Proxy e2 <- handleTag st2 -      subset @e1 @e1-      subset @e2 @e2-      subset @e1 @(e1 :& e2)-      subset @e2 @(e1 :& e2)+      satisfied @(e1 :> e1)+      satisfied @(e2 :> e2)+      satisfied @(e1 :> (e1 :& e2))+      satisfied @(e2 :> (e1 :& e2)) -      subset @(e1 :& e2) @(e1 :& e2)+      satisfied @((e1 :& e2) :> (e1 :& e2))