Iowa Type Theory Commute

Begin chapter on subtyping

June 20, 2023 Aaron Stump Season 4 Episode 10
Begin chapter on subtyping
Iowa Type Theory Commute
More Info
Iowa Type Theory Commute
Begin chapter on subtyping
Jun 20, 2023 Season 4 Episode 10
Aaron Stump

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.

Show Notes

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.