InitialHEADmaster

1 files changed, 59 insertions, 0 deletions

diff --git a/ch15_15.0.example.hs b/ch15_15.0.example.hs
new file mode 100644
index 0000000..8d63903
--- /dev/null
+++ b/ch15_15.0.example.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+
+import Control.Monad.Writer (WriterT, runWriterT, tell)
+import Data.Constraint (Dict (Dict))
+import Data.Foldable (for_)
+import Data.Kind (Type)
+
+data SBool (b :: Bool) where
+  STrue :: SBool 'True
+  SFalse :: SBool 'False
+
+data SomeSBool where
+  SomeSBool :: SBool b -> SomeSBool
+
+fromSBool :: SBool b -> Bool
+fromSBool STrue = True
+fromSBool SFalse = False
+
+toSBool :: Bool -> SomeSBool
+toSBool True = SomeSBool STrue
+toSBool False = SomeSBool SFalse
+
+withSomeSBool :: SomeSBool -> (forall (b :: Bool). SBool b -> r) -> r
+withSomeSBool (SomeSBool s) f = f s
+
+class Monad (LoggingMonad b) => MonadLogging (b :: Bool) where
+  type LoggingMonad b = (r :: Type -> Type) | r -> b
+  logMsg :: String -> LoggingMonad b ()
+  runLogging :: LoggingMonad b a -> IO a
+
+instance MonadLogging 'False where
+  type LoggingMonad 'False = IO
+  logMsg _ = pure ()
+  runLogging = id
+
+instance MonadLogging 'True where
+  type LoggingMonad 'True = WriterT [String] IO
+  logMsg s = tell [s]
+  runLogging m = do
+    (a, w) <- runWriterT m
+    for_ w putStrLn
+    pure a
+
+program :: MonadLogging b => LoggingMonad b ()
+program = do
+  logMsg "hello world"
+  pure ()
+
+dict :: (c 'True, c 'False) => SBool b -> Dict (c b)
+dict STrue = Dict
+dict SFalse = Dict
+
+test :: Bool -> IO ()
+test bool =
+  withSomeSBool (toSBool bool) $ \(sb :: SBool b) ->
+    case dict @MonadLogging sb of
+      Dict -> runLogging @b program