Work@Microsoft    Study@UW.edu    Live@Seattle

Programming Languages Course Introduction (CSE P505) at University of Washington

Rate this post

Course Overview

This course will offer an introduction to programming language semantics through implementation and formal models. It will emphasize functional programming and cover the key features of modern functional languages (including type systems and memory management), along with some ideas from object-oriented and other programming styles.

Course Staff

Instructor: Greg Cooper (greg@cs.brown.edu)
Greg received a Ph.D. in computer science from Brown University in 2008, advised by Shriram Krishnamurthi. In real life he works as a software engineer at Google.

Homework

Homework 1

This post contains the problem statements for the first homework, which is due on Monday, January 19, 2015 at 11:59pm. Please attempt as much as you can before next Thursday’s lecture.

Homework #1

In this assignment, you’ll build parsing utilities that you’ll be able to reuse throughout the course and develop an evaluator for a simple language. The first step is to install Haskell and set up your development environment if you haven’t done so already. See the main course page for relevant links about doing so.

To simplify parsing, we’ll use S-expressions as the surface syntax for our language. For our purposes, S-expressions have three variants:

  • numbers (integers)
  • identifiers (which may contain letters, digits, and symbols, but cannot start with a digit or a single dash followed by a digit)
  • lists of S-expressions

Examples (in concrete syntax):

  • Numbers: 123, -75
  • Identifiers: +, -, *, let, a-multi-word-id
  • Lists: (* 2 (+ -3 4)), (if (> 1 2) -5 10)

Note how they differ from Haskell lists:

  • Syntactically: the separator can be any whitespace, and parentheses mark the start and end of a list. (Actually, our implementation will allow other types of braces, since that’s often useful.)
  • Structurally: they contain a mixture of numbers, identifiers, and lists (which can be nested).

We’ll decompose the problem of building S-expressions from strings into two steps: tokenizing and parsing. The first step turns a string into a list of tokens. The second turns the list of tokens into an S-expression (a tree), or returns an error if the input does not represent a valid S-expression. We’ll also support comments (any characters starting with a semicolon and going until the end of a line) by stripping them out, along with all whitespace, in the tokenizing step.

Download the files Token.hsSExp.hs, and Interp.hs and put them in the directory where you’ll be working.The file Token.hs defines a Token datatype and a parseToken function. The result of parseToken is a Maybe value, where Maybe is defined (in the Standard Prelude) as:

data Maybe a = Nothing | Just a deriving …

If passed a string containing only whitespace and/or comments, parseToken returns Nothing. Otherwise, it returns Just a pair of the token and the input characters that were not consumed in parsing it. You should not need to modify anything in Token.hs, but you should make sure you understand the Token type and parseToken function.

SExp.hs imports the Token module and contains partial definitions for an S-expression parser.

Problem 1. Fill in the implementation of the tokenize function, which, given a string, parses it into a list of tokens. (You can, of course, call the parseToken function to help do this.)


The next step is to try to convert a list of tokens into an S-expression. We’ve defined a type, SExp, and given you a start on parseSExp.

Given a list of tokens, the parsing algorithm is defined as follows:

  • A number token becomes a number S-expression.
  • An identifier token becomes an identifier S-expression.
  • An open brace begins a list S-expression. A matching close brace terminates the list. In between there may be an arbitrary number of S-expressions of any variant.

Not every list of tokens corresponds to a valid S-expression. We have defined a type called Resultto distinguish success from failure without having to abort evaluation via error. This lets you test your code’s behavior on invalid inputs much more easily. If the list parses, your code should return

  Ok (sexp, remaining tokens)

Otherwise, it should return

  Err string-describing-error

We’ve provided a few examples of strings whose tokenized representations should be parseable (or not) and (if so) what they should parse to. There are also functions that, if called on one of the appropriate examples, will evaluate to a pair of (String, Bool), where the string is the test case description and the boolean indicates whether the outcome was as expected. (The built-in mapfunction applies a function to every element of a list; it may come in handy here.)

Problem 2. Fill in the implementation of parseSExp.


Interp.hs defines an abstract syntax tree for a little language with numbers, booleans, a few built-in binary operations, and a conditional form. The final parsing step is to transform an S-expression into an Expr tree representing an expression in this language. (The comments above the Expr data definition show what the concrete S-expression syntax for each variant should look like.)

Problem 3. Fill in the implementation of parseExpr. We’ve provided one example to test your implementation on, and a function to help you do so, but you’ll probably want to add some cases of your own.


Now that we have a way of building abstract syntax trees, we can turn our attention to semantics and implement our first evaluator.

Problem 4. Fill in the implementation of interp.The binary operators should have their usual meaning. Note that all of them expect numeric arguments; however, + and * return numbers, while = and < return booleans.

For if expressions: if the first sub-expression (the condition) evaluates to true, then the result is determined by evaluating the second sub-expression (the consequent). If the first thing evaluates to false, the result is what you get from evaluating the third sub-expression (the alternative).

If you want to try out larger examples (for example, spanning multiple lines), you can save them in a separate text file. (If using Emacs, I’d recommend using a .scm suffix to get S-expression indentation automatically.) Then, to read a string in from a file you can type the following incantation at the REPL prompt:

λ> text <- readFile “<path to file>

Now text will be bound to a string that you can tokenize, etc. If you edit the file, you can just evaluate this expression again, and that will bind text to the new file contents.

Handin MechanicsSubmit your modified versions of SExp.hs and Interp.hs under “Homework 1” in the dropbox linked from the course homepage.

Homework 2
This homework is due on Friday, February 6 Monday, February 9 at 7pm 11pm.

In this homework, we’ll build an interpreter for a language with functions, then add mutable state to it. We’ll support a fairly rich surface syntax and use desugaring to translate down to a small core abstract syntax, with an initial environment that defines a collection of built-in constants and primitive operations.

We’ve pulled the definition of Result into its own module and implemented the Monad type class for it, so feel free to write your interpreters in monadic style and to use do notation if you’re comfortable with that.

This time, we’re also supplying a reference implementation of S-expression parsing.

The surface syntax we’ll support for this assignment is as follows:

<e> ::= <number>

      | (if <e> <e> <e>)

      | x

      | (fun (x …) <e>)

      | (<e> <e> …)

      | (with* ([x <e>] …) <e>)

We’ll desugar this to the following core syntax:

<c> ::= <number>

      | (if <c> <c> <c>)

      | x

      | (fun (x) <c>)

      | (<c> <c>)

Desugaring of functions and applications uses currying to transform a multi-argument function (or application) into a single-argument one. For example:

(fun (g x)

  (g (g x)))

becomes:

(fun (g)

  (fun (x)

    (g (g x))))

and:

(f (+ 2 3) (if (< x y) x y))

becomes:

((f ((+ 2) 3)) (if ((< x) y) x y))

Our examples show desugaring in terms of the corresponding concrete syntax, but it is actually a function from elements of the Expr abstract syntax to elements of the CExpr (“core” expression) abstract syntax.

A with* expression is desugared into a function application:

(with* ([x (+ 1 2)]

        [y (* x x)]
        [x (+ y 3)])

  (+ x y))

is equivalent to:

((fun (x)

   (with* ([y (* x x)]
           [x (+ y 3)])

     (+ x y)))

 (+ 1 2))

Continuing this unfolding, we get:

((fun (x)

   ((fun (y)

      ((fun (x)

         (+ x y))

       (+ y 3)))

    (* x x)))

 (+ 1 2))

The whole expression evaluates to 15 21.

In this example, we’ve left the binary operator calls in sugared form for the sake of simplicity. They would of course also need to be desugared.

Note that it should be an error to reuse a variable name in a multi-argument function; however (as in the example above), it is perfectly legal to rebind the same variable name in a with* expression. Also, a with* expression can have zero or more variable bindings (the zero case being equivalent to the body expression), but a function must have at least one argument, and hence an application must have at least two subexpressions. Your implementation of parseExpr may ignore such concerns and accept functions and applications with too few arguments, but desugar will need to raise an error, since there is no way to represent the corresponding expressions in the core syntax.


Problem 1. Download SExp.hs, Result.hs, and Expr.hs. (The file Token.hs is the same as in Homework 1.) Implement parseExpr, desugar, and checkIds in Expr.hs. You can probably reuse some parts of your parseExpr from Homework 1.

The function checkIds should check that all variable references in a core expression are bound and that no reserved identifier is ever rebound as a function variable. The function should return Ok ()if these conditions hold and Err <reason> if not.

For example, we’d probably call checkIds with the names from the initial environment (bound) and the same names plus “if” and “fun” (reserved).


Problem 2. Download InterpFun.hs. Populate initialEnv with bindings for “true”, “false”, “+”, “*”, “=”, and “<“. The semantics of these operators should be the same as in Homework 1, except that they’re curried now. We’ve provided a function called wrapBinaryArithOp to help define these primitives. Note that it won’t raise an error until both arguments have been supplied, even if the first is of the wrong type.

Next, implement interp for this language. The language should be eager, and the semantics of ifshould be as in Homework 1.


Problem 3. Download InterpStore.hs. Make sure you understand the STR type. If you intend to take advantage of monads, supply appropriate implementations of the return and bind (>>=) operations for the STR monad instance. Regardless of whether you intend to use monadic style/operators, implement the functions alloc (which allocates a value to a fresh location), fetch (which returns the value at the given location), and update (which update the value at the given location).

Use these store functions to define primitives (PrimV instances) for functions called box (which creates a mutable cell), unbox (which returns the contents of a box), and set-box! (which updates the contents of a box). Note that set-box! takes two arguments: first the box, then the new value. These primitives should work on BoxV values, which have been added to the Val datatype.

Populate initialEnv with bindings for “box”, “unbox”, “set-box!”, as well as all of the bindings from Problem 2. You may want to reuse/modify wrapBinaryArithOp to help with this.

An example expression using boxes:

(with* ([b (box 0)] [inc! (fun (n) (set-box! b (+ n (unbox b))))] [_ (inc! 5)] [_ (inc! 3)])
(unbox b))

(should evaluate to 8)

Implement interp for the language with boxes. (How much does the code differ from what you wrote in Problem 2?)

Handin mechanics. Submit your modified Expr.hs, InterpFun.hs, and InterpStore.hs in the dropbox for Homework 2. Don’t forget to test your code. :)

Homework 3
This homework is due Friday, February 27 at 8pm Sunday, March 1 at 11pm. Please read through it at your earliest convenience, make sure that you understand it, and try to make progress before class on the 19th so you can ask questions then.

This will give you practice using continuations (represented as data structures) to implement non-local control features. Start by downloading new versions of Token.hs, Result.hs, SExp.hs, and Expr.hs, along with a new file, InterpCont.hs.

The language grammar is identical to that of Homework 2, and we’ve provided implementations of parseExpr, desugar, and checkIds. So that we’ll have a richer language to play with (and in preparation for studying type-checking), we’ll add a few new types of data: strings, lists, and pairs. We’ve already added the new variants of Val for you:

StringV String — a string constant
EmptyV — an empty list
ConsV Val Val — a non-empty list (first arg can be of any type, second must be a list)
PairV Val Val — a pair: both args may be of any type

Problem 1.

Complete the definition of the Cont datatype and the implementations of the functions apply, callK, and interp; apply should work for either a user-defined function (FunV) or a built-in (PrimV). (We’ll refer to such values as applicable later.) It should raise an error when its first argument is any other type of value.

Problem 2.

Complete the implementations of the following data constructors, recognizers, and selectors:

empty? (defined as emptyP from Haskell) recognizes the empty list (which is written as empty in our language). If given an EmptyV, it should return true; otherwise false.

cons constructs a non-empty linked list (a ConsV), much like Haskell’s (:) operator does. It takes two arguments: the first may be any value, but the second must be a list (either a ConsV or an EmptyV), or else it should raise an error (by calling handleError with a StringV describing the error).

cons? (defined as consP from Haskell) recognizes non-empty lists. If given a ConsV, it should return true; otherwise false (even if the argument is not a list).

first selects the first element of a non-empty list (a ConsV). If given anything else, it should raise an error.

rest selects the rest of a non-empty list (a ConsV). If given anything else, it should raise an error.

pair constructs a pair. It takes two arguments, each of which may be of any type of value (and the two may be of different types).

fst (defined as pairFst to avoid conflicting with the Prelude) selects the first element of a pair.

snd (defined as pairSnd to avoid conflicting with the Prelude) selects the second element of a pair.

Problem 3.

Implement the following non-local control operators:

a. raise raises an error by calling handleError with the current continuation and its argument.

b. call-with-handler takes two arguments (I’ll call them thunk and handler–both of them must be applicable) and uses handler to define an error-handling context for the execution of thunk. The semantics are very similar to exception-handling blocks in languages like Java, JavaScript, and Python, except we’re implementing this functionality with a primitive operator instead of new syntax.

call-with-handler should apply thunk to an arbitrary value (e.g., the empty list). If no errors occur, then the result of the whole expression is the value returned by thunk. However, if an error is raised, handler should be called with the error in the call-with-handler expression’s continuation. For example:

(with* ([f (fun (x) (+ x (raise “bad problem!”)))])

  (call-with-handler
; thunk:

    (fun (_) (f 3))
; handler:
(fun (err) (pair “caught” err))))

should evaluate to: (“caught”, “bad problem!”).

However:

(+ (with* ([f (call-with-handler
; thunk (just returns a function)

               (fun (_) (fun (x) (+ x (raise “really bad problem!”))))
; handler (not called)

               (fun (err) (pair “caught” err)))])
; we’ve left the context of the call-with-handler, so no handler here …

          (f 3)))
should evaluate to an error.

Error handlers may be nested, in which case the handler in the inner context takes precedence. A handler may decide to re-raise an error (or raise a new error), in which case it would propagate to the next outer handler. If no handler is present, the whole evaluation results in an error.

Hint: you’ll want to add a new variant to the Cont datatype, and you’ll want to revise the definition of handleError.

c. call-with-context takes two arguments. The first (call it ctx) may be any value, and the second must be an applicable value (function or primitive operator, call it thunk); call-with-context augments the global context with ctx for the evaluation of thunk (again, applied to an arbitrary value). This context may be read by calling get-context (described below).

The result of the whole expression is the value returned by thunk. When control escapes from the call to call-with-context, whether by ordinary return, raising of an error, or a continuation jump,ctx should “pop” out of the global context.

Hint: you’ll again want to add a new variant of the Cont datatype.

d. get-context takes one argument (which it ignores), reads the global context, and returns a list containing all the values that have been “pushed” by call-with-context, starting with the innermost. For example:

(get-context 12345) => empty

(with* ([f (fun (x) (pair x (get-context 12345)))])

  (call-with-context

   “there”

   (fun (_) (call-with-context

             “hi”

             (fun (_) (f true))))))

=> (true, (cons “hi” (cons “there” empty)))
(pair (call-with-context “context” (fun (_) “hi”))
; we’ve left the call-with-context, so the context is empty again …
(get-context true))
=> (“hi”, empty)

e. call/cc (“call with current continuation”) captures the current continuation, wraps it as a value (you can use PrimV for this) and applies its argument (which must be applicable) to that continuation. As discussed in lecture, you can think of call/cc as a more general, desugared version of let/cc. Calling the continuation should “return” the argument to the point in the control flow where the continuation was captured.

(let/cc k e) <=> (call/cc (fun (k) e))

See the slides/lectures from weeks 5 and 6 for interesting examples of how continuations can be used.

For example, here’s a slightly modified version of the Fibonacci example (end of lecture 5 slides) translated into the syntax our parser understands:

(with* ([y (fun (f)

             ((fun (g) (f (fun (x) ((g g) x))))

              (fun (g) (f (fun (x) ((g g) x))))))]

        [fib (y (fun (fib a b yield/rtn)

                  (with* ([yield/rtn (call/cc (fun (k) (yield/rtn (pair a k))))])

                    (fib b (+ a b) yield/rtn))))]

        [iterate (y (fun (iterate n f x)

                      (if (= n 0)

                          x

                          (iterate (+ n -1) f (f x)))))])

  (iterate 20 (fun (p) (call/cc (snd p))) (pair 1 (fib 1 1))))

This should evaluate to:

Ok (6765, <primitive: continuation>)


When you’re finished, hand in your modified version of InterpCont.hs.

Homework 4
This homework is due on Friday, March 13 at 11pm. However, in exception to the general late policy, we’ll accept it up to 2 days late with only a 5% penalty.

In this homework, we’ll implement a type-checker for a language with functions and explicit universal quantification over types (aka, parametric polymorphism, generic types). The syntax is similar to that of the languages in the previous two assignments, except that we’ve added type annotations on function arguments and a notation for abstracting over types and instantiating parametric types. We’ve provided datatype definitions and parsers for this language. You should start by downloading Result.hs, Token.hs, SExp.hs, Expr.hs, and TypeCheck.hs.

The new concrete syntax is as follows:

— Types.
<t> ::= num | bool | string — basic types
| (<t> , <t>) — pairs
| (list <t>) — lists
| (<t> -> <t>) — functions
| (forall a . <t>) — universally quantified types

— Expressions (surface syntax).
<e> ::= … — previous expression types (note below how function syntax has changed)
| (fun ([x : <t>] …) <e>) — types of function arguments must be declared
| (forall (a …) <t>) — expression with universal quantification over type variables a …
| (<e> < <t> … >) — instantiation of a polymorphic expression with specific types <t> …

Examples:

(fun ([x : num]) (+ x 3))

(with* ([id (forall (a) (fun ([x : a]) x))])
((pair <num bool>) ((id <num>) 3) ((id <bool>) true)))

(forall (a b)

   ((fix <((a -> b) -> ((list a) -> (list b)))>)

     (fun ([map : ((a -> b) -> ((list a) -> (list b)))]
             [f : (a -> b)]
             [lst : (list a)])

         (if ((cons? <a>) lst)

             ((cons <b>) (f ((first <a>) lst))

                                (map f ((rest <a>) lst)))

             (empty <b>)))))

Problem 1. In Expr.hs, complete the implementation of the function `alphaEquiv`, which determines whether two types (possibly involving universal quantification) are equivalent up to alpha-renaming of bound type variables. The third argument, `typeVarMap`, is a stack of correspondences of type variables in the two types. (So, when comparing two “forall” types, you should push a pair with their respective type variables onto `typeVarMap` for the recursive comparison of the bodies.)

For example:
— Free type variables are compared for simple equality.
alphaEquiv (VarT “c”) (VarT “c”) [] ==> True
alphaEquiv (VarT “d”) (VarT “e”) [] ==> False

— Bound variables are equivalent if they were bound by corresponding foralls.
alphaEquiv (ForAllT “a” (ArrowT (VarT “a”) (VarT “c”))
(ForAllT “b” (ArrowT (VarT “b”) (VarT “c”))) [] ==> True

alphaEquiv (ForAllT “a” (ForAllT “b” (ArrowT (VarT “a”)
(ArrowT (VarT “b”) (PairT (VarT “a”) (VarT “b”))))))
(ForAllT “b” (ForAllT “c” (ArrowT (VarT “b”)
(ArrowT (VarT “c”) (PairT (VarT “b”) (VarT “c”)))))) [] ==> True

alphaEquiv (ForAllT “a” (ForAllT “b” (ArrowT (VarT “a”)
(ArrowT (VarT “b”) (PairT (VarT “a”) (VarT “b”))))))
(ForAllT “b” (ForAllT “c” (ArrowT (VarT “c”)
(ArrowT (VarT “b”) (PairT (VarT “b”) (VarT “c”)))))) [] ==> False

— The nesting order for universal quantifiers is significant.

alphaEquiv (ForAllT “a” (ForAllT “b” (ArrowT (VarT “a”)
(ArrowT (VarT “b”) (PairT (VarT “a”) (VarT “b”))))))
(ForAllT “b” (ForAllT “a” (ArrowT (VarT “a”)
(ArrowT (VarT “b”) (PairT (VarT “a”) (VarT “b”)))))) [] ==> False

— Alpha equivalence is not unification.
alphaEquiv (PairT (VarT “a”) NumT) (PairT BoolT (VarT “b”)) [] ==> False

— A tricky example that you’ll want to make sure your code handles correctly.
alphaEquiv (ForAllT “a” (ForAllT “b” (PairT (VarT “a”) (VarT “b”))))
(ForAllT “a” (ForAllT “a” (PairT (VarT “a”) (VarT “a”)))) [] ==> False

Problem 2. In TypeCheck.hs, complete the implementation of the function `freeTypeVars`, which returns all of the type variables that occur free in a given type. (Its second argument, `bound`, is the set of bound type variables, which grows when we enter the body of a “forall” type expression.)

Examples:
freeTypeVars (ArrowT (VarT “a”) BoolT) [] ==> [“a”] freeTypeVars (ForAllT “a” (PairT (VarT “b”) (VarT “a”))) [] ==> [“b”] freeTypeVars (ForAllT “a” (PairT NumT (VarT “a”))) [] ==> []

It’s fine if your implementation returns a list with duplicate elements (when a variable occurs more than once).

Problem 3. In TypeCheck.hs, complete the implementation of `alphaRename`, which renames a given type variable within a type expression. The function should rename all occurrences of the variable, including binding occurrences.

Examples:
alphaRename “a” “b” (ListT (VarT “a”)) ==> ListT (VarT “b”)
alphaRename “a” “b” (ForAllT “a” (PairT (VarT “a”) BoolT)) ==> ForAllT “b” (PairT (VarT “b”) BoolT)

Problem 4. In TypeCheck.hs, complete the implementation of `subst`, which subtitutes a type for a type variable in another type and returns the result. The substitution must be capture-avoiding, as discussed in lectures 2 and 6. You’ll want to use the implementations of `freeTypeVars` and `alphaRename`. You’ll also need the provided functions `allTypeVars` (which returns all type variables in an expression) and `genFreshVar` (which generates a name that’s distinct from everything in a list).

Examples:
subst “a” NumT (ArrowT (VarT “a”) (VarT “a”)) ==> ArrowT NumT NumT
subst “b” (PairT NumT BoolT) (ListT (VarT “b”)) ==> ListT (PairT NumT BoolT)
subst “a” NumT (PairT (VarT “a”) (ForAllT “a” (ArrowT (VarT “a”) (VarT “a”)))) ==>
PairT NumT (ForAllT “a” (ArrowT (VarT “a”) (VarT “a”)))
subst “a” (PairT BoolT (VarT “b”)) (ForAllT “b” (ArrowT (VarT “a”) (VarT “b”))) ==>
ForAllT “c” (ArrowT (PairT BoolT (VarT “b”)) (VarT “c”))

In the last two examples, note how (1) we don’t susbstitute inside a ForAllT whose variable shadows the variable we’re substituting and (2) we alpha-rename (b to c, in this case) to avoid capture of free type variables in the substituted type (the b in (bool, b) in the last example).

Problem 5. In TypeCheck.hs, complete the implementation of `checkType`, which checks the type of an expression in a given context. The context (i.e., “gamma” from type inference rules) is a pair containing (1) a collection of bound type variables and (2) bindings of program variables to types. When checking a type annotation in the source, you’ll want to make use of another helper we’ve defined called `checkClosed`, which checks that a type expression contains no free type variables (in a given context). We’ve also provided an `initialEnv` with primitives from previous assignments, including polymorphic bindings for list and pair operations and a fixed-point combinator.

A few more examples:

1 :: num

(+ 2 4) :: num

(fun ([x : num]) (= x 5)) :: (num -> bool)

— Self-application of identity function:
(with* ([id (forall (a) (fun ([y : a]) y))] [selfapp (fun ([x : (forall a.(a -> a))])

                   ((x <(forall b.(b -> b))>) x))])
(selfapp id)) ::  (forall b.(b -> b))

— Addition and multiplication of Church numerals.
(with* ([two (forall (a)

                     (fun ([s : (a -> a)]
                             [z : a])

                          (s (s z))))] [add (forall (a)

                     (fun ([n : ((a -> a) -> (a -> a))]
                             [m : ((a -> a) -> (a -> a))]
                             [s : (a -> a)]
                             [z : a])

                            ((n s) (m s z))))]
            [mult (forall (a)

                       (fun ([n : ((a -> a) -> (a -> a))]
                               [m : ((a -> a) -> (a -> a))]
                               [s : (a -> a)])

                              (n (m s))))])
(((mult <num>) ((add <num>) (two <num>) (two <num>))

         (two <num>)) (+ 1) 0)) :: num

Problem 6. In Expr.hs, complete the implementation of `erase`, which erases type information and finishes desugaring a DExpr to a CExpr (e.g., rewriting WithD expressions to a combination of AppC & FunC). (The resulting expression could be evaluated with the interpreter you wrote in homework 3.)


When you’re done, hand in your modified copies of Expr.hs and TypeCheck.hs.

Late Policy: Credit for late homework will be discounted by 10% per day for up to three days after the due date. After that, no credit will be given, unless arrangements were made in advance to accommodate an exceptional hardship.

Software

The course will use the Haskell programming language, which is freely available for recent versions of Windows, Mac OS, and Linux. The instructor uses haskell-mode for Emacs, but many other options are available for non-Emacs users.

Online Resources

haskell.org – the language’s homepage (docs, extensive wiki)
Learn You a Haskell – a free, popular online guide to Haskell
Real World Haskell – a free online book about Haskell focusing on real applications
The Haskell wikibook – very complete (and of course it’s free and online)

Approximate Schedule of Lecture Topics

  1. Course intro. Programming in Haskell. Syntax; parsing; evaluation.
  2. Variables; substitution; scope and environments. Functions. Evaluation strategies. (slides)
  3. Mutation. Monads. (slides)
  4. Untyped lambda calculus. Church encodings. Y-combinator. (slides)
  5. Continuations. (slides)
  6. Continuations, part 2; formal semantics (big-step). (slides)
  7. Small-step operational semantics. Simply-typed lambda calculus. (slides)
  8. Explicit parametric polymorphism (System F). Unification, Hindley-Milner type inference. Type soundness. (slides)
  9. Curry-Howard Correspondence. Recursive types. Subtyping. (slides)
  10. Something fun. (slides)

Leave a Comment

Your email address will not be published. Required fields are marked *

Loading...
Scott Ge