Transcript Slides

Advanced Functional Programming
Advanced Functional
Programming
Tim Sheard
Oregon Graduate Institute of Science & Technology
Lecture 5: Monads
• Generic Unification
• Monads
Lecture 1
Tim Sheard
1
Advanced Functional Programming
Reading Assignment
Read the paper
“Generic Unification via Two-Level Types
and Parameterized Modules”
http://www.cse.ogi.edu/~sheard/courses/cse583W03/papers/index.html
Lecture 1
Tim Sheard
2
Advanced Functional Programming
An Example Use
• Unification of types is used for type inference.
data (Mutable ref m ) =>
Type ref m =
Tvar (ref (Maybe (Type ref m)))
| Tgen Int
| Tarrow (Type ref m) (Type ref m)
| Ttuple [Type ref m]
| Tcon String [Type ref m]
Lecture 1
Tim Sheard
3
Advanced Functional Programming
Unify
unify :: Mutable ref m =>
(Type ref m -> Type ref m -> m [String]) ->
Type ref m -> Type ref m -> m [String]
unify occursAction x y =
do { t1 <- prune x
; t2 <- prune y
; case (t1,t2) of
(Tvar r1,Tvar r2) ->
if same r1 r2
then return []
else do { put r1 (Just t2); return []}
(Tvar r1,_) ->
do { b <- occursIn r1 t2
; if b then occursAction t1 t2
else do { put r1 (Just t2)
; return [] }
}
Lecture 1
Tim Sheard
4
Advanced Functional Programming
Unify continued
unify occursAction x y =
do { t1 <- prune x
; t2 <- prune y
; case (t1,t2) of
. . .
(_,Tvar r2) -> unify occursAction t2 t1
(Tgen n,Tgen m) ->
if n==m then return []
else return ["generic error"]
(Tarrow a b,Tarrow x y) ->
do { e1 <- unify occursAction a x
; e2 <- unify occursAction b y
; return (e1 ++ e2)
}
(_,_) -> return ["shape match error"]
}
Lecture 1
Tim Sheard
5
Advanced Functional Programming
Generic Unify
• How can we generalize unify to work on any
type?
• What properties must that type have?
– a variable constructor like Tvar with a reference
• What functions best capture these
properties?
• Capture these functions in a class.
class Mutable ref m => Unify t ref m where
isVar:: t ref m -> Maybe (ref (Maybe (t ref m)))
occursCheck :: ref(Maybe (t ref m)) -> t ref m -> m Bool
occursAction :: t ref m -> t ref m -> m [String]
match :: t ref m -> t ref m -> Maybe [(t ref m, t ref m)]
Lecture 1
Tim Sheard
6
Advanced Functional Programming
Generic Prune
prunefun :: Unify t ref m => t ref m -> m(t ref m)
prunefun typ =
case isVar typ of
Just r -> do { m <- get r
; case m of
Just t -> do { newt <- prunefun t
; put r (Just newt)
; return newt
}
Nothing -> return typ}
Nothing -> return typ
Tvar(Just _ )
Tvar(Just _ )
Tvar(Just _ )
Tvar(Just _ )
Tvar(Just _ )
Tvar(Just _ )
Tuple[ X, Y]
Lecture 1
Tuple[ X, Y]
Tim Sheard
7
Advanced Functional Programming
Generic Unify
uni :: Unify t ref m => t ref m -> t ref m -> m[String]
uni x y =
do { t1 <- prunefun x
; t2 <- prunefun y
; case (isVar t1,isVar t2) of
(Just r1,Just r2) ->
if same r1 r2
then return []
else do { put r1 (Just t2); return []}
(Just r1,_) ->
do { b <- occursCheck r1 t2
; if b then occursAction t1 t2
else do { put r1 (Just t2); return [] }}
(_,Just r2) -> uni t2 t1
(Nothing,Nothing) -> case match t1 t2 of
Just pairs ->
do { errs <- sequence (map (uncurry uni) pairs)
; return (concat errs) }
Nothing -> return["Match error"]
}
Lecture 1
Tim Sheard
8
Advanced Functional Programming
An instance
instance Unify Type IORef IO where
isVar (Tvar r) = Just r
isVar _ = Nothing
occursCheck = occursIn
occursAction x y = return ["Occurs Check error"]
match x y =
let mlist xs ys = if length xs == length ys
then Just(zip xs ys)
else Nothing
in case (x,y) of
(Tgen x,Tgen y) ->
if x==y then Just [] else Nothing
(Tarrow x y,Tarrow a b) -> Just[(x,a),(y,b)]
(Ttuple xs,Ttuple ys) -> mlist xs ys
(Tcon c xs,Tcon d ys) ->
if c==d then mlist xs ys else Nothing
Lecture 1
Tim Sheard
9
Advanced Functional Programming
Monads
• Monads & Actions
• A Monad is an Abstract Data Type (ADT)
• A Monad encapsulates effects
– i.e. hides their implementation
• A Monad uses types to separates Actions
from pure computations
• A Monad controls the order of effects
Lecture 1
Tim Sheard
10
Advanced Functional Programming
Actions
It is sometimes useful to use actions
or side effects in a functional
program .
Update a piece of state (assignment)
do some IO
draw graphics on a display
return an exception rather than an answer
How do we do this?
We use a Monad
A Monad is a type constructor which has an
implied action.
For example: IO Int is an action which
performs some IO and then returns an Int
Lecture 1
Tim Sheard
11
Advanced Functional Programming
Example Monads
IO a
Perform an IO action (like read or write to a file or stdin
or stdout) and then return an item of type: a
GUI a
Perform a GUI action (like draw a pull-down menu) and
then return an item of type: a
State t a
Perform an action which could change the value of a
mutable variable (like an assignment) in a state thread
t, and then return an item of type: a
Parser a
Read some input to build an item of type: a, then chop
the items used to build it off the input device. Also a
parse may fail so must handle failure as well.
Lecture 1
Tim Sheard
12
Advanced Functional Programming
A monad is an ADT
A monad is an abstract datatype
It abstracts computations with effects.
It hides the details of its implementation.
It exports an abstract interface.
It specifies the order in which effects
occur.
It separates pure computations from
effectfull ones using the type system.
It can have multiple implementations.
Lecture 1
Tim Sheard
13
Advanced Functional Programming
Monads Encapsulate Effects
• A monad captures the meaning and use
of computations which have effects on
the real world.
• A monad describes or specifies the
effects in a “purely functional” way.
• A monad allows one to reason about
effects, using the simple rule of
substitution of equals for equals.
• A monad needn’t be implemented this
way
Lecture 1
Tim Sheard
14
Advanced Functional Programming
Sample Effects or Actions
• State
– Update a piece of the store (assignment) as well as return a
final value.
• Exceptional cases
– There may be an error instead of a final value
• Non-determinism
– There may be multiple possible final values
• Partial Computation
– There may be nothing: no final value, or anything else
• Communication
– There may be external influence on the computation
– Perform some Input or Output, as well as a final value.
– Draw graphics on a display
Lecture 1
Tim Sheard
15
Advanced Functional Programming
A Monad uses types to separate Actions
(with effects) from pure computations
• A Monad is a type constructor which has an
implied action.
• For example:
– a computation with type (IO Int )
– an action which might perform some IO and which
then returns an Int
• Computations with non-monadic types
cannot have any effects. They are pure
computations. The user (and the compiler)
can rely on this.
Lecture 1
Tim Sheard
16
Advanced Functional Programming
A monad orders effects
• A Monad specifies which effects come before others.
• The Do operator provides this control over the order in which
computations occur
do { var <- location x -- the first action
; write var (b+1)
-- the next action
}
Lecture 1
Tim Sheard
17
Advanced Functional Programming
A monad’s interface hides details
A monad has an interface that hides
the details of its implementation
Every monad has at least the two
operations
Do
Lets users control the order of actions
Return : a -> Action a
makes an empty action
Each monad has its own additional
operations.
Lecture 1
Tim Sheard
18
Advanced Functional Programming
Monads have Axioms
Order matters (and is maintained by Do)
Do { x <- Do { y <- b; c }
;d} =
Do { y <- b; x <- c; d }
Return introduces no effects
Do { x <- Return a; e } = e[a/x]
Do { x <- e; Return x } = e
Lecture 1
Tim Sheard
19
Advanced Functional Programming
An Example: IO actions
Each function performs an action of doing some IO
? :t getChar
-- get 1 char from stdin
getChar :: IO Char
? :t putChar
-- put Char to stdout
putChar :: Char -> IO()
? :t getLine
-- get a whole line from stdin
getLine :: IO String
? :t readFile
-- read a file into a String
readFile :: FilePath -> IO String
? :t writeFile -- write a String to a file
writeFile :: FilePath -> String -> IO ()
Lecture 1
Tim Sheard
20
Advanced Functional Programming
Modelling IO
• Suppose all that IO captured was the
reading and writing to standard input
and output.
• Then we could model IO a as follows
data Io a =
Io ( String -> (a,String,String))
instance Monad Io where
return x = Io(\ s -> (x,s,""))
(>>=) (Io f) g =
Io(\ s -> let (x,in1,out1) = f s
(Io h) = g x
(y,in2,out2) = h in1
in (y,in2,out1 ++ out2))
Lecture 1
Tim Sheard
21
Advanced Functional Programming
Io operations
getCharX :: Io Char
-- get 1 char from stdin
getCharX = Io(\ (c:cs) -> (c,cs,""))
putCharX :: Char -> Io() -- put Char to stdout
putCharX c = Io(\ s -> ((),s,[c]))
getLineX :: Io String -- get a whole line from stdin
getLineX = do { c <- getCharX
; if c == '\n'
then return ""
else do { cs <- getLineX
; return (c:cs)
} }
Lecture 1
Tim Sheard
22
Advanced Functional Programming
How to perform an IO action
• Some thing of type: IO Int is a potential action which
will return an Int, if it is ever performed.
• In order for the action to occur, it must be performed.
• Any thing with type : IO a typed at top level will be
performed.
• This is the only way that an action can be performed.
•
Stated another way
• An actionful program builds up a potential action, which is
finally performed when typed at top-level.
– laziness is crucial in the implementation here
• Big actionful programs can be built by combining smaller
actionful programs using do.
• No action is ever performed until typed at top level.
Lecture 1
Tim Sheard
23
Advanced Functional Programming
Example: Combining IO actions
getLineX :: Io [Char]
getLineX =
do { c <- getCharX
; if c == '\n'
then return ""
-----
else do { l <- getLine'
; return (c:l)
}
get a char
if its newline
no-op action which
returns empty string
-----
recursively
get a line
no-op action
to cons c to l
}
Potentially reads a string from stdin, if it is ever performed
Lecture 1
Tim Sheard
24
Advanced Functional Programming
Observations
• Actions are first class.
– They can be abstracted (param’s of functions)
– Stored in data structures. -- It is possible to have a list
of actions, etc.
• Actions can be composed.
– They can be built out of smaller actions by glueing
them together with do and return
– They are sequenced with do much like one uses semicolon in languages like Pascal and C.
• Actions can be performed (run).
– separation of construction from performance is key to
their versatility.
• Actions of type: Action () are like
statements in imperative languages.
– They are used only for their side effects.
Lecture 1
Tim Sheard
25
Advanced Functional Programming
Performing an action
• How do we perform an action?
• We need a function with type:
–Io a -> a
• If we have such a function then we break
the abstraction which hides how Io is
implemented.
• In Haskell, the real IO can only be
preformed at top level, when because
the main function must have type IO()
Lecture 1
Tim Sheard
26
Advanced Functional Programming
Modelling Io
Some Monads have models.
A model is a pure function that simulates
the actions of the monad in a pure way.
Our Io monad is a model of a subset of the
IO monad.
If a Monad has a model, we can often
produce a run function with type:
m a -> model_of_m a
The run function uses the actual effects, but
hides them in the model.
Lecture 1
Tim Sheard
27
Advanced Functional Programming
The Model of Io
run (IO f) = f
Suppose the only thing IO did was
getchar and putchar, then then run
might be implemented as:
run g s =
{ stdout := ""
; x= perform g using s as input
; return (x,stdin,stdout)
}
Lecture 1
Tim Sheard
28
Advanced Functional Programming
Sample Monads
data Id x = Id x
data Exception x = Ok x | Fail
data Env e x = Env (e -> x)
data Store s x = Store (s -> (x,s))
data Mult x = Mult [x]
data Output x = Output (x,String)
Lecture 1
Tim Sheard
29
Advanced Functional Programming
Homework
• Make Haskell Class definitions for each of the
monad types on the previous page.
• Think about what other operations are usefull
for each monad and define those.
• Recast the monad laws from the lecture
interms of return and (>>=) instead of return
and do.
• Choose 2 of the monads.
– The first should be either Exception or Output
– The second should be one of Env, Store, Mult
– prove the order or bind law for the two monads you
choose.
Lecture 1
Tim Sheard
30