# Afterword

Lectures and coursework for APL are now complete. The exam will be held in the April/May diet; exact dates will be announced by the Student Administration Service on Monday 2 March 2015.

If you have any questions about the course, or would like to discuss preparation for the exam, then please send me email or drop in during my office hours, 1030–1130 every Wednesday during semester.

Thank you for your participation and contributions to this course.

# Individual Coursework Feedback

I have just sent out by email the grades and detailed feedback sheets for all students’ coursework submissions. My apologies for the extended delay in marking and returning this.

If you would like a short one-to-one meeting for individual feedback then please send me an email to arrange a time at the start of Semester 2.

Thank you for your participation in the course, and I wish you all well for the remainder of your studies in Edinburgh.

# Lecture 19: Exam Review

This final lecture for the course included advice on the exam structure and content, some general information about different kinds of assessment, and discussion of specific questions from previous papers.

# Lecture 18: Dependent Types

Today’s lecture presented the final component in the quartet of type/term interaction: after first-class functions, parameterized types, and polymorphic terms, we have types that depend on the value of terms. Numerical examples include type-safe vectors and matrices; but dependent types can also be used to strengthen the deep embedding of domain-specific languages into a host meta-language. Examples given included typed lambda-terms and logical formulas. The lecture also touched on the Curry-Howard correspondence of propositions-as-types and the use of dependently-typed programming in the machine-assisted proof of mathematical theorems. Finally, there were some references to dependently-typed languages for writing and verifying programs that are correct-by-construction.

# Lecture 17: Higher Polymorphism

Beyond the simply-typed lambda-calculus, and even Hindley-Milner polymorphism, there’s a whole world of type systems for more expressivity, more precision, and more polymorphism. Tuesday’s lecture looked at some of this: issues around subtype polymorphism in object-oriented code, motivations for higher-rank polymorphism, and the wonders of System F. For System F in particular there’s a range of further possibilities: this lecture covered encoding datatypes, but there are also subtyping, bounded and F-bounded quantification, F2, Fω, existential types, and more…

# Lecture 16: Parameterized Types and Polymorphism

This lecture presented examples of parameterized types in different programming languages: families of data types with a common structure, built by applying type constructors to on or more type parameters; as in Java or C# generics, or the algebraic datatypes of Haskell or OCaml. To work with parameterized types we use polymorphic functions — code that can work with more than one type, either in a uniform way (parametric polymorphism) or with type-specific variations (ad-hoc polymorphim). The Hindley-Milner type system, illustrated in this lecture as applied to the simply-typed lambda-calculus, expands types into type schemes that summarize multiple possible types of a polymorphic function. Hindley-Milner is distinctive in guaranteeing that any code has a principal type scheme that captures every possible type, and the efficient Algorithm W for type inference which can find (“infer”) that most general type scheme.

# Lecture 15: Guest Lecture by Bob Atkey

## Static Analysis for Java Concurrency with ThreadSafe Bob Atkey Heriot-Watt University

I’m very pleased to have Bob Atkey present a guest lecture in APL.

Bob is a researcher and developer: his extensive original research on programming languages, types, and effects stands alongside practical work such as that with Edinburgh spin-out Contemplate on their flagship ThreadSafe product for early detection of concurrency bugs in Java.

 ThreadSafe: Static Analysis for Java Concurrency ThreadSafe is the leading static analysis tool for finding and diagnosing dangerous concurrency bugs in Java code. Why wait for customers to find what ThreadSafe can help prevent? Take your free trial today.

He is also an engaging and approachable speaker, and I strongly recommend coming along to hear him this afternoon.

Friday’s lecture presented two different methods for Java programs that are intended to help with writing correct code: the standard Java assert statement; and JML, the Java Modeling Language. Continue reading