Tuesday 11 October is Ada Lovelace Day, and the University of Edinburgh is hosting a series of events in the Main Library. There’s no APL lecture in the afternoon: come along and help improve Wikipedia.
- AM: Guest talks, activities, building things
- PM: Women in STEM Wikipedia edit-a-thon
Link: Event description and booking
Ada Lovelace Day is an international celebration day of the achievements of women in science, technology, engineering and maths (STEM). It aims to increase the profile of women in STEM and, in doing so, create new role models who will encourage more girls into STEM careers and support women already working in STEM.
Links: Ada Lovelace Day; Map of events worldwide
To find out more about Ada Lovelace and her impact on computing — including programming — then I recommend watching these.
“It may be desirable to explain, that by the word operation, we mean any process which alters the mutual relation of two or more things, be this relation of what kind it may. This is the most general definition, and would include all subjects in the universe.”
Ada Lovelace, 1842, identifying the
scope of application for a programmable computer
This lecture completes the quartet of type/term interactions: after first-class functions, parameterized types, and polymorphic terms, we have types that depend on the value of terms. Numerical examples include types to capture vector lengths and matrix dimensions. 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 seen earlier in Wadler’s talk, 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 6: Dependent Types
The coursework assignment for APL is to select a programming language feature from a short list, research what it does, try it out, and write a 10-page report about this. In today’s lecture I presented each of the five possible topics and outlined the assignment structure.
Continue reading Lecture 5: Coursework Assignment Topics
Beyond the simply-typed lambda-calculus, and even Hindley-Milner polymorphism, there’s a world of type systems for more expressivity, more precision, and more polymorphism. Today’s lecture looked at some of this: issues around subtype polymorphism in object-oriented code, motivations for higher-rank polymorphism, and beyond that to 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 4: Higher Polymorphism
||1pm Thursday 29 September
||IF 2.33, Informatics Forum
PLInG is an informal meeting series for Informatics students and staff interested in programming languages. It’s organized by James Cheney and Michel Steuwer with meetings every fortnight or so.
All are welcome to attend, and the format is flexible: with presentations of work in progress, interesting recent papers, reports from conferences, or discussion with visitors. This first meeting is to make plans for the semester and hear trip reports from those just back from last week’s International Conference on Functional Programming (ICFP) in Japan.
Links: Meeting schedule; Mailing list
Today’s lecture gave examples of parameterized types in different programming languages: families of data types with a common structure, built by applying type constructors to one or more type parameters; as in Java or C# generics, or the algebraic datatypes of Haskell and 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).
Continue reading Lecture 3: Parameterized Types and Polymorphism
|APL Lecture 3: Tuesday 26 September 1510–1600
Room G.10, Geosciences
This Tuesday’s lecture will be in a different venue again. If it’s suitable then we’ll be able to reuse for most Tuesdays through semester.
I’ve also posted a set of slides for tomorrow to the Lecture Log page.
Links: Drummond Library Location
Continue reading New Room for Tuesday Lecture
Friday’s lecture introduced the first topic for the course, 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 Lecture 2: Terms and Types
|APL Lecture 2: Friday 23 September 1510–1600
|Medical School Basement Lecture Theatre
Room G.152A, Doorway 6
I have located a smaller venue for this Friday’s lecture, and I hope all following Fridays. On Tuesday afternoons it’s in use by another course, so the search for something suitable continues.
Link: Medical School location
This opening lecture presented some context for studying programming languages, and what might inspire research into new ones. You can read some of this in the slides which are also available by clicking on the title slide image to the right.
Continue reading Lecture 1: What’s So Important About Language?