InitialHEADmaster

1 files changed, 79 insertions, 0 deletions

diff --git a/ch14_14.1.example.hs b/ch14_14.1.example.hs
new file mode 100644
index 0000000..91bfcbf
--- /dev/null
+++ b/ch14_14.1.example.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE RebindableSyntax #-}
+
+import Control.Monad.Indexed qualified as I
+import Data.Coerce (coerce)
+import Fcf (Eval, Filter, Find, IsJust, Not, TyEq, type (<=<), type (=<<))
+import GHC.TypeLits (Nat, type (+))
+import Language.Haskell.DoNotation (Monad, pure, (>>=))
+import System.IO qualified as IO
+import Prelude hiding (Monad, pure, (>>=))
+
+newtype Ix m i j a = Ix
+  { unsafeRunIx :: m a
+  }
+  deriving (Functor, Applicative, Monad)
+
+instance Functor m => I.IxFunctor (Ix m) where
+  imap = fmap
+
+instance (Applicative m, Monad m) => I.IxPointed (Ix m) where
+  ireturn = pure
+
+instance (Applicative m, Monad m) => I.IxApplicative (Ix m) where
+  iap :: forall i j k a b. Ix m i j (a -> b) -> Ix m j k a -> Ix m i k b
+  iap = coerce $ (<*>) @m @a @b
+
+instance Monad m => I.IxMonad (Ix m) where
+  ibind :: forall i j k a b. (a -> Ix m j k b) -> Ix m i j a -> Ix m i k b
+  ibind = coerce $ (=<<) @m @a @b
+
+data LinearState = LinearState
+  { linearNextKey :: Nat
+  , linearOpenKeys :: [Nat]
+  }
+
+newtype Linear s (i :: LinearState) (j :: LinearState) a = Linear
+  { unsafeRunLinear :: Ix IO i j a
+  }
+  deriving (I.IxFunctor, I.IxPointed, I.IxApplicative, I.IxMonad)
+
+newtype Handle s key = Handle
+  { unsafeGetHandle :: IO.Handle
+  }
+
+openFile
+  :: FilePath
+  -> IO.IOMode
+  -> Linear
+      s
+      ('LinearState next open)
+      ('LinearState (next + 1) (next ': open))
+      (Handle s next)
+openFile = coerce IO.openFile
+
+type IsOpen (key :: k) (ts :: [k]) = IsJust =<< Find (TyEq key) ts
+
+type Close (key :: k) (ts :: [k]) = Filter (Not <=< TyEq key) ts
+
+closeFile
+  :: Eval (IsOpen key open) ~ 'True
+  => Handle s key
+  -> Linear
+      s
+      ('LinearState next open)
+      ('LinearState next (Eval (Close key open)))
+      ()
+closeFile = coerce IO.hClose
+
+-- If I try to write this point-free GHC gets angry. Not sure why that is:
+--
+-- • Couldn't match representation of type ‘a0’ with that of ‘IO a’
+--     arising from a use of ‘coerce’
+--
+-- 79 | runLinear = coerce
+--    |             ^^^^^^
+runLinear :: (forall s. Linear s ('LinearState 0 '[]) ('LinearState n '[]) a) -> IO a
+runLinear a = coerce a