What are functional programming months

Introduction to functional programming

Transcript

1 Introduction to functional programming Prof. Dr. Manfred Schmidt-Schauÿ Artificial Intelligence and Software Technology November 20, 2006

2 monads and I / O monads is a data type for (sequential) actions i.a .: parameterized with internal state and output type of the actions encapsulated passing on of the state combiners for actions encapsulation is usually encapsulated. the state and the passing on of the state Introduction to functional programming, fol

3 monads important use of monads sequencing concepts of imperative programming and side effects in pure, referential transparent form input-output, i.e. IO stateful calculations single-threaded objects to be used introduction to functional programming, fol

4 Monads: Limits If the outside world changes without the influence of the program: Sequentiality helps, but the theoretical model does not fit. The monad model does not support interchangeable inputs and outputs. Implementation of the monads does not correspond to the pure lambda calculus: no call-by-name theory but call-by-need theory There are non-monadic approaches to input-output in functional programming language Introduction to functional programming, fol

5 monads in Haskell's special monad syntax; supported by the compiler monads are implemented as type classes. The type class system and the type checker in Haskell are essential for the correct and safe use of monads. Introduction to functional programming, fol

6 Type class Monad Monad with type constructor m Objects of type (ma) are actions with output type a Monad methods are: >> =: sequential linking of two actions return: creation of an action Sometimes actions are already predefined Note: Monad is a constructor class Introduction to the functional programming, fol

7 Type class Monad programming = construction of compound actions. The result is obtained by applying: (combined action) applied to (input) no direct access to the internal state. Introduction to functional programming, fol

8 actions init action action State: A State: B State: C return Introduction to functional programming, fol

9 Type class Monad Definition of the type class Monad in the Haskell Prelude: class Monad m where return :: a -> ma (>> =) :: ma -> (a -> mb) -> mb --- (Bind) (> >) :: ma -> mb -> mb fail :: String -> ma - Minimal complete definition: (>> =), return p >> q = p >> = \ _ -> q fail s = error s The operator >> = is also called a bind. Introduction to functional programming, fol

10 Monad: the do notation a1 >> = (\ x -> a2 >> = (\ y -> a3 >> = \ _-> return (x, y))) can be written more easily than: do {x <- a1; y <- a2; a3; return (x, y)} Caution x <- a1 does not mean that a1 and x are bound! but: the value of the action a1 is tied to x Introduction to functional programming, fol

11 Monad: the do notation Translation rules for the do notation: do {x <- e; s} = e >> = \ x-> do {s} do {e; s} = e >> do {s} do {e} = e Introduction to functional programming, fol

12 Monad: algebraic properties Monad laws: 1: return x >> = f = fx 2: m >> = return = m 3: m1 >> = (\ x-> m2 >> = \ y-> m3) = (m1 >> = \ x-> m2) >> = \ y-> m3 if x FV (m3) Introduction to functional programming, fol

13 Monad: algebraic properties Property of the bind operation using do: do {x <- m 1; do {y <- do {x <- m 1; y <- m 2; = m 2}; m 3 m 3} Unfortunately the type system or the compiler cannot check the validity of these laws when a data type is declared to be an instance of monad. The programmer is responsible for this. Introduction to functional programming, fol

14 Examples: Data structures as monads data Maybe a = Nothing Just a becomes a monad: instance Monad Maybe where Just x >> = k = k x Nothing >> = k = Nothing return = Just fail s = Nothing Introduction to functional programming, fol

15 Recalculating the laws of monads 1: return x >> = f = fx 2: m >> = return = m 3: m1 >> = (\ x-> m2 >> = \ y-> m3) = (m1> > = \ x-> m2) >> = \ y-> m3 if x FV (m3) instance Monad Maybe where Just x >> = k = kx Nothing >> = k = Nothing return = Just fail s = Nothing Introduction to functional programming, fol

16 Recalculating the laws of monads Recalculating by defining Maybe We use the call-by-need variant of a lambda calculus, which let uses as a syntactic construct to model sharing. We assume that it has already been proven that reduction preserves equality and that some transformation rules have already been proven to be correct. Note that call-by-name with beta reduction must not be used in connection with proving the correctness of the monad laws. Introduction to functional programming, fol

17 Recalculating the Monad Laws 1. return x >> = f = f x: Just x >> = f is just defined as f x. 2. m >> = return = m: m >> = Just: m can only be Just x or Nothing in terms of type. In the first case the result is Just x, i.e. m. In the second case m = Nothing, the result is Nothing, i.e. also m. Introduction to functional programming, fol

18 Recalculating the Laws of Monads 3. We verify the third law of monads: If m_1 = Nothing, then the left side results in Nothing. After applying the definition twice, the right-hand side also yields Nothing. If m_1 = Just s, the result on the left is: let x = s in m_2 >> = \ y -> m_3. On the right side the result is: (let x = s in m_2) >> = \ y -> m_3. The equation is correct because the transformation of the let-shift outwards is correct. Introduction to functional programming, fol

19 Lists as monads Lists can be seen as monads with the definitions: instance Monad [] where (x: xs) >> = f = fx ++ (xs >> = f) [] >> = f = [] return x = [x] fail s = [] Introduction to functional programming, fol

20 algebraic rules of the list monad 1. [x] >> = f = f x ++ ([] >> = f) = f x. 2. m >> = \ x -> [x] gives for m = [] again [] m = s: zs gives the expression let x = s, xs = zs in [x] ++ (xs >> = \ y -> [y]). right side is right after let-slide. m = bot gives bot on both sides Induction can be carried out for finite lists, for infinite lists: Induction with an extra base case bot The call-by-need calculus should also be used here! Introduction to functional programming, fol

21 List monad and do notation The do notation is analogous to list comprehensions: [e x <- xs; y <- ys] corresponds to the notation: do {x <- xs; y <- ys; return e} The equivalent bind definition that fits the transformation rules for list comprehensions: xs >> = f = concat (map f xs) List comprehensions can do a little more than the do notation: predicates and patterns. Introduction to functional programming, fol

22 State monad State monad encapsulates actions that change a state allows sequential composition of actions newtype StateTransformer sa = ST (s -> (a, s)) - s State type - a Type of output value - s -> (a, s ) Type of an action apply :: StateTransformer sa -> s -> (a, s) apply (ST f) x = fx instance Monad (StateTransformer s) where return x = ST $ \ s -> (x, s) a1> > = aa2 = ST action where action = \ s -> let (res, s) = apply a1 s in apply (aa2 res) s Introduction to functional programming, fol

23 State monad Example Example: Account balance that can be changed: --- Operations on the state: incr = ST $ \ s -> ((), s + 1) decr = ST $ \ s -> ((), s- 1) hole = ST $ \ s -> (s, s) add n = ST $ \ s -> ((), s + n) sub n = ST $ \ s -> ((), s - n) clear = ST $ \ _ -> ((), 0) check p = ST $ \ s -> (ps, s) beginning = ST (\ ein -> ((), ein)) Introduction to functional programming, fol

24 state monad Example test = (start >> incr >> incr >> add 3 >> hole) show test = (apply test 4444)> (4449,4449) :: (integer, integer) test2 = start >> incr >> add 3 >> sub 5 show test2 = (apply test2 3333)> ((), 3332) :: ((), Integer) Introduction to functional programming, fol

25 Control structures for actions Examples of control structures: forever :: Monad m => ma -> mb forever a = a >> forever a repeatn :: (Monad a, Num b) => b -> ac -> a () repeatn 0 a = return () repeatn na = a >> repeatn (n-1) a Introduction to functional programming, fol

26 Control structures for actions Examples repeatn :: (Monad m, Num a) => a -> mb -> m () repeatn 0 a = return () repeatn na = a >> repeatn (n-1) a test3 = beginning> > incr >> (repeatn 5 (add 3)) >> sub 5 show test3 = (apply test3 6666)> ((), 6677) :: ((), Integer) Introduction to functional programming, fol

27 Control structures for actions for has a list as input and a function fa that generates an action from each list element: - Action per element of a list for :: Monad m => [a] -> (a -> mc) -> m () for [] fa = return () for (n: ns) fa = fa n >> for ns fa ---- alternatively: for ns fa = sequence_ (map fa ns) - where: sequence_ :: Monad a => [ab] -> a () - sequence_ as = foldr (>>) (return ()) as - print :: Show a => a -> IO () testprint numbers = for [1..10 ] print Introduction to functional programming, fol

28 Control structures for actions sequence: Results of the actions in a list sequence [] = return [] sequence (a: as) = ​​do {r <- a; rs <- sequence as; return (r: rs)} Introduction to functional programming, fol

29 Control structures for actions while :: Monad m => m Bool -> m a -> m () while check a = do {b <- check; if b then a >> while check a else return ()} test4 = beginning >> (add 10) >> while (check (\ x -> x> 0)) decr show test4 = (apply test4 7777)> (() , 0) :: ((), Integer) Introduction to functional programming, fol

30 Monadic IO in Haskell input / output by means of actions Actions of the type IO a, action operate on world a is the type of the return value Haskell program = action of the type IO (). Program is applied to World Return value: World may have changed Introduction to functional programming, fol

31 Monadic IO in Haskell model concept The type IO a is an abbreviation for: type IO a = World -> (a, World) An action of the type IO a returns a pair: Value of the type a World: (changed outside world) Monadic programming forces single-threaded use of world World cannot be copied in the program. Introduction to functional programming, fol

32 Monadic IO; Instance definition instance Monad IO where (>> =) = primbindio return = primretio New definition in the Haskell Wiki: instance Monad IO where (>> =) = ... return = ... fail s = ioerror (usererror s) The functions that are not displayed are predefined and cannot be implemented or replaced by yourself. Introduction to functional programming, fol

33 Monadic IO; Examples are predefined: getchar :: IO Char - World -> (Char, World) putchar :: Char -> IO () - Char -> (World -> ((), World)) IO programming relies on the predefined basic IO actions on introduction to functional programming, fol

34 IO functions Examples The getchar and putchar actions can be combined to echo using >> =: echo :: IO () echo = getchar >> = putchar Bind causes sequential execution with argument transfer Used type instance of >> = IO Char -> ( Char -> IO ()) -> IO () Introduction to functional programming, fol

35 IO functions Examples double echo: getchar >> = (\ c -> putchar c >> putchar c) read in and output a line: getline :: IO [Char] getline = getchar >> = \ c -> if c == \ n then return [] else getline >> = \ cs -> return (c: cs) putline :: [Char] -> IO () putline [] = return () putline (c: cs) = putchar c >> putline cs Introduction to functional programming, fol

36 Notation with do Example: >> = - notation translated into do notation. getline = getchar >> = \ c -> if c == \ n then return [] else getline >> = \ cs -> return (c: cs) getline = do {c <- getchar; if c == \ n then return [] else do {cs <- getline; return (c: cs)}} Introduction to functional programming, fol

37 cells using IORef (from Haskell Hierarchical Liberaries) External memory cells: data IORef a - as in ML newioref :: a -> IO (IORef a) readioref :: IORef a -> IO a writeioref :: IORef a -> a - > IO () count :: Int -> IO Int count n = do {r <- newioref 0; loop r 1} where loop r i i> n = readioref r otherwise = do {v <- readioref r; writeioref r (v + i); loop r (i + 1)} Introduction to functional programming, fol

38 cells using IORef testing the count action: * Main> do {n <- count 0; print n} 0 * Main> do {n <- count 10; print n} 55 Introduction to functional programming, fol

39 Treatment of the outside world All interactions with World only through IO actions. Condition There is always only one World object in the current state World may not be copied, i.e. no old versions may be kept This is guaranteed by a single-threaded treatment of World Introduction to functional programming, fol

40 Properties of the IO monad So that input / output in Haskell functions correctly and programming remains pure, the following properties and restrictions apply: A Haskell program is an IO action, i.e. of the IO () type. IO actions can only be combined with >> = single user-definable basic action by means of return reliable sequencing of the associated IO actions IO actions can be used as required in the program. IO monad has no hole. The result of main is only obtained after the end of the program Introduction to functional programming, fol

41 An unsafe way out unsafe, non-pure, possibility: unsafeperformio, bypasses all restrictions. Introduction to functional programming, fol

42 A functional coding of the IO operators Implementation of Bind (>> =) and return (assuming that World cannot be copied) return :: a -> IO a return a = \ w -> (a, w) ( >> =) :: IO a -> (a -> IO b) -> IO bm >> = k = \ w -> case (mw) of (r, w) -> krw Here w is the new world. The monad laws apply, Introduction to Functional Programming, fol

43 Reduction and monads Beta reduction is not compatible with OK actions and the OK monad. In particular, Church-Rosser's theorem no longer applies to the combination of the (copying) beta rule with IO actions. Required: delayed evaluation with sharing. i.e. a call-by-need lambda calculus Introduction to functional programming, fol

44 Reduction and Monads Example by Simon Peyton Jones. do {c <- getchar; putchar c; putchar c} Translate using the definition of do and >> =: \ w -> case getchar w of (c, w1) -> case putchar c w1 of (_, w2) -> putchar c w2 Would be Church's theorem -Rosser apply, the compiler would be allowed to replace the same expressions: \ w -> case getchar w of (c, w1) -> case putchar c w1 of (_, w2) -> putchar (fst (getchar w )) w2 error: the world reference w was copied delayed evaluation with sharing prevents this effect Introduction to functional programming, fol

45 Examples for monads: pocket calculator A simple pocket calculator is programmed as an example for the combination of a state monad with the IO monad. Input / output via the console for the sake of simplicity. Calculator: the task of input: numbers from digits 0-9, operators +, -, * and /, decimal point, c and =. Result: arithmetic result after left brackets 123 * 456 = gives: Introduction to functional programming, fol

46 Pocket calculator: monadic State: saves operator and the two operands Implementation: saves function and operator. module Main where type CalcState = (Float -> Float, Float) type CalcTransformer a = CalcState -> (a, CalcState) Introduction to functional programming, fol

47 Pocket calculator: monadic We need the following CalcTransformer for the simulation clear :: CalcTransformer () clear (g, 0.0) = ((), (id, 0.0)) clear (g, z) = ((), (g, 0.0) ) digit :: Float -> CalcTransformer () digit d (g, z) = ((), (g, z * d)) oper :: (Float -> Float -> Float) -> CalcTransformer () oper o ( g, z) = ((), (o (gz), 0.0)) total :: CalcTransformer () total (g, z) = ((), (id, gz)) readresult :: CalcTransformer Float readresult (g, z) = (gz, (g, z)) Introduction to functional programming, fol

48 Pocket calculator: monadic startstate :: CalcState startstate = (id, 0.0) Introduction to functional programming, fol

49 Pocket calculator: monadic operation for the input operator: calcstep :: Char -> CalcTransformer () calcstep x isdigit x = digit (fromint (ord x - ord 0)) x == + = oper (+) x == - = oper (-) x == * = oper (*) x == / = oper (/) x == c = clear x == = = total Introduction to functional programming, fol

50 Pocket calculator: monadic Implementation: calc :: String -> CalcTransformer Float calc "" s = readresult s calc (x: xs) s = let (_, newstate) = calcstep xs in calc xs newstate main = fst (calc "123 * 456 = "startstate) Introduction to functional programming, fol

51 As state monad Before: type CalcState = (Float -> Float, Float) type CalcTransformer a = CalcState -> (a, CalcState) Generalization of CalcTransformer: newtype StateTransformer sa = ST (s -> (a, s)) s: Typ of the state; a: Type of output newtype: Specialized form of data One constructor / one argument / strict constructor No loss of efficiency, but more type safety Introduction to functional programming, fol

52 As a state monad newtype StateTransformer sa = ST (s -> (a, s)) Auxiliary function for unpacking: apply :: StateTransformer sa -> s -> (a, s) apply (ST action) = action Introduction to functional programming, fol

53 State Transformers as Monad StateTransformer s as Instance of Monad We define (>> =) and return: instance Monad (StateTransformer s) where return x = ST $ \ s -> (x, s) m >> = k = ST action where action s = apply (k res) s where (res, s) = apply ms res mssk Introduction to functional programming, fol

54 Instance of Monad (>>) automatically defined by the instance definition (>>) :: StateTransformer sa -> StateTransformer sb -> StateTransformer sbm >> k = m >> = \ _ -> k Introduction to functional programming, fol

55 Pocket calculator, monadic Calculator using StateTransformer sa: type CalcTransformer = StateTransformer CalcState clear :: CalcTransformer () clear = ST action where action (g, 0.0) = ((), (id, 0.0)) action (g, z) = ( (), (g, 0.0)) digit :: Float -> CalcTransformer () digit d = ST $ \ (g, z) -> ((), (g, z * d)) oper :: (Float -> Float -> Float) -> CalcTransformer () oper o = ST $ \ (g, z) -> ((), (o (gz), 0.0)) Introduction to functional programming, fol

56 Pocket calculator, monadic (2) total :: CalcTransformer () total = ST $ \ (g, z) -> ((), (id, gz)) readresult :: CalcTransformer Float readresult = ST $ \ (g, z) -> (gz, (g, z)) Introduction to functional programming, fol

57 pocket calculator, monadic calcstep remains; New is: calc :: String -> CalcTransformer Float calc "" = readresult calc (x: xs) = calcstep x >> calc xs with do notation: calc "" = readresult calc (x: xs) = do calcstep x calc xs or calc (x: xs) = do {calcstep x; calc xs} Introduction to functional programming, fol

58 Pocket calculator with IO World Program a Program :: IO a where IO a = World -> (a, world) Introduction to functional programming, fol

59 IO; Input examples for output functions: putchar :: Char -> IO () putstr :: String -> IO () putstrln :: String -> IO () print :: Show a => a -> IO () Introduction to the functional programming, fol

60 IO; Output examples for input functions: getchar :: IO Char getline :: IO String getcontents :: IO String interact :: (String -> String) -> IO () readio :: Read a => String -> IO a getline: : Read a => IO a Introduction to functional programming, fol

61 IO; Files Examples for and for functions on files writefile :: FilePath -> String -> IO () appendfile :: FilePath -> String -> IO () readfile :: FilePath -> IO String Introduction to functional programming, fol

62 Pocket calculator with single entry A variation of the calculator with IO is main = do k <- getline let (g, z) = apply (calc k) startstate print $ g Introduction to functional programming, fol

63 Combination of monads with IO state monads + other monads m: newtype STT sma = STT (s -> m (a, s)) apply :: STT sma -> s -> m (a, s) apply (STT f) = f instance Monad m => Monad (STT sm) where return x = STT $ \ s -> return (x, s) a >> = k = STT action where action s = do (x, s) <- apply as apply (kx) s Introduction to Functional Programming, fol

64 Combination of state monad with IO type CalcTransformer = STT CalcState IO IOMonad as a generalization: ioprint and iogetchar as external functions. class Monad m => IOMonad m where iogetchar :: m Char ioprint :: Show a => a -> m () IO should be an instance: instance IOMonad IO where iogetchar = getchar ioprint = print Introduction to functional programming, fol

65 Last step: STT s m should be an instance of IOMonad: class MonadTransformer t where promote :: Monad m => m a -> t m a instance MonadTransformer (STT s) where promote g = STT $ \ s -> do {x <- g; return (x, s)} instance IOMonad m => IOMonad (STT sm) where iogetchar = promote iogetchar ioprint x = promote $ ioprint x promote :: (MonadTransformer t, Monad m) => ma -> tma Introduction to functional programming , fol

66 Result of the combination A monad that combines status actions and OK actions. and type-safe is introduction to functional programming, fol

67 Calculator as Combined Monad clear :: Monad m => STT CalcState m () clear = STT action where action (g, 0.0) = return ((), (id, 0.0)) action (g, z) = return (( ), (g, 0.0)) total :: IOMonad m => STT CalcState m () total = STT $ \ (g, z) -> do {ioprint $ gz; return ((), (id, gz))} digit :: Monad m => Float -> STT CalcState m () digit d = STT $ \ (g, z) -> return ((), (g, z * d)) oper :: Monad m => (Float -> Float -> Float) -> STT CalcState m () oper o = STT $ \ (g, z) -> return ((), (o (gz), 0.0)) readresult :: Monad m => STT CalcState m Float readresult = STT $ \ (g, z) -> return (gz, (g, z)) Introduction to functional programming, fol

68 Pocket calculators as combined monads main = do apply calc startstate return () ---- (apply calc startstate) :: IO ((), (Float -> Float, Float)) calc :: CalcTransformer () calc = do {k <- iogetchar; if k == \ n then do {x <- readresult; ioprint x} else do {calcstep k; calc}} Introduction to functional programming, fol

69 Pocket calculator file: Calculator6.hs Slight extensions: Extended status, floating point numbers as input Introduction to functional programming, fol

70 Pocket calculator: Source module Main where import Char import IO main :: io () main = do hsetbuffering stdin NoBuffering hsetbuffering stdout NoBuffering - apply calc startstate return () type CalcState = ((String, Int), Double -> Double, Double) Introduction to functional programming, fol

71 Pocket calculator: Source startstate :: CalcState startstate = (("", 0), id, 0.0) calcstep :: Char -> CalcTransformer () calcstep x --- isdigit x = digit (fromint (ord x - ord 0)) isdigit x = digit (frominteger (tointeger (ord x - ord 0))) x == + = oper (+) x == - = oper (-) x == * = oper (*) x == / = oper (/) x == c = clear x == = = total x ==. = comma otherwise = nothing Introduction to functional programming, fol

72 Pocket calculator: Source newtype StateTransformer sa = ST (s -> (a, s)) newtype STT sma = STT (s -> m (a, s)) apply :: STT sma -> s -> m (a, s ) apply (STT f) x = fx instance Monad m => Monad (STT sm) where return x = STT $ \ s -> return (x, s) k1 >> = k2 = STT action where action s = do (x , s) <- apply k1 s apply (k2 x) s type CalcTransformer = STT CalcState IO class Monad m => IOMonad m where Introduction to functional programming, fol

73 Pocket calculator: Source iogetchar :: m Char ioprint :: Show a => a -> m () instance IOMonad IO where iogetchar = getchar ioprint = print class MonadTransformer t where promote :: Monad m => ma -> tma instance MonadTransformer ( STT s) where promote g = STT $ \ s -> do {x <- g; return (x, s)} instance IOMonad m => IOMonad (STT s m) where iogetchar = promote iogetchar ioprint x = promote $ ioprint x Introduction to functional programming, fol

74 Pocket calculator: Source clear :: Monad m => STT CalcState m () clear = STT action where action (str, g, 0.0) = return ((), (("c", 0), id, 0.0)) action (str, g, z) = return ((), (("c", 0), g, 0.0)) total :: IOMonad m => STT CalcState m () total = STT $ \ (_, g, z ) -> do {ioprint $ gz; return ((), (("t", 0), id, gz))} digit :: Monad m => Double -> STT CalcState m () digit d = STT $ \ ((str, dignum), g, z) -> if str == "t" then return ((), (("d", 0), g, d)) else if str == "." then return ((), ((".", dignum + 1), g, z + (0.1 ^ dignum) * d)) Introduction to functional programming, fol

75 Calculator: Source else return ((), (("d", 0), g, z * d)) comma :: Monad m => STT CalcState m () comma = STT $ \ ((str, _), g, z) -> if str == "d" str == "c" str == "" str == "o" then return ((), ((".", 1), g, z)) else if str == "t" then return ((), ((".", 1), g, 0.0)) else return ((), ((".", 30), g, z)) do nothing: : Monad m => STT CalcState m () do nothing = STT $ \ (sta, g, z) -> return ((), (sta, g, z)) oper :: Monad m => (Double -> Double - > Double) -> STT CalcState m () oper o = STT $ \ (_, g, z) -> return ((), (("o", 0), o (gz), 0.0)) readresult :: Monad m => STT CalcState m Double Introduction to functional programming, fol

76 Pocket calculator: Source readresult = STT $ \ (_, g, z) -> return (gz, (("r", 0), g, z)) calc :: CalcTransformer () calc = do {k <- iogetchar ; if k == \ n then do {x <- readresult; ioprint x} else do {calcstep k; calc}} Introduction to functional programming, fol