November 12, 2021

<aside> 🔗 Slides can be found at : "https://github.com/juniorxxue/talks/tree/main/hkuplg-2021-11-12"

</aside>

<aside> 👉 This article is derived from my problem session at HKU PL Research Group.

</aside>

Warm-up

Typed Racket, considered as the most sophisticated type system for Scheme, demonstrates a way how to type check untyped program incrementally, idiomatically, and type safely. The secret behind it is occurrence typing.

In this article, we trace back to the origin of occurrence typing and see how Typed Racket benefits from it without introducing new idioms. And we can further see how refinement types fundamentally subsume it.

<aside> 💡 Interested audiences may want to skim the introduction in Andrew M. Kent’s Ph.D. dissertation “Advanced Logical Type Systems for Untyped Languages” or play with some trivial examples in Liquid Haskell but it’s not compulsory.

</aside>

Sorry for failing the expectation, the original title written in the email is "From Occurrence Typing to Refinement Types", but considering the timing and also the length of contents, I put "On Understanding Occurrence Typing" as the main focus, and try to reveal the mechanism behind it.

What is Occurrence Typing?

So, What is Occurrence Typing? I believe people would have their own opinions about it. But there're still some misunderstandings.

• "Is it just a type-safe downcast?"
• "Is it a kind of typed-driven overloading?"
• "Is it one of dependent type systems?" or
• "Is it just a dynamic type checking?"

eh? some are correct and some are not, I will answer one by one at the end of the talk.

According to the Wikipedia (believe it or not, it has its own wiki page):

In programming language theory, flow-sensitive typing (also called flow typing or occurrence typing) is a type system where the type of an expression depends on its position in the control flow.

I doubt its correctness, but apparently this definition has already been accepted by most of people.

In fact, occurrence typing has become extremely both in industry and academia, and both has gone too far, in totally different directions. So it's reasonable that people would like to view it differently.

But if you want to ask "is there a one that's both practical enough and has been reasoned exhaustively?"