On Friday, I gave a talk at the Scottish Programming Languages Seminar (SPLS) at Heriot-Watt. Many thanks to Greg Michaelson for organising everything and giving me time to speak.
I've put the slides I used on-line as a PDF file (with two small fixes, see below).
The talk presents an extension of a Nakano-style typed λ-calculus with a delay modality for guarded recursion. In short, this means:
▷so that for any type
A, there is another type
▷ Arepresenting an
Adelayed by one step in the current time stream.
replaceMinfunctions as examples of this.
As I mentioned during the talk, this is based on Conor's blog post Time files like an Applicative Functor from over two years ago.
The hoped-for outcome is a nice way of programming with codata in a functional language like Haskell. Still more hopefully, this will extend to systems with dependently types too, though I am still confused about where the clock variables ought to live.
I fixed two typos that were present in copy of the slides that I used in the talk:
On slide 18 (page 42 in the PDF), I had “Time Files like an Applicative Functor” as the title of Conor's blog post. Obviously, time is rubbish at filing, or at least not as good as applicative functors are.
On slide 28 (page 57 in the PDF), I had the semantics of data type descriptions as an endofunction on some undefined curly D thing. It ought to be the powerset of the semantic domain.