Difference between revisions of "Output/Input"
(Types and instances for more mutable arrays added) |
m (Unlinked "IO, partible-style") |
||
(41 intermediate revisions by the same user not shown) | |||
Line 1: | Line 1: | ||
− | [[Category: |
+ | [[Category:Theoretical foundations]] |
+ | === <u>Clearing away the smoke and mirrors</u> === |
||
− | Let me guess...you've read every other guide, tutorial, lesson and introduction and none of them have helped - you still don't understand I/O in Haskell. |
||
+ | <div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
− | Alright then - have a look at this: |
||
+ | The implementation in GHC uses the following one: |
||
<haskell> |
<haskell> |
||
+ | type IO a = World -> (a, World) |
||
− | data OI -- abstract, primitive |
||
+ | </haskell> |
||
+ | An <code>IO</code> computation is a function that (logically) takes the state of the world, and returns a modified world as well as the return value. Of course, GHC does not actually pass the world around; instead, it passes a dummy “token,” to ensure proper sequencing of actions in the presence of lazy evaluation, and performs input and output as actual side effects! |
||
− | partOI :: OI -> (OI, OI) -- |
||
− | getchar :: OI -> Char -- primitives |
||
− | putchar :: Char -> OI -> () -- |
||
+ | <tt>[https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.168.4008&rep=rep1&type=pdf A History of Haskell: Being Lazy With Class], Paul Hudak, John Hughes, Simon Peyton Jones and Philip Wadler.</tt> |
||
− | seq :: a -> b -> b -- also primitive |
||
+ | </div> |
||
+ | ...so what starts out as an I/O action of type: |
||
− | instance Partible OI where ... |
||
+ | <haskell> |
||
− | class Partible a where |
||
− | + | World -> (a, World) |
|
− | parts :: a -> [a] |
||
− | . |
||
− | . |
||
− | . |
||
</haskell> |
</haskell> |
||
− | |||
− | No up-front explanation; I'm guessing you've seen more than enough of those, so I'm trying something different. I will explain it later... |
||
+ | is changed by GHC to approximately: |
||
− | Yes, of course there's more to Haskell I/O than <code>getchar</code> and <code>putchar</code>; I've downsized it for convenience. If you want, you can add the rest afterwards... |
||
− | |||
− | Yes, they're somewhat arcane, but they can be used to emulate all the classic approaches to I/O in Haskell, albeit in miniature: |
||
<haskell> |
<haskell> |
||
+ | () -> (a, ()) |
||
− | module ClassicIO where |
||
− | import qualified Prelude as T |
||
− | import Prelude(Char, String) |
||
− | import Prelude(($), (.)) |
||
− | import Data.List(map, foldr, zipWith) |
||
− | import OutputInput |
||
− | import Partible |
||
− | |||
− | -- simple text -- |
||
− | |||
− | {- main :: (String -> String) -} |
||
− | |||
− | runMain_text :: (String -> String) -> OI -> () |
||
− | runMain_text main = \u -> case part u of |
||
− | (u1, u2) -> |
||
− | putchars (main (getchars u1)) u2 |
||
− | |||
− | getchars :: OI -> String |
||
− | getchars = map getchar . parts |
||
− | |||
− | putchars :: String -> OI -> () |
||
− | putchars s = foldr seq () . zipWith putchar s . parts |
||
− | |||
− | |||
− | -- dialogues -- |
||
− | |||
− | {- main :: Dialogue -} |
||
− | |||
− | runMain_dial :: Dialogue -> OI -> () |
||
− | runMain_dial main = \u -> foldr seq () $ yet $ |
||
− | \l -> zipWith respond (main l) (parts u) |
||
− | |||
− | type Dialogue = [Response] -> [Request] |
||
− | |||
− | data Request = Getq | Putq Char |
||
− | data Response = Getp Char | Putp |
||
− | |||
− | yet :: (a -> a) -> a |
||
− | yet f = f (yet f) |
||
− | |||
− | respond :: Request -> OI -> Response |
||
− | respond Getq = \u -> case getchar u of c -> Getp c |
||
− | respond (Putq c) = \u -> seq (putchar c u) Putp |
||
− | |||
− | |||
− | -- continuations -- |
||
− | |||
− | {- main :: (() -> IOResult) -> IOResult -} |
||
− | |||
− | runMain_cont :: ((() -> IOResult) -> IOResult) -> OI -> () |
||
− | runMain_cont main = call (main done) |
||
− | |||
− | newtype IOResult = R (OI -> ()) |
||
− | |||
− | call :: IOResult -> OI -> () |
||
− | call (R a) = a |
||
− | |||
− | done :: () -> IOResult |
||
− | done () = R $ \ u -> part u `seq` () |
||
− | |||
− | getchar_cont :: (Char -> IOResult) -> IOResult |
||
− | getchar_cont k = R $ \u -> case part u of |
||
− | (u1, u2) -> |
||
− | case getchar u1 of |
||
− | c -> seq c (call (k c) u2) |
||
− | |||
− | putchar_cont :: Char -> (() -> IOResult) -> IOResult |
||
− | putchar_cont c k = R $ \u -> case part u of |
||
− | (u1, u2) -> |
||
− | seq (putchar c u1) (call (k ()) u2) |
||
− | |||
− | -- state-passing -- |
||
− | |||
− | {- main :: IOState -> ((), IOState) -} |
||
− | |||
− | runMain_stat :: (IOState -> ((), IOState)) -> OI -> () |
||
− | runMain_stat main = \u -> seq (main (ini_st u)) () |
||
− | |||
− | newtype IOState = S OI |
||
− | |||
− | ini_st :: OI -> IOState |
||
− | ini_st = S |
||
− | |||
− | getchar_stat :: IOState -> (Char, IOState) |
||
− | getchar_stat (S u) = case part u of |
||
− | (u1, u2) -> |
||
− | case getchar u1 of |
||
− | c -> seq c (c, S u2) |
||
− | |||
− | putchar_stat :: Char -> IOState -> ((), IOState) |
||
− | putchar_stat c (S u) = case part u of |
||
− | (u1, u2) -> |
||
− | seq (putchar c u1) ((), S u2) |
||
− | |||
− | -- and those weird, fickle things ;-) |
||
− | |||
− | {- main :: IO () -} |
||
− | |||
− | runMain_wfth :: IO () -> OI -> () |
||
− | runMain_wfth main = main |
||
− | |||
− | type IO a = OI -> a |
||
− | |||
− | getchar_wfth :: IO Char |
||
− | getchar_wfth = getchar |
||
− | |||
− | putchar_wfth :: Char -> IO () |
||
− | putchar_wfth = putchar |
||
− | |||
− | unit :: a -> IO a |
||
− | unit x = \u -> part u `seq` x |
||
− | |||
− | bind :: IO a -> (a -> IO b) -> IO b |
||
− | bind m k = \u -> case part u of |
||
− | (u1, u2) -> (\x -> x `seq` k x u2) (m u1) |
||
− | |||
− | -- supporting definitions -- |
||
− | -- |
||
− | getchar :: OI -> Char |
||
− | getchar = "getchar" `invokes` T.getChar |
||
− | |||
− | putchar :: Char -> OI -> () |
||
− | putchar c = "putchar" `invokes` T.putChar c |
||
</haskell> |
</haskell> |
||
− | + | As the returned unit-value <code>()</code> contains no useful information, that type can be simplified further: |
|
− | Now look closely at those imports... |
||
− | |||
− | Moving on, here are examples using each of those approaches: |
||
<haskell> |
<haskell> |
||
+ | () -> a |
||
− | module Echoes where |
||
+ | </haskell> |
||
− | import Prelude(String, Char(..), Eq(..)) |
||
− | import Prelude(($)) |
||
− | import ClassicIO |
||
− | import OutputInput(runOI) |
||
+ | <sub>Why "approximately"? Because "logically" a function in Haskell has no observable effects.</sub> |
||
− | echo_text :: String -> String |
||
− | echo_text (c:cs) = if c == '\n' then [] else c : echo_text cs |
||
+ | ---- |
||
− | echo_dial :: Dialogue |
||
+ | === <u>Previously seen</u> === |
||
− | echo_dial p = Getq : |
||
− | case p of |
||
− | Getp c : p' -> |
||
− | if c == '\n' then |
||
− | [] |
||
− | else |
||
− | Putq c : |
||
− | case p' of |
||
− | Putp : p'' -> echo_dial p'' |
||
+ | The type <code>() -> a</code> (or variations of it) have appeared elsewhere - examples include: |
||
− | echo_cont :: (() -> IOResult) -> IOResult |
||
− | echo_cont k = getchar_cont $ \c -> |
||
− | if c == '\n' then |
||
− | k () |
||
− | else |
||
− | putchar_cont c (\_ -> echo_cont k) |
||
+ | * page 2 of 13 in [https://fi.ort.edu.uy/innovaportal/file/20124/1/22-landin_correspondence-between-algol-60-and-churchs-lambda-notation.pdf A Correspondence Between ALGOL 60 and Church's Lambda-Notation: Part I] by Peter Landin: |
||
− | echo_stat :: IOState -> ((), IOState) |
||
+ | :{| |
||
− | echo_stat s = case getchar_stat s of |
||
+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
− | (c, s') -> |
||
− | if c == '\n' then |
||
− | ((), s') |
||
− | else |
||
− | case putchar_stat c s' of |
||
− | (_, s'') -> echo_stat s'' |
||
+ | The use of <code>λ</code>, and in particular (to avoid an irrelevant bound variable) of <code>λ()</code> , to delay and possibly avoid evaluation is exploited repeatedly in our model of ALGOL 60. A function that requires an argument-list of length zero is called a ''none-adic'' function. |
||
− | echo_wfth :: IO () |
||
+ | </div> |
||
− | echo_wfth = getchar_wfth `bind` \c -> |
||
+ | <sup> </sup> |
||
− | if c == '\n' then |
||
+ | <haskell> |
||
− | unit () |
||
+ | (\ () -> …) :: () -> a |
||
− | else |
||
− | putchar_wfth c `bind` \_ -> echo_wfth |
||
</haskell> |
</haskell> |
||
+ | |} |
||
+ | * page 148 of 168 in [[IO Semantics|Functional programming and Input/Output]] by Andrew Gordon: |
||
− | Regarding <code>seq</code>, this should work as expected[[#refs|[1][2][3]]]: |
||
+ | :{| |
||
− | |||
+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
+ | <pre> |
||
+ | abstype 'a Job = JOB of unit -> 'a |
||
+ | </pre> |
||
+ | </div> |
||
+ | <sup> </sup> |
||
<haskell> |
<haskell> |
||
+ | data Job a = JOB (() -> a) |
||
− | -- for GHC 8.6.5 |
||
− | {-# LANGUAGE CPP #-} |
||
− | #define during seq |
||
− | module Sequential(seq) where |
||
− | import qualified Prelude(during) |
||
− | |||
− | {-# NOINLINE seq #-} |
||
− | infixr 0 `seq` |
||
− | seq :: a -> b -> b |
||
− | seq x y = Prelude.during x (case x of _ -> y) |
||
</haskell> |
</haskell> |
||
+ | |} |
||
+ | * page 3 of [https://www.cs.bham.ac.uk/~udr/papers/assign.pdf Assignments for Applicative Languages] by Vipin Swarup, Uday S. Reddy and Evan Ireland: |
||
− | It didn't work? Try this instead: |
||
+ | :{| |
||
− | |||
+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
+ | A value of type <code>Obs 𝜏</code> is called an ''observer''. Such a value observes (i.e. views or inspects) a state and returns a value of type <code>𝜏</code>. [...] An observer type <code>Obs 𝜏</code> may be viewed as an implicit function space from the set of states to the type <code>𝜏</code>. |
||
+ | </div> |
||
+ | <sup> </sup> |
||
<haskell> |
<haskell> |
||
+ | type Obs tau = State -> tau |
||
− | -- for GHC 8.6.5 |
||
− | {-# LANGUAGE CPP #-} |
||
− | #define during seq |
||
− | module Sequential(seq) where |
||
− | import qualified Prelude(during) |
||
− | import GHC.Base(lazy) |
||
− | |||
− | infixr 0 `seq` |
||
− | seq :: a -> b -> b |
||
− | seq x y = Prelude.during x (lazy y) |
||
</haskell> |
</haskell> |
||
+ | |} |
||
+ | * [https://image.slidesharecdn.com/lazyio-120422092926-phpapp01/95/lazy-io-15-728.jpg page 15] of ''Non-Imperative Functional Programming'' by Nobuo Yamashita: |
||
− | As for those extensions - they stay with each definition. |
||
− | |||
− | That still didn't work? Well, give this a try: |
||
+ | :{| |
||
<haskell> |
<haskell> |
||
− | + | type a :-> b = OI a -> b |
|
− | yet f = y where y = f y |
||
</haskell> |
</haskell> |
||
+ | |} |
||
+ | * [http://h2.jaguarpaw.co.uk/posts/mtl-style-for-free MTL style for free] by Tom Ellis: |
||
− | Now that we're firmly on the topic of implementation details, did you notice how easy it was to define that allegedly ''warm, fuzzy''[[#refs|[4]]] <code>IO</code> type using this curious new <code>OI</code> type, and those primitives? |
||
− | |||
− | Sometimes that can be a hint that doing the opposite will be difficult or even impossible while staying within standard Haskell 2010. As it happens, this is one of those cases... |
||
− | |||
− | To define <code>OI</code>, <code>partOI</code>, <code>getchar</code> and <code>putchar</code> will require: |
||
− | |||
− | * modifying your preferred Haskell implementation - lots of work; |
||
− | |||
− | * using some other language for the definitions, with Haskell then calling the foreign code - extra work to deal with two different languages; |
||
− | |||
− | * using unsafe or implementation-specific primitives - work needed to avoid conflicts with Haskell semantics; |
||
− | |||
− | * using implementation-specific extensions - work needed to track relevant extensions, and possible conflicts with Haskell semantics. |
||
− | |||
− | For now, I'll just use the extensions - they're ugly, but at least they'll be contained, as they are in those alternate definitions of <code>seq</code>. But who knows - if this approach to I/O proves useful enough, it might make its way into a future Haskell standard...that's how <code>IO</code> happened[[#refs|[5]]]. |
||
− | |||
− | In the meantime, take a very deep breath: |
||
+ | :{| |
||
<haskell> |
<haskell> |
||
+ | data Time_ a = GetCurrentTime (UTCTime -> a) |
||
− | -- for GHC 8.6.5 |
||
− | {-# LANGUAGE MagicHash, UnboxedTuples #-} |
||
− | module OutputInput(OI, Monomo, runOI, invokes, seq) where |
||
− | import Prelude(Bool, Char, Double, Either, Float, Int, Integer, Maybe) |
||
− | import Prelude(String, Eq(..)) |
||
− | import Prelude(($), (++), error, all) |
||
− | import Control.Concurrent(ThreadId, MVar, Chan, QSem, QSemN) |
||
− | import Control.Concurrent.STM(STM, TVar, TMVar, TChan, TQueue, TBQueue) |
||
− | import Control.Concurrent.STM(TArray) |
||
− | import Control.Monad.ST(ST) |
||
− | import Data.Array(Array) |
||
− | import Data.Array.IO(IOArray) |
||
− | import Data.Array.ST(STArray) |
||
− | import Data.Char(isSpace) |
||
− | import Data.IORef(IORef) |
||
− | import Data.STRef(STRef) |
||
− | import Data.Time(UTCTime, NominalDiffTime, Day, TimeOfDay) |
||
− | import Data.Time(LocalTime, TimeZone, ZonedTime) |
||
− | import Data.Time(DiffTime) |
||
− | import Data.Time(UniversalTime) |
||
− | import System.Directory(XdgDirectory, XdgDirectoryList, Permissions) |
||
− | import System.IO(Handle, IOMode, BufferMode, SeekMode, HandlePosn) |
||
− | import System.IO(TextEncoding, Newline, NewlineMode) |
||
− | import Partible |
||
− | import Sequential |
||
− | import GHC.Base(IO(..), State#, MutVar#, RealWorld) |
||
− | import GHC.Base(seq#, newMutVar#, atomicModifyMutVar#, noDuplicate#) |
||
− | |||
− | data OI = OI OI# |
||
− | |||
− | instance Partible OI where |
||
− | part = partOI |
||
− | |||
− | partOI :: OI -> (OI, OI) |
||
− | partOI (OI h) = case part# h of (# h1, h2 #) -> (OI h1, OI h2) |
||
− | |||
− | runOI :: (OI -> a) -> IO a |
||
− | runOI g = IO $ \s -> case dispense# s of |
||
− | (# s', h #) -> seq# (g (OI h)) s' |
||
− | |||
− | invokes :: Monomo a => String -> IO a -> OI -> a |
||
− | (name `invokes` IO act) (OI h) |
||
− | = (name `invokes#` act) h |
||
− | |||
− | class Monomo a |
||
− | |||
− | -- local definitions -- |
||
− | -- |
||
− | type OI# = String -> State# RealWorld |
||
− | |||
− | part# :: OI# -> (# OI#, OI# #) |
||
− | part# h = case h "partOI" of |
||
− | s -> case dispense# s of |
||
− | (# s', h1 #) -> |
||
− | case dispense# s' of |
||
− | (# _, h2 #) -> (# h1, h2 #) |
||
− | |||
− | dispense# :: IO# OI# |
||
− | dispense# s = case newMutVar# () s of |
||
− | (# s', r #) -> (# s', expire# s' r #) |
||
− | |||
− | expire# :: State# s -> MutVar# s () -> String -> State# s |
||
− | expire# s r name = case atomicModifyMutVar# r use s of |
||
− | (# s', () #) -> s' |
||
− | where |
||
− | use x = (error nowUsed, x) |
||
− | nowUsed = name' ++ ": already expired" |
||
− | name' = if all isSpace name then "(unknown)" |
||
− | else name |
||
− | |||
− | invokes# :: Monomo a => String -> IO# a -> OI# -> a |
||
− | (name `invokes#` act) h = case act (noDuplicate# (h name)) of (# _, t #) -> t |
||
− | |||
− | type IO# a = State# RealWorld -> (# State# RealWorld, a #) |
||
− | |||
− | -- supplemental instances -- |
||
− | -- |
||
− | instance (Monomo a, Monomo b) => Monomo (Array a b) |
||
− | instance Monomo Bool |
||
− | instance Monomo BufferMode |
||
− | instance Monomo Char |
||
− | instance Monomo a => Monomo (Chan a) |
||
− | instance Monomo Day |
||
− | instance Monomo DiffTime |
||
− | instance Monomo Double |
||
− | instance (Monomo a, Monomo b) => Monomo (Either a b) |
||
− | instance Monomo Float |
||
− | instance Monomo Handle |
||
− | instance Monomo HandlePosn |
||
− | instance Monomo Int |
||
− | instance Monomo Integer |
||
− | instance Monomo (IO a) |
||
− | instance (Monomo a, Monomo b) => Monomo (IOArray a b) |
||
− | instance Monomo IOMode |
||
− | instance Monomo a => Monomo (IORef a) |
||
− | instance Monomo a => Monomo [a] |
||
− | instance Monomo LocalTime |
||
− | instance Monomo a => Monomo (Maybe a) |
||
− | instance Monomo a => Monomo (MVar a) |
||
− | instance Monomo Newline |
||
− | instance Monomo NewlineMode |
||
− | instance Monomo NominalDiffTime |
||
− | instance Monomo Permissions |
||
− | instance Monomo QSem |
||
− | instance Monomo QSemN |
||
− | instance Monomo SeekMode |
||
− | instance Monomo (ST s a) |
||
− | instance (Monomo a, Monomo b) => Monomo (STArray s a b) |
||
− | instance Monomo (STM a) |
||
− | instance Monomo a => Monomo (STRef s a) |
||
− | instance Monomo TextEncoding |
||
− | instance Monomo ThreadId |
||
− | instance Monomo TimeOfDay |
||
− | instance Monomo TimeZone |
||
− | instance (Monomo a, Monomo b) => Monomo (TArray a b) |
||
− | instance Monomo a => Monomo (TBQueue a) |
||
− | instance Monomo a => Monomo (TChan a) |
||
− | instance Monomo a => Monomo (TMVar a) |
||
− | instance Monomo a => Monomo (TQueue a) |
||
− | instance (Monomo a, Monomo b, Monomo c, Monomo d, Monomo e, Monomo f) => Monomo (a, b, c, d, e, f) |
||
− | instance (Monomo a, Monomo b, Monomo c, Monomo d, Monomo e) => Monomo (a, b, c, d, e) |
||
− | instance (Monomo a, Monomo b, Monomo c, Monomo d) => Monomo (a, b, c, d) |
||
− | instance (Monomo a, Monomo b, Monomo c) => Monomo (a, b, c) |
||
− | instance (Monomo a, Monomo b) => Monomo (a, b) |
||
− | instance Monomo a => Monomo (TVar a) |
||
− | instance Monomo () |
||
− | instance Monomo UniversalTime |
||
− | instance Monomo UTCTime |
||
− | instance Monomo XdgDirectory |
||
− | instance Monomo XdgDirectoryList |
||
− | instance Monomo ZonedTime |
||
</haskell> |
</haskell> |
||
+ | |} |
||
+ | * [http://h2.jaguarpaw.co.uk/posts/impure-lazy-language An impure lazy programming language], also by Tom Ellis: |
||
− | Now you can start breathing again :-) |
||
+ | :{| |
||
<haskell> |
<haskell> |
||
+ | data IO a = IO (() -> a) |
||
− | module Partible where |
||
− | import Data.Array |
||
− | import Data.List |
||
− | |||
− | class Partible a where |
||
− | part :: a -> (a, a) |
||
− | parts :: a -> [a] |
||
− | |||
− | -- Minimal complete definition: part or parts |
||
− | part u = case parts u of u1:u2:_ -> (u1, u2) |
||
− | parts u = case part u of (u1, u2) -> u1 : parts u2 |
||
− | |||
− | |||
− | instance (Ix a, Partible b) => Partible (Array a b) where |
||
− | part arr = case unzip (map part' (assocs arr)) of |
||
− | (al1, al2) -> (new al1, new al2) |
||
− | where |
||
− | new = array (bounds arr) |
||
− | part' (i, u) = case part u of |
||
− | (u1, u2) -> ((i, u1), (i, u2)) |
||
− | |||
− | instance (Partible a, Partible b) => Partible (Either a b) where |
||
− | parts (Left u) = map Left (parts u) |
||
− | parts (Right v) = map Right (parts v) |
||
− | |||
− | instance (Partible a, Partible b, Partible c, Partible d, Partible e) => Partible (a, b, c, d, e) where |
||
− | parts (u, v, w, x, y) = zipWith5 (,,,,) (parts u) (parts v) (parts w) (parts x) (parts y) |
||
− | |||
− | instance (Partible a, Partible b, Partible c, Partible d) => Partible (a, b, c, d) where |
||
− | parts (u, v, w, x) = zipWith4 (,,,) (parts u) (parts v) (parts w) (parts x) |
||
− | |||
− | instance (Partible a, Partible b, Partible c) => Partible (a, b, c) where |
||
− | parts (u, v, w) = zipWith3 (,,) (parts u) (parts v) (parts w) |
||
− | |||
− | instance (Partible a, Partible b) => Partible (a, b) where |
||
− | parts (u, v) = zipWith (,) (parts u) (parts v) |
||
</haskell> |
</haskell> |
||
+ | |} |
||
+ | * page 2 of [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.128.9269&rep=rep1&type=pdf Unique Identifiers in Pure Functional Languages] by Péter Diviánszky: |
||
− | If you remember, I dispensed with an up-front explanation to try something different. Now that you've |
||
+ | :{| |
||
− | seen just how different this all is, here's the explanation... |
||
+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
− | |||
+ | [...] The type <code>Id</code> can be hidden by the synonym data type |
||
− | That abstract <code>partOI</code> and its overloaded associates <code>part</code> and <code>parts</code>? They help an optimising Haskell implementation to determine when it's safe to use those optimisations. Consider this definition: |
||
+ | <pre> |
||
− | |||
+ | :: Create a :== Id -> a |
||
+ | </pre> |
||
+ | </div> |
||
+ | <sup> </sup> |
||
<haskell> |
<haskell> |
||
− | + | type Create a = Id -> a |
|
</haskell> |
</haskell> |
||
+ | |} |
||
+ | * page 7 of [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.701.930&rep=rep1&type=pdf Functional Reactive Animation] by Conal Elliott and Paul Hudak: |
||
− | One simple optimisation would be to replace the duplicates of <code>n^2</code> with a single, shared local definition: |
||
+ | :{| |
||
− | |||
+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
+ | An early implementation of Fran represented behaviors as implied in the formal semantics: |
||
<haskell> |
<haskell> |
||
+ | data Behavior a = Behavior (Time -> a) |
||
− | testme n = let x = n^2 in x + x |
||
</haskell> |
</haskell> |
||
+ | </div> |
||
+ | |} |
||
+ | * page 26 of [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf How to Declare an Imperative] by Philip Wadler: |
||
− | This definition: |
||
+ | :{| |
||
− | |||
+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
+ | The type <code>'a io</code> is represented by a function expecting a dummy argument of type <code>unit</code> and returning a value of type <code>'a</code>. |
||
+ | <pre> |
||
+ | type 'a io = unit -> a |
||
+ | </pre> |
||
+ | </div> |
||
+ | <sup> </sup> |
||
<haskell> |
<haskell> |
||
+ | type Io a = () -> a |
||
− | main' u = putchars "ha" u `seq` putchars "ha" u |
||
− | |||
</haskell> |
</haskell> |
||
+ | |} |
||
+ | * The [https://www.vex.net/~trebla/haskell/IO.xhtml Haskell I/O Tutorial] by Albert Lai: |
||
− | would likewise be rewritten, with the result being: |
||
+ | :{| |
||
+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
+ | But I can already tell you why we cannot follow other languages and use simply <code>X</code> or <code>() -> X</code>. |
||
+ | </div> |
||
+ | |} |
||
+ | * [http://comonad.com/reader/2011/free-monads-for-less-3 Free Monads for Less (Part 3 of 3): Yielding IO] by Edward Kmett: |
||
+ | :{| |
||
+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
<haskell> |
<haskell> |
||
+ | newtype OI a = forall o i. OI (FFI o i) o (i -> a) deriving Functor |
||
− | main' u = let x = putchars "ha" u in x `seq` x |
||
</haskell> |
</haskell> |
||
+ | </div> |
||
− | |||
+ | <sup> </sup> |
||
− | but, as noted by Philip Wadler[[#refs|[6]]]: |
||
− | |||
− | <blockquote>''[...] the laugh is on us: the program prints only a single <code>"ha"</code>, at the time variable <br><code>x</code> is bound. In the presence of side effects, equational reasoning in its simplest form <br>becomes invalid.''</blockquote> |
||
− | |||
− | ''Equational reasoning'' is the basis for that simple optimisation and many others in implementations like GHC - so far they've been serving us quite well. |
||
− | |||
− | What - just treat I/O-centric definitions as some special case by modifying GHC? Haskell implementations are complicated enough as is! |
||
− | |||
− | The problem is being caused by the code being treated as though it's pure, so let's modify the code instead. In this case, one simple solution is to make all calls to I/O-centric definitions unique: |
||
− | |||
<haskell> |
<haskell> |
||
− | + | type Oi a = forall i . i -> a |
|
− | (u1, u2) -> |
||
− | putchars "ha" u1 `seq` putchars "ha" u2 |
||
</haskell> |
</haskell> |
||
+ | |} |
||
+ | * page 27 of [https://blog.higher-order.com/assets/scalaio.pdf Purely Functional I/O in Scala] by Rúnar Bjarnason: |
||
− | But what about: |
||
+ | :{| |
||
− | |||
+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
+ | <pre> |
||
+ | class IO[A](run: () => A) |
||
+ | </pre> |
||
+ | </div> |
||
+ | <sup> </sup> |
||
<haskell> |
<haskell> |
||
− | + | class Io a where run :: () -> a |
|
− | |||
− | main' = oops (putchars "ha") (putchars "ha") |
||
</haskell> |
</haskell> |
||
+ | |} |
||
+ | * [https://stackoverflow.com/questions/6647852/haskell-actual-io-monad-implementation-in-different-language/6706442#6706442 ysdx's answer] to [https://stackoverflow.com/questions/6647852/haskell-actual-io-monad-implementation-in-different-language this SO question]: |
||
− | Will the laugh be on us, again? |
||
+ | :{| |
||
− | |||
+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
− | This is Haskell, not Clean[[#refs|[7]]] - there are no uniqueness types to help fend off such potentially-troublesome expressions. For now, the simplest way to make sure <code>OI</code> values are only used once is to have the implementation treat their reuse as being invalid e.g. by throwing an exception or raising an error to stop the offending program. |
||
+ | Let's say you want to implement <code>IO</code> in SML : |
||
− | |||
+ | <pre> |
||
− | In the prototype implementation, this all-important ''single-use'' property is maintained by <code>expire#</code>. |
||
+ | structure Io : MONAD = |
||
− | |||
+ | struct |
||
− | As for that curious <code>Monomo</code> class and its instances, they leverage Haskell's type system to provide an extra measure of safety for the prototype - an actual implementation would instead use an annotation[[#refs|[8]]] to achieve the same result e.g: |
||
+ | type 'a t = unit -> 'a |
||
− | |||
+ | ⋮ |
||
+ | end |
||
+ | </pre> |
||
+ | </div> |
||
+ | <sup> </sup> |
||
<haskell> |
<haskell> |
||
+ | type T a = () -> a |
||
− | newEmptyMVar :: monomo a . OI -> MVar a |
||
</haskell> |
</haskell> |
||
+ | |} |
||
+ | * [https://stackoverflow.com/questions/45136398/is-the-monadic-io-construct-in-haskell-just-a-convention/45141523#45141523 luqui's answer] to [https://stackoverflow.com/questions/45136398/is-the-monadic-io-construct-in-haskell-just-a-convention this SO question]: |
||
− | Now for the much-maligned[[#refs|[9][10]]] <code>seq</code>...you could be tempted into avoiding it by using a new data type: |
||
+ | :{| |
||
− | |||
− | <haskell> |
+ | |<haskell> |
− | newtype |
+ | newtype IO a = IO { runIO :: () -> a } |
− | |||
− | getchar' :: OI -> Result Char |
||
− | putchar' :: Char -> OI -> Result () |
||
</haskell> |
</haskell> |
||
+ | |} |
||
+ | * [https://stackoverflow.com/questions/15418075/the-reader-monad/15419592#15419592 luqui's answer] to [https://stackoverflow.com/questions/15418075/the-reader-monad this SO question]: |
||
− | and case-expressions: |
||
+ | :{| |
||
− | |||
− | <haskell> |
+ | |<haskell> |
− | + | newtype Supply r a = Supply { runSupply :: r -> a } |
|
− | respond' Getq = \u -> case getchar' u of Is c -> Getp c |
||
− | respond' (Putq c) = \u -> case putchar' c u of Is _ -> Putp |
||
</haskell> |
</haskell> |
||
+ | |} |
||
+ | * [https://stackoverflow.com/questions/51770808/how-exactly-does-ios-work-under-the-hood/51772273#51772273 chi's answer] to [https://stackoverflow.com/questions/51770808/how-exactly-does-ios-work-under-the-hood this SO question]: |
||
− | But before you succumb: |
||
+ | :{| |
||
+ | |<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote"> |
||
+ | As long as we have its special case <code>IO c = () ~> c</code>, we can represent (up to isomorphism) […] <code>a ~> c</code> […] |
||
+ | </div> |
||
+ | |} |
||
+ | Of these, it is the [https://hackage.haskell.org/package/oi/docs/src/Data-OI-Internal.html#OI implementation of <code>OI a</code>] in Yamashita's [https://hackage.haskell.org/package/oi oi] package which is most interesting as its values are ''monousal'' - once used, their contents remain constant. This single-use property also appears in the implementation of the abstract <code>decision</code> type described by F. Warren Burton in [https://academic.oup.com/comjnl/article-pdf/31/3/243/1157325/310243.pdf Nondeterminism with Referential Transparency in Functional Programming Languages]. |
||
− | <haskell> |
||
− | unit_Result :: a -> Result a |
||
− | unit_Result = Is |
||
+ | ---- |
||
− | bind_Result :: Result a -> (a -> Result b) -> Result b |
||
+ | === <code>IO</code><u>, redefined</u> === |
||
− | bind_Result (Is x) k = k x |
||
− | </haskell> |
||
+ | Based on these and other observations, a reasonable distillment of these examples would be <code>OI -> a</code>, which then implies: |
||
− | Oh look - <code>Result</code> is one of '''those''' types[[#refs|[11]]]... |
||
− | |||
− | The bang-pattern[[#refs|[12]]] extension? So you can instead write: |
||
<haskell> |
<haskell> |
||
+ | type IO a = OI -> a |
||
− | respond'' :: Request -> OI -> Response |
||
− | respond'' Getq = \u -> let !c = getchar u in Getp c |
||
− | respond'' (Putq c) = \u -> let !z = putchar c u in Putp |
||
</haskell> |
</haskell> |
||
+ | Using Burton's ''pseudodata'' approach: |
||
− | As you can see, <code>z</code> isn't used anywhere - there is no need for it. This being Haskell, if it isn't needed, it normally isn't evaluated. For now, the bang-pattern extension modifies the evaluation of |
||
− | <code>z</code> in order to prevent <code>respond''</code> being rewritten as: |
||
<haskell> |
<haskell> |
||
+ | -- abstract; single-use I/O-access mediator |
||
− | respond'' :: Request -> OI -> Response |
||
+ | data Exterior |
||
− | respond'' Getq = \u -> let !c = getchar u in Getp c |
||
+ | getchar :: Exterior -> Char |
||
− | respond'' (Putq c) = \u -> Putp |
||
+ | putchar :: Char -> Exterior -> () |
||
− | </haskell> |
||
+ | -- from section 2 of Burton's paper |
||
− | Will bang-patterns ever be included in a future Haskell standard? If so, will you still be able to use them like this? If not, will you be left with the clean-up job? |
||
+ | data Tree a = Node { contents :: a, |
||
+ | left :: Tree a, |
||
+ | right :: Tree a } |
||
+ | -- utility definitions |
||
− | Perhaps you'll find some other way for correctly sequencing the evaluation that you like; all well and good...but others might not. For me, the simplest way I've found to make this approach to I/O work is with <code>seq</code> - one that's actually sequential. |
||
+ | type OI = Tree Exterior |
||
+ | getChar' :: OI -> Char |
||
− | But maybe - after all that - you still want <code>seq</code> banished from Haskell. Perhaps you still don't understand I/O in Haskell. It could be that you're dismayed by what you've read here. Alternately, you may have seen or tried this all before, and know it doesn't work - darn... |
||
+ | getChar' = getchar . contents |
||
+ | putChar' :: Char -> OI -> () |
||
− | If that's you, the corresponding language proposal[[#refs|[13]]] has a list of other articles and research papers I've found which describe or refer to alternative approaches - perhaps one (or more) of them will be more acceptable. |
||
+ | putChar' c = putchar c . contents |
||
+ | part :: OI -> (OI, OI) |
||
− | As noted by Owen Stephens[[#refs|[14]]]: |
||
+ | parts :: OI -> [OI] |
||
+ | part t = (left t, right t) |
||
− | <blockquote>''I/O is not a particularly active area of research, but new approaches are still being discovered, <br>iteratees being a case in point.''</blockquote> |
||
+ | parts t = let !(t1, t2) = part t in |
||
+ | t1 : parts t2 |
||
+ | </haskell> |
||
+ | Of course, in an actual implementation <code>OI</code> would be abstract like <code>World</code>, and for similar reasons. This permits a simpler implementation for <code>OI</code> and its values, instead of being based on (theoretically) infinite structured values like binary trees. That simplicity has benefits for the <code>OI</code> interface, in this case: |
||
− | Who knows - the Haskell language could return to having a pure, fully-defined approach to I/O...and it could be you that finds it :-D |
||
+ | <haskell> |
||
+ | data OI |
||
+ | part :: OI -> (OI, OI) |
||
+ | getChar' :: OI -> Char |
||
+ | putChar' :: Char -> OI -> () |
||
+ | </haskell> |
||
+ | <sup> </sup> |
||
+ | ---- |
||
− | P.S: Why the name <code>OI</code>? Many years ago I was tinkering with arrows for performing I/O, labelling them <code>OI a b</code> out of expediency. More recently, I discovered a set of slides[[#refs|[15]]] describing another approach to I/O which used values of type <code>OI a</code> in a similar fashion to what I've been describing here. I've reused the name because of that similarity. |
||
− | |||
− | |||
− | <span id="refs">References</span>: |
||
− | |||
− | [1] [[Sequential ordering of evaluation]]; Haskell Wiki.<br> |
||
− | |||
− | [2] [https://gitlab.haskell.org/ghc/ghc/-/issues/5129 Ticket# 5129: "evaluate" optimized away]; GHC bug tracker.<br> |
||
+ | === <u>Various questions</u> === |
||
− | [3] [https://mail.haskell.org/pipermail/glasgow-haskell-users/2006-November/011480.html Thread: seq vs. pseq]; Haskell mail archive.<br> |
||
+ | * Is the C language "purely functional"? |
||
− | [4] [https://www.cs.nott.ac.uk/~pszgmh/appsem-slides/peytonjones.ppt Wearing the hair shirt: a retrospective on Haskell]; Simon Peyton Jones.<br> |
||
+ | ::No: |
||
− | [5] [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.168.4008&rep=rep1&type=pdf A History of Haskell: being lazy with class]; Paul Hudak, John Hughes, Simon Peyton Jones and Philip Wadler.<br> |
||
+ | ::* C isn't "pure" - it allows unrestricted access to observable effects, including those of I/O. |
||
+ | ::* C isn't "functional" - it was never intended to be [[Referential transparency|referentially transparent]], which severely restricts the ability to use [[Equational reasoning examples|equational reasoning]]. |
||
+ | * Is the Haskell language "purely functional"? |
||
− | [6] [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.91.3579&rep=rep1&type=pdf How to Declare an Imperative]; Philip Wadler.<br> |
||
+ | ::[https://chadaustin.me/2015/09/haskell-is-not-a-purely-functional-language Haskell is not a purely functional language], but is often described as being referentially transparent. |
||
− | [7] [https://clean.cs.ru.nl/Clean The Clean homepage]; Radboud University, Nijmegen, The Netherlands.<br> |
||
+ | * Can functional programming be liberated from the von Neumann paradigm? |
||
− | [8] [[Monomorphism by annotation of type variables]]; Haskell Wiki.<br> |
||
+ | ::That remains an [[Open research problems|open research problem]]. |
||
− | [9] [https://mail.haskell.org/pipermail/haskell/2002-May/009622.html Thread: State monads don't respect the monad laws in Haskell]; Haskell mail archive.<br> |
||
+ | * Can a language be "purely functional" or "denotative"? |
||
− | [10] [http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.71.1777&rep=rep1&type=pdf The Impact of ''seq'' on Free Theorems-Based Program Transformations]; Patricia Johann and Janis Voigtlander. |
||
+ | ::Conditionally, yes - the condition being the language is restricted in what domains it can be used in: |
||
− | [11] [[Monad]]; Haskell Wiki.<br> |
||
+ | ::* If a language is free of observable effects, including those of I/O, then the only other place where those effects can reside is within its implementation. |
||
− | [12] [https://downloads.haskell.org/~ghc/7.8.4/docs/html/users_guide/bang-patterns.html 7.18. Bang patterns]; GHC user's guide.<br> |
||
+ | ::* There is no bound on the ways in which observable effects can be usefully combined, leading to a similarly-unlimited variety of imperative computations. |
||
+ | ::* A finite implementation cannot possibly accommodate all of those computations, so a subset of them must be chosen. This restricts the implementation and language to those domains supported by the chosen computations. |
||
+ | * Why do our programs need to read input and write output? |
||
− | [13] [[Partibles for composing monads]]; Haskell Wiki.<br> |
||
+ | ::Because programs are usually written for [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.628.7053&rep=rep1&type=pdf practical] purposes, such as implementing domain-specific [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.2089&rep=rep1&type=pdf little languages] like [https://dhall-lang.org Dhall]. |
||
− | [14] [https://www.owenstephens.co.uk/assets/static/research/masters_report.pdf Approaches to Functional I/O]; Owen Stephens.<br> |
||
+ | ---- |
||
− | [15] <span style="color:#ba0000">Non-Imperative Functional Programming</span>; Nobuo Yamashita.<br> |
||
+ | === <u>See also</u> === |
||
+ | * [https://pqnelson.github.io/2021/07/29/monadic-io-in-ml.html Monadic IO in Standard ML] |
||
− | [[User:Atravers|Atravers]] 03:05, 20 August 2020 (UTC) |
||
+ | * [[Disposing of dismissives]] |
||
+ | * [[IO then abstraction]] |
||
+ | * [https://okmij.org/ftp/Computation/IO-monad-history.html The IO monad in 1965] |
Revision as of 12:36, 14 January 2022
Clearing away the smoke and mirrors
The implementation in GHC uses the following one:
type IO a = World -> (a, World)
An IO
computation is a function that (logically) takes the state of the world, and returns a modified world as well as the return value. Of course, GHC does not actually pass the world around; instead, it passes a dummy “token,” to ensure proper sequencing of actions in the presence of lazy evaluation, and performs input and output as actual side effects!
A History of Haskell: Being Lazy With Class, Paul Hudak, John Hughes, Simon Peyton Jones and Philip Wadler.
...so what starts out as an I/O action of type:
World -> (a, World)
is changed by GHC to approximately:
() -> (a, ())
As the returned unit-value ()
contains no useful information, that type can be simplified further:
() -> a
Why "approximately"? Because "logically" a function in Haskell has no observable effects.
Previously seen
The type () -> a
(or variations of it) have appeared elsewhere - examples include:
- page 2 of 13 in A Correspondence Between ALGOL 60 and Church's Lambda-Notation: Part I by Peter Landin:
The use of
λ
, and in particular (to avoid an irrelevant bound variable) ofλ()
, to delay and possibly avoid evaluation is exploited repeatedly in our model of ALGOL 60. A function that requires an argument-list of length zero is called a none-adic function.(\ () -> …) :: () -> a
- page 148 of 168 in Functional programming and Input/Output by Andrew Gordon:
abstype 'a Job = JOB of unit -> 'a
data Job a = JOB (() -> a)
- page 3 of Assignments for Applicative Languages by Vipin Swarup, Uday S. Reddy and Evan Ireland:
A value of type
Obs 𝜏
is called an observer. Such a value observes (i.e. views or inspects) a state and returns a value of type𝜏
. [...] An observer typeObs 𝜏
may be viewed as an implicit function space from the set of states to the type𝜏
.type Obs tau = State -> tau
- page 15 of Non-Imperative Functional Programming by Nobuo Yamashita:
type a :-> b = OI a -> b
- MTL style for free by Tom Ellis:
data Time_ a = GetCurrentTime (UTCTime -> a)
- An impure lazy programming language, also by Tom Ellis:
data IO a = IO (() -> a)
- page 2 of Unique Identifiers in Pure Functional Languages by Péter Diviánszky:
[...] The type
Id
can be hidden by the synonym data type:: Create a :== Id -> a
type Create a = Id -> a
- page 7 of Functional Reactive Animation by Conal Elliott and Paul Hudak:
An early implementation of Fran represented behaviors as implied in the formal semantics:
data Behavior a = Behavior (Time -> a)
- page 26 of How to Declare an Imperative by Philip Wadler:
The type
'a io
is represented by a function expecting a dummy argument of typeunit
and returning a value of type'a
.type 'a io = unit -> a
type Io a = () -> a
- The Haskell I/O Tutorial by Albert Lai:
But I can already tell you why we cannot follow other languages and use simply
X
or() -> X
.
- Free Monads for Less (Part 3 of 3): Yielding IO by Edward Kmett:
newtype OI a = forall o i. OI (FFI o i) o (i -> a) deriving Functor
type Oi a = forall i . i -> a
- page 27 of Purely Functional I/O in Scala by Rúnar Bjarnason:
class IO[A](run: () => A)
class Io a where run :: () -> a
Let's say you want to implement
IO
in SML :structure Io : MONAD = struct type 'a t = unit -> 'a ⋮ end
type T a = () -> a
newtype IO a = IO { runIO :: () -> a }
newtype Supply r a = Supply { runSupply :: r -> a }
As long as we have its special case
IO c = () ~> c
, we can represent (up to isomorphism) […]a ~> c
[…]
Of these, it is the implementation of OI a
in Yamashita's oi package which is most interesting as its values are monousal - once used, their contents remain constant. This single-use property also appears in the implementation of the abstract decision
type described by F. Warren Burton in Nondeterminism with Referential Transparency in Functional Programming Languages.
IO
, redefined
Based on these and other observations, a reasonable distillment of these examples would be OI -> a
, which then implies:
type IO a = OI -> a
Using Burton's pseudodata approach:
-- abstract; single-use I/O-access mediator
data Exterior
getchar :: Exterior -> Char
putchar :: Char -> Exterior -> ()
-- from section 2 of Burton's paper
data Tree a = Node { contents :: a,
left :: Tree a,
right :: Tree a }
-- utility definitions
type OI = Tree Exterior
getChar' :: OI -> Char
getChar' = getchar . contents
putChar' :: Char -> OI -> ()
putChar' c = putchar c . contents
part :: OI -> (OI, OI)
parts :: OI -> [OI]
part t = (left t, right t)
parts t = let !(t1, t2) = part t in
t1 : parts t2
Of course, in an actual implementation OI
would be abstract like World
, and for similar reasons. This permits a simpler implementation for OI
and its values, instead of being based on (theoretically) infinite structured values like binary trees. That simplicity has benefits for the OI
interface, in this case:
data OI
part :: OI -> (OI, OI)
getChar' :: OI -> Char
putChar' :: Char -> OI -> ()
Various questions
- Is the C language "purely functional"?
- No:
- C isn't "pure" - it allows unrestricted access to observable effects, including those of I/O.
- C isn't "functional" - it was never intended to be referentially transparent, which severely restricts the ability to use equational reasoning.
- No:
- Is the Haskell language "purely functional"?
- Haskell is not a purely functional language, but is often described as being referentially transparent.
- Can functional programming be liberated from the von Neumann paradigm?
- That remains an open research problem.
- Can a language be "purely functional" or "denotative"?
- Conditionally, yes - the condition being the language is restricted in what domains it can be used in:
- If a language is free of observable effects, including those of I/O, then the only other place where those effects can reside is within its implementation.
- There is no bound on the ways in which observable effects can be usefully combined, leading to a similarly-unlimited variety of imperative computations.
- A finite implementation cannot possibly accommodate all of those computations, so a subset of them must be chosen. This restricts the implementation and language to those domains supported by the chosen computations.
- Why do our programs need to read input and write output?
- Because programs are usually written for practical purposes, such as implementing domain-specific little languages like Dhall.