Created
May 18, 2023 20:01
-
-
Save monadplus/68c8df9bb4115665d40e894877533875 to your computer and use it in GitHub Desktop.
Haskell: indexed monad example
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE DerivingVia #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE RebindableSyntax #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE TypeOperators #-} | |
module IxMonad where | |
import Control.Monad.Indexed | |
import Control.Monad.Trans.Ix | |
import Data.Coerce | |
import Fcf hiding (type (+)) | |
import GHC.TypeLits (Nat, type (+)) | |
import Language.Haskell.DoNotation | |
import System.IO hiding (Handle, openFile) | |
import qualified System.IO as IO | |
import Prelude hiding (Monad (..), pure) | |
data LinearState = LinearState | |
{ linearNextKey :: Nat, | |
linearOpenKeys :: [Nat] | |
} | |
newtype Linear s (i :: LinearState) (j :: LinearState) a = Linear {unsafeRunLinear :: IO a} | |
deriving (IxFunctor, IxPointed, IxApplicative, IxMonad) via (Ix IO) | |
lift :: IO a -> Linear s i i a | |
lift = coerce | |
openFile :: | |
FilePath -> | |
IOMode -> | |
Linear | |
s | |
('LinearState next open) | |
('LinearState (next + 1) (next ': open)) | |
(Handle s next) | |
openFile = coerce IO.openFile | |
-- 's' is a rigid skolem type variable | |
-- and prevents leaking the value outside 'runLinear' | |
newtype Handle s key = Handle {unsafeGetHandle :: IO.Handle} | |
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 | |
runLinear :: | |
(forall s. Linear s ('LinearState 0 '[]) ('LinearState n '[]) a) -> IO a | |
runLinear = coerce | |
-- OK | |
main :: IO () | |
main = runLinear $ do | |
h <- openFile "/etc/passwd" ReadMode | |
lift $ IO.hPutStr (coerce h) "\nroot:x:0:0::/root:/bin/bash" | |
closeFile h | |
-- BOGUS: we forgot to close the file handle | |
-- | |
-- main :: IO () | |
-- main = runLinear $ do | |
-- h <- openFile "/etc/passwd" ReadMode | |
-- lift $ IO.hPutStr (coerce h) "\nroot:x:0:0::/root:/bin/bash" |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment