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
(λ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
| λ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.
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.
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.
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 …
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
such intermediate data structures. Fusion involves inlining recursive functions which is really hard but GHC is already really good at inlining non- recursive functions.
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
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.
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
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.
LANGUAGE GADTs, KindSignatures # -} data Expr :: * -> * where ExprInt :: Int -> Expr Int ExprBool :: Bool -> Expr Bool ExprPlus :: Expr Int -> Expr Int -> Expr Int
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.
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
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
:: 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
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