Iowa Type Theory Commute
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
Iowa Type Theory Commute
Begin chapter on subtyping
•
Aaron Stump
•
Season 4
•
Episode 10
We begin a discussion of subtyping in functional programming. In this episode, I talk about how subtyping is a neglected feature in implemented functional programming languages (for example, not found in Haskell), and how it could be very useful for writing lighter, more elegant code. I also talk about how subtyping could help realize a new vision for practical strong functional programming, where the language has a pure, terminating core language, then a monad for pure but possibly diverging computation, and finally a monad for impurity and divergence.