{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}

-- |
-- Module      : FileIO
-- Description : The Linear File IO example from the Linear Haskell paper.
--
-- We implement a function that prints the first line of a file.
--
-- We do this with the normal file IO interface in base and the linear file IO
-- interface in linear-base. With the latter, the protocol for using files is
-- enforced by the linear type system. For instance, forgetting to close the file
-- will induce a type error at compile time. That is, typechecking proves that all
-- opened files are closed at some later point in execution. With the former
-- interface, we have code that type checks but will error or cause errors at
-- runtime.
module Simple.FileIO where

-- Linear Base Imports
import qualified Control.Functor.Linear as Control
import Control.Monad ()
import Data.Text
import Data.Unrestricted.Linear
import qualified System.IO as System
import qualified System.IO.Resource.Linear as Linear
import Prelude

-- *  Non-linear first line printing

--------------------------------------------

-- openFile :: FilePath -> IOMode -> IO Handle
-- IOMode = ReadMode | WriteMode | AppendMode | ReadWriteMode
-- hGetLine :: Handle -> IO String
-- hPutStr :: Handle -> String -> IO ()
-- hClose :: Handle -> IO ()

printFirstLine :: FilePath -> System.IO ()
printFirstLine :: FilePath -> IO ()
printFirstLine FilePath
fpath = do
  Handle
fileHandle <- FilePath -> IOMode -> IO Handle
System.openFile FilePath
fpath IOMode
System.ReadMode
  FilePath
firstLine <- Handle -> IO FilePath
System.hGetLine Handle
fileHandle
  FilePath -> IO ()
System.putStrLn FilePath
firstLine
  Handle -> IO ()
System.hClose Handle
fileHandle

-- This compiles but can cause issues!
-- The number of file handles you can have active is finite and after that
-- openFile errors. This is especially critical on mobile devices or systems
-- with limited resources.
printFirstLineNoClose :: FilePath -> System.IO ()
printFirstLineNoClose :: FilePath -> IO ()
printFirstLineNoClose FilePath
fpath = do
  Handle
fileHandle <- FilePath -> IOMode -> IO Handle
System.openFile FilePath
fpath IOMode
System.ReadMode
  FilePath
firstLine <- Handle -> IO FilePath
System.hGetLine Handle
fileHandle
  FilePath -> IO ()
System.putStrLn FilePath
firstLine

-- This compiles, but will throw an error!
printFirstLineAfterClose :: FilePath -> System.IO ()
printFirstLineAfterClose :: FilePath -> IO ()
printFirstLineAfterClose FilePath
fpath = do
  Handle
fileHandle <- FilePath -> IOMode -> IO Handle
System.openFile FilePath
fpath IOMode
System.ReadMode
  Handle -> IO ()
System.hClose Handle
fileHandle
  FilePath
firstLine <- Handle -> IO FilePath
System.hGetLine Handle
fileHandle
  FilePath -> IO ()
System.putStrLn FilePath
firstLine

-- * Linear first line printing

--------------------------------------------

linearGetFirstLine :: FilePath -> RIO (Ur Text)
linearGetFirstLine :: FilePath -> RIO (Ur Text)
linearGetFirstLine FilePath
fp = Control.do
  Handle
handle <- FilePath -> IOMode -> RIO Handle
Linear.openFile FilePath
fp IOMode
System.ReadMode
  (Ur Text
t, Handle
handle') <- Handle %1 -> RIO (Ur Text, Handle)
Linear.hGetLine Handle
handle
  Handle %1 -> RIO ()
Linear.hClose Handle
handle'
  Ur Text %1 -> RIO (Ur Text)
forall (m :: * -> *) a. Monad m => a %1 -> m a
Control.return Ur Text
t

linearPrintFirstLine :: FilePath -> System.IO ()
linearPrintFirstLine :: FilePath -> IO ()
linearPrintFirstLine FilePath
fp = do
  Text
text <- RIO (Ur Text) -> IO Text
forall a. RIO (Ur a) -> IO a
Linear.run (FilePath -> RIO (Ur Text)
linearGetFirstLine FilePath
fp)
  FilePath -> IO ()
System.putStrLn (Text -> FilePath
unpack Text
text)

{-
    For clarity, we show this function without do notation.

    Note that the current approach is limited.
    We have to make the continuation use the unit type.

    Enabling a more generic approach with a type index
    for the multiplicity, as descibed in the paper is a work in progress.
    This will hopefully result in using

    `(>>==) RIO 'Many a %1-> (a -> RIO p b) %1-> RIO p b`

    as the non-linear bind operation.
    See https://github.com/tweag/linear-base/issues/83.
-}

-- * Linear and non-linear combinators

-------------------------------------------------

-- Some type synonyms
type RIO = Linear.RIO

type LinHandle = Linear.Handle

-- | Linear bind
-- Notice the continuation has a linear arrow,
-- i.e., (a %1-> RIO b)
(>>#=) :: RIO a %1 -> (a %1 -> RIO b) %1 -> RIO b
>>#= :: forall a b. RIO a %1 -> (a %1 -> RIO b) %1 -> RIO b
(>>#=) = RIO a %1 -> (a %1 -> RIO b) %1 -> RIO b
forall a b. RIO a %1 -> (a %1 -> RIO b) %1 -> RIO b
forall (m :: * -> *) a b.
Monad m =>
m a %1 -> (a %1 -> m b) %1 -> m b
(Control.>>=)

infixl 1 >>#= -- same fixity as base.>>=

-- | Non-linear bind
-- Notice the continuation has a non-linear arrow,
-- i.e., (() -> RIO b). For simplicity, we don't use
-- a more general type, like the following:
-- (>>==) :: RIO (Ur a) %1-> (a -> RIO b) %1-> RIO b
(>>==) :: RIO () %1 -> (() -> RIO b) %1 -> RIO b
>>== :: forall b. RIO () %1 -> (() -> RIO b) %1 -> RIO b
(>>==) RIO ()
ma () -> RIO b
f = RIO ()
ma RIO () %1 -> (() %1 -> RIO b) %1 -> RIO b
forall a b. RIO a %1 -> (a %1 -> RIO b) %1 -> RIO b
forall (m :: * -> *) a b.
Monad m =>
m a %1 -> (a %1 -> m b) %1 -> m b
Control.>>= (\() -> () -> RIO b
f ())

infixl 1 >>== -- same fixity as base.>>=

-- | Inject
-- provided just to make the type explicit
inject :: a %1 -> RIO a
inject :: forall a. a %1 -> RIO a
inject = a %1 -> RIO a
forall (m :: * -> *) a. Monad m => a %1 -> m a
Control.return

-- * The explicit example

-------------------------------------------------

getFirstLineExplicit :: FilePath -> RIO (Ur Text)
getFirstLineExplicit :: FilePath -> RIO (Ur Text)
getFirstLineExplicit FilePath
path =
  (FilePath -> RIO Handle
openFileForReading FilePath
path)
    RIO Handle
%1 -> (Handle %1 -> RIO (Ur Text, Handle))
%1 -> RIO (Ur Text, Handle)
forall a b. RIO a %1 -> (a %1 -> RIO b) %1 -> RIO b
>>#= Handle %1 -> RIO (Ur Text, Handle)
readOneLine
    RIO (Ur Text, Handle)
%1 -> ((Ur Text, Handle) %1 -> RIO (Ur Text)) %1 -> RIO (Ur Text)
forall a b. RIO a %1 -> (a %1 -> RIO b) %1 -> RIO b
>>#= (Ur Text, Handle) %1 -> RIO (Ur Text)
closeAndReturnLine -- Internally uses (>>==)
  where
    openFileForReading :: FilePath -> RIO LinHandle
    openFileForReading :: FilePath -> RIO Handle
openFileForReading FilePath
fp = FilePath -> IOMode -> RIO Handle
Linear.openFile FilePath
fp IOMode
System.ReadMode
    readOneLine :: LinHandle %1 -> RIO (Ur Text, LinHandle)
    readOneLine :: Handle %1 -> RIO (Ur Text, Handle)
readOneLine = Handle %1 -> RIO (Ur Text, Handle)
Linear.hGetLine
    closeAndReturnLine ::
      (Ur Text, LinHandle) %1 -> RIO (Ur Text)
    closeAndReturnLine :: (Ur Text, Handle) %1 -> RIO (Ur Text)
closeAndReturnLine (Ur Text
unrText, Handle
handle) =
      Handle %1 -> RIO ()
Linear.hClose Handle
handle RIO () %1 -> (() %1 -> RIO (Ur Text)) %1 -> RIO (Ur Text)
forall a b. RIO a %1 -> (a %1 -> RIO b) %1 -> RIO b
>>#= (\() -> Ur Text %1 -> RIO (Ur Text)
forall a. a %1 -> RIO a
inject Ur Text
unrText)

printFirstLineExplicit :: FilePath -> System.IO ()
printFirstLineExplicit :: FilePath -> IO ()
printFirstLineExplicit FilePath
fp = do
  Text
firstLine <- RIO (Ur Text) -> IO Text
forall a. RIO (Ur a) -> IO a
Linear.run (RIO (Ur Text) -> IO Text) -> RIO (Ur Text) -> IO Text
forall a b. (a -> b) -> a -> b
$ FilePath -> RIO (Ur Text)
getFirstLineExplicit FilePath
fp
  FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Text -> FilePath
unpack Text
firstLine