Functional Programming

McMaster University - CAS 743

Winter 2006

Instructor

Dr. Wolfram Kahl, ITB-245 , ext: 27042, kahl@mcmaster.ca.

The course outline is available as PostScript and as PDF .

News

Final: Monday, April 10, 11:30-14:30, ITB-222
Presentation topics

Schedule

Midterm: March 6, 9:00-10:00 in ITB-222
Lecture: Mondays and Thursdays, 8:30-10:00 in ITB-222
Lectures begin on Monday, 9th January

Lecture Slides

(4-up on Letter paper --- printing on A4 paper will cut off a part.)

Haskell Introduction (January 12): ,
Haskell - Function Typing (January 16): ,
Haskell - Expression Evaluation, IO Introduction (January 19): , - WC.hs, Cat.hs, Usrs.hs
Haskell - Pattern matching, case, let, where, list functions (January 23): ,
Haskell - Prelude text processing functions, higher-order list functions (January 26): ,
Haskell - Data Types and Type Classes 1 (January 30):
- Simple type classes: Eq, Ord; type of members, default definitions, instances, class invariants (contracts), deriving, superclasses
- Simple data declarations
- Modules: unqualified and qualified import, export lists, abstract data types with non-standard class instances
Haskell - Data Types and Type Classes 2 (February 2):
- The numeric class hierarchy, the Show class, the cost of conversion between show :: a -> String and shows :: a -> ShowS
- Prelude types Either and Maybe, binary tree type Tree, primitive recursion (either, maybe, foldTree); recod syntax.
- Show instance for Tree: linear complexity with ShowS composition, quadratic complexity with String concatenation.
Haskell - Data Types and Type Classes 3 (February 6):
- Exercise: Define the dayatype HTree for Huffman trees, and the decoding function decode :: HTree a -> [Bool] -> [a]
  (Additional exercise: Define encode :: Eq a => [a] -> (HTree a, [Bool]) such that uncurry decode . encode = id and the generated code string is as short as possible.)
- The type class Data.Monoid.Monoid, monoid laws, monoid homomorphisms.
- Alternative representation of monoids using ``dictionary'' records.
- The ``constructor class'' Functor; kinds as ``types for the type language''.
- Definition of categories (as generalised monoids). The Haskell category: types as objects; functions as morphisms.
- Definition of functors as ``category homomorphisms''. Resulting laws for fmap.

Semantics 1 (February 9):

Exercise: Complete and verify:

instance Functor Maybe ...
instance Functor (Either c) ...
instance Functor ((,) c) ...
instance Functor ((->) c) ...
instance Functor Tree ...
instance Functor HTree ...

newtype K c a = K c
instance Functor (K c) ...

newtype Plus f g a = MkPlus (Either (f a) (g a))
instance Functor (Plus f g) ...

Additional Exercise:

data Functor1 f where
  fmap1 :: (a -> b) -> f a c -> f b c

instance Functor1 Either ...
instance Functor1 (,)  ...
instance Functor1 (->) ...

Another data example:
```
data T a = T a [T a]
```
Exercise: Functor instance!
Understanding recursive function definitions as using least fixed points
Definition of CPOs
Knaster-Tarski Fixed-point Theorem

Categories and Semantics 2 (February 13)
- Exercise
- Categories as generalisation of preorders
- Category-theoretic duality principle
- Universal constructions in Category Theory:
  - Initial objects, (direct) products (and pullbacks) as examples of limits
  - Terminal objects, direct sums (coproducts) (and pushouts) as examplies of colimits
  - Definition of diagram as graph homomorphism into the underlying graph of a category; definition of ``diagram commutes''.
- Constructing an example morphism chain using the functor
```
data L a = E | C Bool a

instance Functor L where ...  -- completed and verified in class
```
  starting from the initial object of the Haskell category
```
data Empty  -- contains undefined as only element
```
  and (skipped in class) the morphisms
```
injectL0 :: Empty -> L Empty
injectL0 _ = undefined         -- the unique morphism from the initial object

injectL1 :: L Empty -> L (L Empty)
injectL1 = fmap injectL0

injectL2 :: L (L Empty) -> L (L (L Empty))
injectL2 = fmap injectL1

...
```
  The colimit of this chain is the semantics of the recursive datatype [ Bool ] = L [ Bool ].
  The colimit contains all finite and inifinite lists - it has to contain infinite lists, too, to be a CPO.
- Aside: Constructor arguments in data declarations can be annotated as strict be prefixing the argument types with a ``!''. To keep the drawings of the chain CPOs smaller, I really used
```
data L' a = E | C !Bool a
```
  in class; there, C is strict in the first argument. Strictness annotations can be useful for efficiency considerations.
Monads 1 (February 16)
- Exercise
- class Monad
- class Read
- Phil Wadler: ``Replacing Failure with a List of Successes''
Monads 2 (February 27)
- Exercise
- class Monad including fail
- newtype, and review of sets-implemented-as-lists abstract export example
- class MonadPlus (and Haskell-1.3 class MonadZero)
Rewriting (March 9)
- Abstract rewriting: Normal form, confluence (strategy irrelevant for evaluation result), Church-Rosser (calculational reasoning can be replaced by evaluation), termination
- Term rewriting: Signature, term, rule, rule application, TRS
- Σ-Algebras, equational logic
- Untyped λ-calculus; mentioned that β and η rules can be presented as rules of a Combinatory Reduction System (CRS) [Klop-1980]
- Exercise: With Y = λ f . (λ x . f (x x)) (λ x . f (x x)), show Y f = f (Y f), i.e., show that Y is a fixpoint combinator.
λ-Calculi (March 13)
- Exercise
- Simply typed λ-calculus without type annotations at bound variables: typing á la Curry
  - Non-unique types
  - With type variables: principal types
- Simply typed λ-calculus with type annotations at bound variables: typing á la Church
  - Unique types
- Second-order λ-calculus
  - Example: (λ f : (∀ &alpha . &alpha → α) . pair (f Int 5) (f Char 'a')) (&Lambda &beta . &lambda x : &beta . x)
- Hindley-Milner typing
Some Haskell Patterns (March 16)
- Exercise
- Bredth-first search
- Memoisation

Assignments

Assignment 1 (handed out Jan. 16, due Jan. 26): , - StateMachine_skel.hs
For literate Haskell modules typeset in LaTeX, there are two options:
- ``Hack'': implement code environments using verbatim, for example by using code.sty with
```
 \usepackage{code}
 
```
- The proper solution: Use lhs2tex to process .lhs files into .tex files, which are then fed to LaTeX.
For mathematical notation, I like to use the Z notation, see the Z archive and the following two books which are available on-line:
- J. M. Spivey: The Z Notation: A Reference Manual
- Jim Woodcock and Jim Davies: Using Z: Specification, Refinement, and Proof
One way to get this in LaTeX is using oz.sty - documentation: , ; original site.
Assignment 2 (handed out Jan. 26, due Feb. 2): ,
Assignment 3 (handed out Feb. 6, due Feb. 16): , - Wikipedia SAT entry, SATLIB Benchmarks page (includes link to the format definition distributed in class)
Assignment 4 (handed out Feb. 16, due March 2): ,

Official Statements

Academic Dishonesty

``Academic dishonesty consists of misrepresentation by deception or by other fraudulent means and can result in serious consequences, e.g. the grade of zero on an assignment, loss of credit with a notation on the transcript (notation reads: ``Grade of F assigned for academic dishonesty''), and/or suspension or expulsion from the university.

It is your responsibility to understand what constitutes academic dishonesty. For information on the various kinds of academic dishonesty please refer to the Academic Integrity Policy, specifically Appendix 3, located at http://www.mcmaster.ca/senate/academic/ac_integrity.htm

The following illustrates only three forms of academic dishonesty:

Plagiarism, e.g. the submission of work that is not one's own or for which other credit has been obtained.
Improper collaboration in group work.
Copying or using unauthorized aids in tests and examinations.''

Discrimination

``The Faculty of Engineering is concerned with ensuring an environment that is free of all adverse discrimination. If there is a problem that cannot be resolved by discussion among the persons concerned, individuals are reminded that they should contact the Department Chair, the Sexual Harassment Office or the Human Rights Consultant, as soon as possible.''

(

-Viewer)

(