Learn · Functional Programming with OCaml
Lecture 8 of 73Week 2
Static vs dynamic semantics, and type inference
Prof. K C Sivaramakrishnan · IIT Madras
Credits and licence
- From
- Functional Programming with OCaml, IIT Madras (at NPTEL)
- Licence
- CC BY-NC-SA, as NPTEL states it. Non-commercial use only.
- Attribution
- NPTEL states: "Distributed under Creative Commons Attribution-ShareAlike / CC BY - NC - SA", beside a BY-NC-SA badge.
- Who can watch
- Tweens profiles and older. How courses are placed
All the lectures
- Course introduction: what you'll learn, how it's run
- Why functional programming?
- A tour of OCaml: values, types, and the toplevel
- Your first OCaml program: hello, world (and beyond)
- Tutorial: temperature conversions and small expressions
- Literals: integers, floats, booleans, strings
- `let` bindings and shadowing
- Static vs dynamic semantics, and type inference
- Operators, precedence, and common pitfalls
- `if`/`then`/`else` as an expression
- Tutorial: small expressions, end to end
- Functions as values, and anonymous functions
- Recursion
- Currying and partial application
- Tail recursion and accumulators
- Local functions and mutual recursion
- Tutorial: Fibonacci, GCD, power, digits
- Tuples
- Records
- Variants (sum types)
- Recursive types: lists, trees, expressions
- Tutorial: a tiny AST for OCaml
- Tutorial: a tiny file system
- Basic patterns: literals, variables, wildcards
- Pattern matching on lists and trees
- Nested patterns and or-patterns
- Guards: when-clauses on patterns
- Exhaustiveness checking
- Tutorial: an interpreter for the OCaml AST
- Functions as values, revisited
- map: transform every element
- filter: keep what passes the predicate
- fold: reduce a list to a single value
- Function composition and pipelines
- Tutorial: fold across data structures
- Mutable references
- Mutable records and arrays
- Exceptions
- Streams and Laziness
- Memoization
- Module basics
- Module signatures
- Functors
- Tutorial: A Queue functor
- The option monad and `let*`
- Monad laws, the list monad, and the result monad
- The state monad and parameterised state
- GADTs: variants with type-level information
- GADTs: use cases beyond toy interpreters
- GADTs: hlists and witnesses
- Tutorial: a tiny well-typed evaluator
- Why test a type-safe program?
- Specifications and invariants
- Designing test cases: black-box and glass-box
- Unit testing
- Property-based testing with QCheck
- Model-based testing of stateful data structures
- Tutorial: testing the expr evaluator with OUnit2 and QCheck
- What memory safety is, and why it is a security story
- Memory safety by construction
- Data races are undefined behaviour
- Where OCaml itself has UB
- Tutorial: walking Heartbleed end to end
- Locality: safe stack allocation
- Uniquenss: the only reference
- Linearity: use at most once
- Contention: Synchronisation at compile time
- Portability: data race freedom across domains
- Tutorial: a resource-management API
- Why do we need an OS?
- MirageOS Unikernel Background
- MirageOS Basics
- Suresh the Stationmaster: a worked unikernel example