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.

Links: Lecture slides; Exam arrangements

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 18: Dependent Types

Title slideToday’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.
Continue reading

Lecture 17: Higher Polymorphism

Title slideBeyond 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…
Continue reading

Lecture 16: Parameterized Types and Polymorphism

Slides for APL Lecture 16: Parameterized Types and PolymorphismThis 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.
Continue reading

Lecture 15: Guest Lecture by Bob Atkey

APL Lecture 15: Guest Lecture by Bob Atkey - Static Analysis for Java Concurrency with ThreadSafeStatic Analysis for Java Concurrency with ThreadSafe
Bob Atkey
Heriot-Watt University

Bob AtkeyI’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 issue report 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.

Links: Slides; Bob Atkey; Contemplate

Lecture 14: Terms and Types

apl14Friday’s lecture began a final block of material on types in programming languages: some of the ways they are used, and their relation to the mathematical models of lambda-calculus and type theory. This lecture presented the simply-typed lambda-calculus and some examples of programming language support for first-class functions. Continue reading