Announcements

The "Sample Exam" materials have been on the left sidebar for a while, including a link that lets you try out the exam website.

The "Final Exam" link is now on the sidebar too, near the top. This links to the exam site. The exam site will go live and let you begin the exam from tomorrow at 9:30AM. As mentioned in various places, you can sit the exam in any 2 hour block (+ 10 minutes reading time, + a time adjustment for students with relevant ELPs). You don't have to start at 9:30AM, but you do need to start it before 11:30AM.

There are more relevant hints on the forum. The forum will now go into "exam mode" where students can only add private topics, and we will make them public as appropriate.

I have uploaded the notes from today's review lecture, where we worked through some sample exam questions together.

By the way, I can confirm our answer for Q3 C) regarding the existentially typed function having no concrete value it can be applied to was correct - unless you count the special Error value we discussed in Week 7, which can be of any type! -Rob

I have uploaded the solutions to this week's tutorial.

Note also that there are some sample exams available (see the left sidebar). The "Take the Exam" link will take you to a sample exam interface (accessible using your zID credentials) to give you an idea of the interface for the final exam, which will be online. You can view its solutions, reset it and re-attempt it as many times as you like. Also, please feel free to ignore the sample questions regarding "most general unifiers" and STM, which are not part of this year's course. -Rob

I have uploaded the notes from today's lecture on concurrency and session types.

Thursday's lecture will be a revision lecture. Please gather any questions or topic areas you want us especially to address in that lecture. -Rob

I had forgotten to upload Week 9's tutorial solutions - they are up now. -Rob

I've updated the Assignment 2 spec (now version 1.4.2) to clarify that the output Program of your infer function is what will be compared with the expected output for marking (not the output of tyinf --dump type-infer).

I have also uploaded the code and notes from today's lecture on overloading and subtyping, as well as longform notes on these topics. -Rob

I have uploaded the code and notes from today's lecture on existential types and brief introduction to monads. -Rob

Please note I have updated the Assignment 2 spec (now version 1.4.1) to fix a bug in the PROGRAM rule in Figure 3. It should have only one premise, which should say that scheme σ can be inferred directly from expression e using a GEN judgement - not an INF or any other judgement! Thanks to the student who spotted that.

Additionally, an introductory video from last year that explains the approach and some of the infrastructure for the assignment (final 20min of the video) and includes a more thorough walk-through of last Thursday lecture's type inference example (from about 20min in) has been posted to the Echo360 video set for this class. You can find this in your Echo360 videos (e.g. by following a link from Moodle). Many thanks to Craig McLaughlin for giving us his permission to re-release it. -Rob

Assignment 2: "Type Inference for Polymorphic MinHS" is now released.

Again, please let us know on the Ed forum if you have any issues accessing or using the supplied material.

I have uploaded the notes I presented in today's lecture on type inference, relevant adapted longform notes, and the solutions to this week's tutorial. -Rob

I have uploaded the Haskell demo code and notes from today's lecture on parametric polymorphism. -Rob

The 3161 exam date was moved to Friday the 29th of November. There should not be any clashes with other courses, but we know of one clash with a supplementary exam scheduled for the T3 exam period. Please check your exam timetable and get in contact if you have a clash on the 29th.

We have given this hint about Assignment 1 to a few students: The Haskell sources you were supplied with can help you understand the relationship between Hindsight concrete and abstract syntax. In a few parts of the spec document, the types and meaning of Hindsight elements are described using the concrete syntax the user would type. If you are struggling to understand how this relates to the syntax tree which the evaluator must process, note that you already have a working parser for Hindsight. The "minhs" binary can be built even if you haven't implemented much of the evaluator, and it includes a way to examine the abstract syntax of example Hindsight programs.

There will be another round of help sessions this week. Updates about that on the relevant pinned post on the forum.

We have a survey invitation for students who are (a) international and (b) doing a dual-degree such as Engineering/Commerce or Engineering/Science. The survey is being done by UNSW academics to better understand differences in teaching style. If you are in that group and want your voice to be heard, use this QR code to join the survey:

I have uploaded the Haskell demo code and notes for product, sum, unit, empty and recursive types from today's lecture, as well as this week's tutorial solutions. -Rob

We have finished marking assignment 0 "Proofs".

You should be able to view your marks by running `3161 classrun -check Proofs` on a CSE computer or by connecting to the web interface to give here .

The spec document has been updated to version 1.0.6.

Thanks to the eagle-eyed readers, who spotted two type-incorrect elements. It is now clearer that primitive arithmetic ops like addition are computational values, so they have the '↓c' big-step form not '↓v'. Addition must be reduced before it can be used as a function argument, so the previously incorrect example in the 2.9 recfun explanation has been fixed.

I've uploaded the notes I made during yesterday's lecture, as well as longform notes regarding the lecture's content on trace properties, type safety, errors and exception handling. -Rob

I have uploaded the demo of Haskell laziness from the Thursday lecture.

Two revisions to the Assignment 1 spec have been uploaded. If you have a copy of the spec document which shows a 2023 due date, download a fresh version. Another update has been made to fix a typo in the presentation of the dynamic semantics of primitive ops, thanks to the student who spotted that.

Assignment 1: "Hindsight" is now released. Let us know on the Ed forum if you have any issues accessing or using the supplied material.

Marking assignment 0 is underway. The completed week 5 tutorial is uploaded. Remember to flex during "flex week" in the coming week, and see you in week 7!

The proof sketch and code written in the lecture are up, as is the tutorial, and the longform note on abstract machines.

The code from the lecture is up. There were a couple of questions about eta-reduction in the help sessions. I have put up a shorter longform note summarising the equivalences of the lambda calculus.

Thanks to the student who looked at the clarified Part C and noticed that part of the question had gone missing. That is now fixed. Part C has two subparts. If you can't find one of them, download it again.

I have put up a long-form note about the tiny imperative language and Hoare logic we discussed in today's lecture.

There have been multiple questions about Part C. The spec document has been updated to include some notes of clarification.

We have uploaded some long-form notes written in earlier iterations of this course. They may make it easier to revise the material from the earlier lectures than going over the slides. See the 'Longform Notes' section in the page outline. The Haskell code and partial proof from Tuesday's lecture, and the completed tutorial from Week 2, have also been uploaded.

The assignment deadline has been extended from Mon 30th Sep to Fri 4th Oct.

The code and proof sketch from the lecture has also been uploaded.

Uploaded a longer version of the L-M-N lemma proof in a homework style to the Week 2 region. The source is also in the same place as the TeX snippet example.

Fixed the typo "marks will be won or lots" to "no marks will be won or lost" in the TeX snippet guide.

As requested on the forum, we've uploaded the TeX source of some of the maths syntax used in the assignment spec and lecture slides.

The spec for assignment 0 is now visible. The assignment will be due on Monday the 30th and will be submitted via CSE's give mechanism. This assignment release is fairly early so that you can look at the whole assignment, get started on the syntax parts, and think about compilation and scope issues. The material related to scope checking and semantics will be covered on Tuesday the 24th, and the lambda calculus material will be covered on Thursday the 26th.

More files will be added to this website as the course progresses, so look at what is available for each week on the left sidebar.

The Ed forum was set up in Week 1. Everyone who was enrolled on the 8th of September should have received an invitation email to their official UNSW email address (zXXX@ad.unsw.edu.au) inviting you to join. If you have joined the course more recently, or otherwise have not yet gotten an invitation email yet, please email the class account cs3161@cse.unsw.edu.au soon.

The Ed forum will be the primary venue for discussion and announcement in the course going forward.

Make sure to log in to Ed with zXXXXXXX@unsw.edu.au as your username—Ed doesn't understand UNSW email aliases well and has a proclivity for creating redundant accounts. If something isn't working email cs3161@cse.unsw.edu.au as soon as possible and we can get it sorted.