MuniHac 2020: Richard Eisenberg - Partial Type Constructors

Title: Partial Type Constructors
Speaker: Richard Eisenberg

When we describe the type Set a, we say that this type makes sense for any a. But this is a small lie: it really only makes sense for types a that have an ordering – that is, types for which Ord a holds. This small lie has far-reaching consequences. It means that we cannot write a Functor instance for Set, it means we might accidentally write uncallable functions that take a Set, and it means we must repetitively write Ord a ... constraints on every function working with Sets.

This talk will explore the possibility of explicitly partial type constructors, where we can declare loudly that types like Set work only with some type arguments, but not others. The design proposed improves error messages, simplifies type signatures, and allows instances like Functor over Sets.

[AlexBerg]

Amazing!
Eisenberg is amazing! This research and explanation is amazing! The slides are amazing!
Thank you, Richard!

[GergoErdi]

I think a "tricky example that *needs* quantified type application constraints" example they were looking for at the end could be something like the traversal of a free monad.

[progrockkeyboardist]

This is something that ML gets right and Haskell gets wrong. Some abstractions are not parametrized by just types, but rather by more elaborate *structures* that contain types and also contain other things.

And, by the way, in this proposal, `fmap` is wrong. For the `Functor` instance on `Set` to make sense, `fmap` must only be applied to strictly monotone functions.