Table of Contents

Introduction

• Welcome
• How to get the compilers
• Overview

Basics

• Working with an interpreter
• Basic types: numbers, lists and tuples
• Nice to meet you, Mr. Typing
• Defining simple functions
  • Let and where clauses
• Higher-order functions
  • Anonymous functions
  • Partial application
• Totality

Lists

• Maps, folds and zips
• More origami: unfolds
• Comprehensions

Data type definition

• Basic definition in Haskell
• Pattern matching
• GADT-like definition
• Records in Haskell
• Attribute grammars: UUAGC

Modularity

• Haskell module system
• Agda module system

Parametric polymorphism

• Introduction
• Defining polymorphic types and functions
• Implicit arguments

Dependent types

• Defining a safer stack
• Dependent pairs and functions
• with clauses
  • View patterns
• Universes

Ad-hoc polymorphism

• Problem statement
• Solution 1: instance arguments
• Solution 2: type classes
  • Introduction
  • Multiparameter type classes: functional dependencies and type families
  • Automatic derivation in Haskell
  • Emulating dependent typing in Haskell

Laziness and codata

• Working with infinite structures
• Forcing evaluation
• Codata in Agda

I/O

• Side-effects
• Do notation
• Uniqueness typing

Functors

• Container types
• Important functors

Monads

• Trying to get state
  • The Reader and Writer monads
• Monads and do notation
• Important monads
• Monad transformers
• Monad comprehensions
• Indexed monads

Applicative

• Parsing
• Bracket notation

Logic and types

• Introduction to logic
• Curry-Howard isomorphism
• Theorem proving

More about types

• Kinds
• Universe polymorphism
• Cumulativity

Extending the syntax

• Template Haskell
• DSLs in Idris