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.