Upgrade to Pro — share decks privately, control downloads, hide ads and more …

UU Haskell Summer School

Anler
August 25, 2016

UU Haskell Summer School

My experience in Utrecht University summer school of code in applied functional programming with Haskell

Anler

August 25, 2016
Tweet

More Decks by Anler

Other Decks in Programming

Transcript

  1. Cost of 1.850€ including: 2 weeks (4th - 15th July)

    with housing, breakfast, lunch and a couple of dinners with the teachers. Each day consisted of 2 conferences and 2 labs. Around 200 hours of content packed into around 70 hours of course which I’ll skim in ~1 hour
  2. λ-calculus Is a higher-order Term Rewriting System and simplistic programming

    language that is Turing-Complete and supports higher-order functions naturally.
  3. Church-Turing thesis Establishes an equivalence in computing capability between: λ

    Calculus (Alonzo Church) Turing Machine (Alan Turing)
  4. –Stephen Diehl “the design of the core calculus should drive

    development, not the fronted language”
  5. Core Language As small as possible functional language so that

    is easy to implement but still rich enough to allow modern languages to be translated into it without losing efficiency.
  6. Grammar e ::= x (variables)
 | e e (applications)
 |

    λx.e (abstractions) Application associates to the left. Only unary functions and unary application.
  7. Rewrite rules β reduction - Used to simplify expressions: 


    (λx.e)a→ β e[x →a] α conversion - Used to avoid name capturing:
 (λx. λy. x y) y → (λx. λz. x z) y η conversion - Used to allow point-free style of programming:
 λx. e x → η e
  8. Simply-Typed λ-calculus e ::= x (variables)
 | e e (applications)


    | λx:t.e (abstractions) t ::= τ (type variables)
 | τ → τ (function types) Function types nest to the right: τ → σ → ρ = τ → (σ → ρ). Programs always terminate so it’s not Turing complete. There are no polymorphic functions.
  9. fixed-point combinator Is a combinator with the property that for

    any f: 
 fix f = f (fix f) We say that (fix f) is a fixed point of f. Fixed point combinators can be used to express recursion in the lambda calculus (Y-combinator is the most famous one). Not typeable in the simply-typed lambda calculus without introducing the (fix :: (a → a) → a) primitive.
  10. polymorphism The typed lambda calculus based on the idea of

    type abstraction and application is called System F or polymorphic lambda calculus. Haskell’s core language isn’t really System F because in System F type inference is undecidable, so Haskell never infer a polymorphic type for a lambda argument without annotation (Monomorphism Restriction). System F has higher-rank polymorphism, Haskell allows it through RankNTypes language extension but they cannot be inferred.
  11. Most Haskell constructs can be desugared to λ-calculus Constructors of

    recursive data types using the Scott- Encoding Constructors of data types using the Church-Encoding General recursion using a fixed-point combinator Pattern matching using nested applications of case functions if-then-else can be expressed as a function …
  12. Generic Programming Is a form of abstraction that allows defining

    functions that can operate on large class of datatypes.
  13. Advantages Eliminate boilerplate code and focus in the interesting parts

    Programs that adapt automatically as they evolve
  14. Implementation Idea If we can describe regular datatypes in a

    different way, using a limited number of combinators, we can use this common structure to formally define algorithms for all regular datatypes. Steps to follow: Abstract from recursion Describe the “remaining” structure systematically
  15. Objective With this: data Bit = O | I class

    Encode a where put :: a -> [Bit] be able to do this: data Exp = Const Int | Plus Exp Exp deriving (Show,Encode)
  16. Pattern Functor on Lists data [a] = [] | a:[a]

    data ListF a r = NilF | ConsF a r Isomorphic type: type List’ a = Fix (ListF a)
  17. Pattern Functor on Trees data Tree a = Tip a

    | Bin (Tree a) a (Tree a) data TreeF a r = TipF a | BinF r a r Isomorphic type: type Tree’ a = Fix (TreeF a)
  18. Combinators for creating pattern functors systematically data (f:+:g) r =

    L (f r) | R (f r) data (f:*:g) r = f r:*:g r data I r = I r data K a r = K a data U r = U
  19. Pattern Functor on Lists data ListF a r = NilF

    | ConsF a r becomes: type ListS a r = U:+:(K a:*:I) r
  20. Pattern Functor on Trees data TreeF a r = TipF

    a | BinF r a r becomes: type TreeS a r = K a:+:(I:*:K a:*:I) r
  21. Problem sum $ map (+1) $ map (*2) [1 ..10]

    Allocates intermediate lists that consume memory even when they not appear in the result.
  22. Fusion With fusion we want the compiler to automatically eliminate

    such intermediate data structures. Fusion involves inlining recursive functions which is really hard but GHC is already really good at inlining non- recursive functions.
  23. One technique Define our functions in terms of foldr/build (not

    all of them can) and exploit the fact that GHC’s simplifier will perform the following transformation: foldr c n (build g) -> g c n
  24. The main idea behind this trick is that build is

    the inverse of foldr, build builds a list with (:) and [], on the other hand foldr op n on the other hand replaces all (:) by op and [] by n. Knowing that we can tell why foldr op n (build g) is doing some redundant work that can be removed directly with 
 g op n
  25. Other technique Two important functions foldl and zip are not

    folds, in this case a technique using the dual of folds: unfolds, is used because they (as folds) can also fuse… but I still don’t understand it
  26. Monads Monads encode a common pattern that arises when working

    with multiple data types. The interface of such pattern is: sequencing embedding
  27. Monads are not About sequencing Haskell already has a primitive

    that allows sequencing without the need of monads: let Impure or about side-effects About making Haskell imperative
  28. Maybe Type sequencing: 
 stepResult >>= nextComp = case stepResult

    of
 Nothing -> Nothing
 Just result -> nextComp result embedding:
 return result = Just result
 maybe1 >>= \r1 -> maybe2 >>= \r2 -> …
  29. Either Type sequencing: 
 stepResult >>= nextComp = case stepResult

    of
 Left err -> Left err
 Right result -> nextComp result embedding:
 return result = Right result
 either1 >>= \r1 -> either2 >>= \r2 -> …
  30. State Type type State s a = s -> (a,

    s) sequencing: 
 stepResult >>= nextComp = \s -> 
 let (s’, result) = stepResult s
 in (nextComp result) s’ embedding:
 return result = \s -> (result, s)
 state1 >>= \r1 -> state2 >>= \r2 -> …
  31. Maybe: >>= sequences operations that may give no results and

    shortcuts evaluation in those cases, return embeds a function that never fails. Either: >>= sequences operations that may result in an error and shortcuts evaluation in those cases, return embeds a function that never gives an error. State: >>= sequences operations that may modify a piece of state and threads that state through the operations, return embeds a function that never modifies the state.
  32. IO The IO type is just another types that uses

    sequencing and embedding so it’s abstracted as a Monad, although it is kind of a special type: is a primitive type, >>= and return are primitive functions named bindIO and returnIO there is no (politically correct) function IO a -> a values of IO a denote side-effecting computations that can be executed by the runtime system Notice: The specialty of IO has really not much to do with being a Monad
  33. IO in Haskell More and more features have been integrated

    into IO, for instance: classic file and terminal IO: putStr, hPutStr references: newIORef, readIORef, writeIORef access to the system: getArgs, getClockTime exceptions: throwIO, try, catch concurrency: forkIO
  34. Transformers A way of stacking different Monads on top of

    each other and use functionality of the underlying monads in the top monad. For (nearly) any monad, we can define a corresponding monad transformer.
  35. Transformers 
 transformers package Lift a computation from the argument

    monad to the constructed monad. class MonadTrans t where lift :: Monad m => m a -> t m a
  36. MaybeT Type newtype MaybeT m a = MaybeT (m (Maybe

    a)) import Control.Monad.Trans.Class
 import Control.Monad.Trans.Maybe checkPassword :: MaybeT IO Bool
 checkPassword = do
 password <- lift getLine
 if password == "secret"
 then return True
 else fail "invalid password"
  37. ExceptT Type newtype ExceptT e m a = ExceptT (m

    (Either e a)) import Control.Monad.Trans.Class
 import Control.Monad.Trans.Except checkPassword :: ExceptT String IO Bool
 checkPassword = do
 password <- lift getLine
 if password == "secret"
 then return True
 else throwE "invalid password"
  38. StateT Type newtype StateT s m a = StateT (s

    -> m (a, s)) import Control.Monad.Trans.Class
 import Control.Monad.Trans.State
 import qualified Data.Map as Map getContact :: StateT (Map.Map String String) IO ()
 getContact = do
 input <- lift getLine
 let [name, phone] = words input
 modify (Map.insert name phone)
 return () …
 execStateT getContact Map.empty
  39. Transformers 
 mtl package This library extends the transformers library

    with multi- parameter type classes with functional dependencies such as MonadState and MonadReader. Transformers is Haskell 98 and thus more portable, and doesn't tie you to functional dependencies (GHC specific). But because it lacks the monad classes, you'll have to lift operations to the composite monad yourself.
  40. Motivation data Expr = ExprInt Int
 | ExprBool Bool
 |

    ExprPlus Expr Expr Our type allows to mix Int and Bool when adding.
  41. Rewrite example using GADTs… {-# LANGUAGE GADTs, KindSignatures # -}

    data Expr :: * where
 ExprInt :: Int -> Expr
 ExprBool :: Bool -> Expr
 ExprPlus :: Expr -> Expr -> Expr
  42. … and we encode the types of the terms {-#

    LANGUAGE GADTs, KindSignatures # -} data Expr :: * -> * where
 ExprInt :: Int -> Expr Int
 ExprBool :: Bool -> Expr Bool
 ExprPlus :: Expr Int -> Expr Int -> Expr Int
  43. What’s the result? take' :: Int -> [a] -> [a]


    take' 0 _ = []
 take' n l = head l:take' (n - 1) (tail l) let v = error “kaboom”
 v -> ?
 length (take 3 v) -> ?
  44. What’s the result? take' :: Int -> [a] -> [a]


    take' 0 _ = []
 take' n l = head l:take' (n - 1) (tail l) let v = error “kaboom”
 v -> ***Exception
 length (take 3 v) -> 3
  45. What drives evaluation Every expression is evaluated when needed. It

    is pattern- matching (and evaluation of conditions) what drives evaluation in Haskell. With garbage collection we do not have to worry when the life of a value ends. With lazy evaluation we do not have to worry when the life of a value starts.
  46. Where lazy evaluation matters Describing process-like structures Recurrent relations Combining

    function, e.g. by building an infinite structure and inspecting only a finite part of it Composing functions, e.g. map (+1) . map (*2) $ …
  47. Non-termination In lambda calculus we can encode recursion and therefore

    nonterminating terms A nonterminating value is usually written ⊥ In Haskell ⊥ is available as undefined :: a In the presence of ⊥, a function f is called strict if 
 f ⊥ = ⊥ We can force evaluation with the primitive function
 seq, ($!) :: a -> b -> b
  48. Concurrency Language constructs or library functions that allow you to

    structure a program into multiple threads of control that are executed concurrently. Mainly a structuring mechanism No parallel hardware required to make use of it Useful in many settings that have nothing directly to do with parallelism Non deterministic
  49. Threads Control.Concurrent forkIO :: IO () -> IO ThreadId threadDelay

    :: Int -> IO () yield :: IO () myThreadId :: IO ThreadId killThread :: ThreadId -> IO () throwTo :: Exception e => ThreadId -> e -> IO () Very lightweight. They are created and scheduled by the GHC runtime. Use -thread to use OS threads behind the scenes Use STM for communicating between threads
  50. Parallelism The concept of running programs on multiple CPUs in

    the hope of getting a speedup. It really is about speed, not structuring Deterministic
  51. Running in parallel Control.Parallel We mark parts of the program

    that we consider suitable for parallel evaluation We let the runtime system decide about all the details par :: a -> b -> b Indicates that it may be beneficial to evaluate the first argument in parallel with the second. Eval monad makes easier to define parallel strategies. It is a strict identity monad