I. Streams (aka Lazy or Infinite Lists) and Lazy evaluation A. Goals ------------------------------------------ THE AMAZING UTILITY OF STREAMS (LAZY LISTS, INFINITE LISTS) Want to: ------------------------------------------ 1. Example ------------------------------------------ TWO EXAMPLES TO GENERALIZE > data Tree a = Lf > | Br a (Tree a) (Tree a) > square x = x * x > sum_odd_squares Lf = 0 > sum_odd_squares (Br v t1 t2) = > (if odd v > then square v > else 0) > + sum_odd_squares t1 > + sum_odd_squares t2 > fib :: Integer -> Integer > fib 0 = 0 > fib 1 = 1 > fib n = fib(n-2) + fib(n-1) > odd_fibs n = next 1 > where next k = > if k > n > then [] > else let f = (fib k) > in > if odd(f) > then f : next(1 + k) > else next (1 + k) ------------------------------------------ What do sum_odd_squares and odd_fibs do? how are these similar? what parts of each are enumeration? mapping? filtering?accumulation? 2. expressing enumeration, mapping, filtering, accumulation as functionals ------------------------------------------ THE PARTS ENUMERATION > -- of trees > preorder Lf = [] > preorder (Br v t1 t2) = > v : (preorder t1 ++ preorder t2) > -- of integers from 1 to k > to k = [1 .. k] ACCUMULATION, FILTERING, MAPPING ------------------------------------------ What have we seen that does accumulation like this? What have we seen that does filtering? What have we seen that does mapping? 3. putting the pieces together ------------------------------------------ PUTTING THE PIECES TOGETHER ------------------------------------------ 4. improving the syntax What do we want? ------------------------------------------ PIPELINE SYNTAX > sum_odd_squares3 tree = > preorder tree # filter odd > # map square > # foldr (+) 0 > odd_fibs3 n = > to n # map fib > # filter odd ------------------------------------------ B. Power of map, filter, accumulate paradigm 1. representing standard data as lazy lists How would you represent a polynomial as a lazy list? a vector? a matrix? C. Lazy evaluation, computing with infinite objects 1. Infinite lists (streams) a. computations with infinite streams ------------------------------------------ SIEVE TO FIND PRIMES > p `divides` x = (x `mod` p) == 0 > sieve :: Integral a => [a] -> [a] > sieve (p:ps) = > p : sieve > (filter (\x -> > not (p `divides` x)) > ps) > primes :: [Integer] > primes = sieve [2 ..] > first_50 = take 50 primes ------------------------------------------ How could you use this to write a test for being a prime? 2. implicit definition of streams ------------------------------------------ IMPLICITLY DEFINED STREAMS > ones :: [Integer] > ones = 1 : ones > zipWith :: (a->b->c) -> [a]->[b]->[c] > zipWith f (a:as) (b:bs) > = f a b : zipWith f as bs > zipWith _ _ _ = [] > add_lists :: [Integer] -> [Integer] > -> [Integer] > add_lists = zipWith (+) > integers :: [Integer] > integers = 1 : add_lists ones integers > nats :: [Integer] > nats = 0 : add_lists ones nats > fibs :: [Integer] > fibs = 0 : 1 > : (add_lists (tail fibs) > fibs) ------------------------------------------ II. Input/Output in functional languages A. the problem ------------------------------------------ THE PROBLEM WITH I/O WANT: referential transparency BUT: Input/Output seems to be a def: a *reactive system* is a system that Examples: ------------------------------------------ ------------------------------------------ NONDETERMINISM vs. REFERENTIAL TRANSPARENCY Suppose the expression choose e1 e2 returns either e1 or e2, at random. Does that make a language not referentially transparent? Operating system example. [ merge ] __> [ O. S. ] ___> [ split ] ^ ^ | | | |_______ [ prog 1 ] <_______| | | | | . | | . | | . | |____________ [ prog n ] <__________| ------------------------------------------ B. solutions 1. lazy synchronized streams ------------------------------------------ LAZY SYNCHRONIZED STREAMS Program has type [Response] -> [Request] Examples: data Request = Getq | Putq Char data Response = Getp Char | Putp echo :: [Response] -> [Request] echo p = Getq : (case p of (Getp c : p2) -> if (c == '\n') then [] else Putq c : (case p2 of (Putp : p3) -> echo p3 ------------------------------------------ 2. continuations ------------------------------------------ CONTINUATIONS Program has type Answer All parts of the program that do I/O take an Answer continuation representing the rest of the program Examples: putcK :: Char -> Answer -> Answer getcK :: (Char -> Answer) -> Answer putcK c k -- getcK k -- echo :: Answer -> Answer echo k = getcK (\c -> if (c == '\n') then k else putcK c ( echo k)) ------------------------------------------ 3. monads ------------------------------------------ MONADIC I/O Program has type IO () Examples putc :: Char -> IO () getc :: IO Char echo :: IO() echo = getc >>= \c -> if (c == '\n') then return () else putc c >> echo ------------------------------------------ What are the similarities to continuations? advantages? 4. other approaches III. Reasoning about functional programs A. Basic tools 1. equational reasoning ------------------------------------------ CALCULATIONAL STYLE Basic format for proving equations X = < hint why X = Y > Y = < hint why Y = Z > Z This really means that X = Y and Y = Z, from which X = Z follows. ------------------------------------------ ------------------------------------------ EXAMPLE CALCULATION Suppose we have > fst x y = x > snd x y = y > cons x y f = f x y > car z = z fst > cdr z = z snd Then car (cdr (cons 3 (cons 1 2))) = (cdr (cons 3 (cons 1 2))) fst = (cons 3 (cons 1 2) snd) fst = (snd 3 (cons 1 2)) fst = cons 1 2 fst = fst 1 2 = 1 ------------------------------------------ 2. structural induction a. for finite lists ------------------------------------------ STRUCTURAL INDUCTION FOR FINITE LISTS General form To prove: for all l::[a], P(l) holds. Technique: Exercise: append [] bs = bs append (a:as) bs = a:(append as bs) prove for all cs :: [a] (append cs []) = cs ------------------------------------------ can you do the proof? b. for trees ------------------------------------------ STRUCTURAL INDUCTION FOR TREES > data Tree a = Lf > | Br a (Tree a) (Tree a) What is needed to prove for all t::(Tree a), P(t)? ------------------------------------------ c. generalizing how to describe structural induction in general? B. partial and infinite lists, laziness (Thompson 17.9) 1. finite, partial lists ------------------------------------------ FINITE PARTIAL LISTS def: A finite-partial list of type [t] is either: [], -- the empty list _|_, -- a nonterminating computation -- of type [t], or (a:as), where a::t and as::[t] So to prove P(x) for all x::[t], ------------------------------------------ 2. infinite lists ------------------------------------------ INFINITE LISTS To prove P(xs) holds for all infinite lists of type [t]: for all natural numbers n, xs!!n Example: Each element of the list > plus4s = [1, 5 ..] is odd. Proof: by induction Basis: (n = 0) odd(plus4s!!0) = < def of plus4s > odd([1, 5 ..]!!0) = < def of !!> odd(1) = < def of odd> True Inductive step. Let n >= 0. Assume odd(plus4s!!n) odd(plus4s!!(n+1)) = < def of plus4s > odd([1, 5 ..]!!(n+1)) = < def of !! and Haskell notation> odd(plus4s!!n + 4) = < by the inductive hypothesis, plus4s!!n is odd, and by arithmetic add 4 to an odd number is odd> True ------------------------------------------ ------------------------------------------ PROVING EQUATIONS ABOUT INFINITE LISTS An equation between lists is valid if it is valid for all fp-lists. Reason: the set of fp-lists include all approximations of the infinite lists. Example: Prove, for all functions f, g and for all lists xs, (map f . map g) xs = map (f.g) xs ------------------------------------------ IV. Module systems in Haskell (Thompson 2.4 and 15) A. Motivation: programming in the large B. semantics How is a module like a record? C. modules in Haskell ------------------------------------------ EXAMPLE MODULE > module Shape (Shape(Rectangle, Ellipse), > Radius, Side, Vertex, > square, circle, area > ) where > > data Shape = Rectangle Side Side > | Ellipse Radiaus Radius > deriving Show > > type Radius = Float > type Side = Float > type Vertex = (Float, Float) > > square s = Rectangle s s > circle r = Ellipse r r > area :: Shape -> Float > area (Rectangle s1 s2) = s1 * s2 > area (Ellipse r1 r2) = pi * r1 * r2 > mars = Ellipse 1 1.093 ------------------------------------------ What does this export? What is hidden? D. namespace control 1. exports ------------------------------------------ HIDING EXPORTING TYPE CONSTRUCTORS Export list of module module Shape ( ) where ^^^ the export list Exporting types: Shape(..) -- exports Shape and all constructors Shape(Rectangle, Ellipse) -- exports Shape and named constructors Shape -- exports Shape, not the constructors ------------------------------------------ If you were designing Haskell, how would you allow exports of class definitions? Suppose we want a default if export list is omitted, what should it be? Is it better to name the exported names or the hidden ones? 2. imports ------------------------------------------ IMPORTS > import SOEGraphics makes all the names in the given module available ------------------------------------------ ------------------------------------------ DEALING WITH CONFLICTS > import Graphics > import CowboySimulation What if both define "draw"? ------------------------------------------ ------------------------------------------ RESOLVING CONFLICTS import Graphics(openWindow, runGraphics) import Graphics hiding (draw) import qualified Graphics ------------------------------------------ E. higher order V. Research Directions in Functional Programming Languages A. Adapting ideas to mainstream languages B. Type systems C. Integration with real world D. More expressive syntax E. Compilation and Optimization 1. On conventional machines a. when is it safe to implement updates destructively b. implicit caching and memoization 2. Novel architectures a. Data Flow Machines b. Graph reduction machines F. Parallelism 1. How to express? a. Implicit (as in data flow) b. Explicit (what constructs?) 2. How to map processes to processors? 3. mobile code, distribution G. Nondeterminism