Type systems: the strong, the strict and the safe.
Or the weak, the loose, and the unsafe. But does it mean anything?
After a couple of corona semesters, the forthcoming one seems to be unaffected by any viruses, and things are back to normal. So right now, at the end of the spring semester, we plan for a semester in a standard, non-corona set-up.
We should, however, keep in mind the the virus plague is not over yet and right now, towards end of June, the infection rates go up in many countries throughout Europe. Currently, there seems politically no push towards (re-)introducing restrictions, as the variants responsible for the current rise in incidences are of a ``milder’’ variety. So no cause of alarm, they say.
I suspect, however, not even experts can foresee the future, and they base their prognostications of what will happen next autumn on what had happened last autumn. Still, the rise is disquieting, because at the beginning of this year, experts seems sure, that at least it will be a hassle-free summer, perhaps or probably there might be a next wave in autumn or winter, but in the meantime, we can all forget about viruses. But now the numbers are rising already before the calendaric summer has started.
So we can hope for a normal and relaxed semester, but keep in mind it could turn out otherwise (again).
Lectures will be held the way it used to be before corona, if someone still remembers, i.e., in the lecture hall.
One perhaps positive effect of the virus times was that many lectures produced video-ed versions of the presentations, like screencasts or recorded lectures. This lecture as well. We will not make a new version of the videos, there is no reason for doing that, but will link in the versions produced mostly 2020, uploaded at youtube.
The lecture will be given in Norwegian, at least that’s the plan. It’s actually my first lecture ever given in Norwegian. We have to see how it goes. If it’s incomprehensible, or the pronounciations unbearable, we’ll have to consider alternative solutions. In these (inofficial) pages, however, I’ll write in English, it takes too much time otherwise.
The videos are a fine supplementary information and format. Though reading the book and in particular doing the exercises is central for mastering the material. I like to compare that with learning to play the guitar. No particular reason for exactly choosing guitars as comparison, except that at the moment and since some time I try to learn doing that. Of course one can watch and listen to Eric Clapton, Andrés Segovia, or Eddie van Halen on youtube (or whatever your top guitar hero might be), maybe watching the close-ups of the finger plays, or listening to some guitar teacher. That may be instructive, watching and reading and listening may help to correct the way you hold your guitar or your fingers, or you may see new techniques, and it sure will be inspiring and motivating, to see and listen to some masters.
But unless one strums the six strings with one’s own fingers, starting with simple chords, and gradually advancing the level of difficulty, one will never get far.
And the same here. Therefore, doing the exercises is important!
Learning is not the product of teaching. Learning is the product of the activity of learners. (John Holt)
Or the weak, the loose, and the unsafe. But does it mean anything?
A small amount of background information (best read in the context of the first sets)
or maybe also not the first time.
A glance at Church numerals, inductive data types, and pattern matching
Or maybe how not to implement it?
(White-)space exploration, FORTRAN, lexing, antiquity & fetischism
or why Y?
A lesser known fact on Ackermann’s function
like for instance the compiler construction course.
Some clarification (I hope)
Formal methods as sales pitch
In the lecture, we covered type inference for generic polymorphism in a typed calculus with higher-order functions, including recursive functions and let-bin...
Some remarks about variations on the theme