Higher Kinded Parametricity

I've moved to Bengaluru to teach functional programming (and other things) to my team in Atlassian. Our project is a large Scala application. Scala enables functional programming, but it is only made possible, not easy.

Instead of using Scala to teach functional programming, we should use something easier. For a few years I've been using Haskell to teach functional programming. Sometimes I hear from people that Elm, Kotlin or Java could be easier. I want to write about a big benefit I get out of Haskell that I wouldn't be able to get from these tools.

The Data61 fp-course contains a lot of functional programming exercises. It starts with Optional and List, then moves to Functor. One of the Functor exercises is the `void` function:

``````void ::
Functor f =>
f a
-> f ()``````

This takes a bit of explaining. I explain what `Functor` is, then I explain what the parametric type constructor `f` means.

Elm, Kotlin and Java lack the type-system feature which makes the above type possible to write. It's not an exercise that can be given. Instead, we'd have code duplication:

``````voidOptional ::
Optional a
-> Optional ()

voidList ::
List a
-> List ()``````

Code duplication might seem preferable because these types don't contain things we have to explain. The problem comes at implementation time.

Our original `void` type had only one inhabitant:

``void fa = const () <\$> fa``

But our `voidOptional` has four inhabitants:

``````voidOptional = const Empty

voidOptional = const (Full ())

voidOptional Empty = Full ()
voidOptional (Full _) = Empty

voidOptional Empty = Empty
voidOptional (Full _) = Full ()``````

And `voidList` has infinite inhabitants!

Making things specific instead of polymorphic makes things more complicated. Someone trying to work on the `void` exercise will use Haskell's tools to get directed toward the solution. If the exercise got split into the specific versions, people no longer get directed; implementors have to be careful.

This concept is parametricity on type constructors. When teaching, I see people quickly gain an intution for parametricity and use it as a reasoning tool, over and over.

The Functor exercises come after the Optional and List exercises. The Functor exercises exist to teach about the operations that Functor provides. They do not exist to teach about Optional and List, so should not have to mention them.

During my experience with teaching Haskell, I have seen people learn Functor, Applicative and Monad functions very quickly. I think a big part comes from using parametricity during the exercises. I do not agree that Elm, Kotlin nor Java could make learning these functions easier.