McMaster University — Fall 2009
Lecture Notes
16 September:
- Simple types in Haskell, including type variables for polymorphic types.
- Semantic versus syntactic associativity;
function type construction associates to the right,
while function application associates to the left.
- Typing rules for simple terms, in particular function application.
- Function combinators:
id, (.),
const, flip, curry, uncurry
Used as examples for type inference.
- Infix operators are not expressions; operator sections.
21 September:
- CPOs — Wikipedia
- strict and non-strict functions
undefined and error
Maybe- Pattern matching
- Data type definitions using “
data”
Either- Recommended exercises:
23 September: Name Binding Mechanisms
- Name bindings that can occur at module top-level: Function bindings and pattern bindings
- Higher-order functions:
map, filter
- λ-abstraction
- Typing of λ-abstraction in Haskell
- Simply typed λ-calculus
- Untyped
λ-calculus: variable binding, free variables, substitution
28 September: Name Binding Mechanisms (continued)
- Untyped
λ-calculus continued: α-conversion, α-equivalence;
β-reduction
- Reduction strategies: leftmost-innermost (call-by-value),
leftmost-outermost (call-by-name)
- Short interlude:
- “Forcing call-by-value'' with
seq
foldr versus foldl; List.foldl'
30 September: Name Binding Mechanisms (continued)
- Untyped
λ-calculus continued: η-reduction
- η-expansion in typed λ-calculus and Haskell
- Recursion, fixpoint combinator Y,
fixpoint approximation in CPOs, using
factorial example
- λ-abstraction over patterns in Haskell
- Name bindings in
case expressions
and in left-hand sides.
- as-patterns (“
@”),
irrefutable patterns (“~”)
2 October: Haskell Type Classes
- Prelude type classes
- Declaring instances for type classes
- Instances and abstract data types
5 October:
- Polymorphic types
- Polymorphically typed λ-calculus
(second-order λ-calculus, λ2,
System F)
let bindings, let-polymorphism
(Hindley-Milner typing)
- Haskell Type Classes
7 October:
- Mark Jones'
Tree class;
depth-first and breadth-first tree traversals
- Exercise
9 October: Monads
14 October: Monads (ctd.)
class Monad:
- Kleisli composition
(>=>)
- Monad laws
- Missing
Functor superclass; liftM
Aside: Don't use OverlappingInstances lightheartedly!
do Notation
fail
- Examples for use of
Maybe and [] as monads
16 October: Monads (ctd.)
class MonadPlus
- State monads:
19 October: Categories
- Categories as generalisation of preorders
- Universal constructions in category theory
as generalisation of ordering concepts::
- Initial objects correspond to least elements
- (direct) products correspond to greatest lower bounds
- Functors as generalisation of order homomorphisms
21 October
26 October
- Stream programming:
fibs = 1 : 1 : zipWith (=) fibs (tail fibs)
can also be used for the next-generation function in cellular automata.
- Other discussion related to Assignment 2
- Parser combinators (ctd.)
- State monad transformer:
Control.Monad.State.StateT
28 October
11 November
16 November
18 November
- Typing of λ-abstractions between types and terms;
short mention of the λ-cube
- Dependently-typed programming in Agda
23 November
25 November
25 November
- RELax project presentation
- Agda (ctd.)
2 December
(
-Viewer)
(
-Viewer)