Teaching Polymorphism

Post.md

"Is Haskell a good first programming language?"

This question was asked at the recent HaskellX conference, with both practicioners as well as teachers being present. I won't reiterate everything that was said, and instead link to a recording of the podium discussion (https://skillsmatter.com/skillscasts/10952-park-bench-panel-session-with-haskellx-experts).

One particular argument, that I've heard come up multiple times now, is that teachers are complaining about the length function being polymorphic. Apparently length :: forall a. Foldable f => f a -> Int is hard to grasp/understand/accept for a new-comer. The solutions proposed to solve this problem are to:

1. Return length to its non-Foldable type
2. Use a custom Prelude to teach beginners

Drawbacks for 1 include that practicioners like the fact that length works for all kinds of data structures, and don't want that taken away from them. The primary problem with solution 2 is that students can't go and use their aquired knowledge to work on Open Source Haskell projects, because Real-World-Haskell does not use their custom learning Prelude.

The discussion also mentioned that other languages might be better suited and specifically highlighted Elm and PureScript. Elm doesn't suffer from the mentioned problem, because it doesn't support the kind of polymorphism that length needs, so it only has the monomorphic version of length in its standard-library.

I will suggest a different approach using PureScript, even though it features an even more polymorphic version of length.

I claim that discovering length by looking at its type signature is an inherently flawed approach.

Students aren't good at abstraction - Type checkers are

What if we stopped looking at functions in isolation, and instead defined a context first.

"Write a function which accepts an Array and returns "LONG" if it's longer than 3 or "SHORT" otherwise."

Let's assume the student has already learned about if statements:

measureArray :: forall a. Array a -> String
measureArray array = if ?length array > 3 then "LONG" else "SHORT"

?length here is a typed-hole (which Haskell also supports using a different syntax _length). PureScript's compiler knows how to do more with these typed holes though. If we compile this piece of code the compiler returns the following message:

Error 1 of 1

  Hole 'length' has the inferred type

    Array a0 -> Int

  You could substitute the hole with one of these values:

    Data.Array.length           :: forall a. Array a -> Int
    Data.Foldable.length        :: forall a b f. Foldable f => Semiring b => f a -> b
    Data.Semiring.one           :: forall a. Semiring a => a
    Data.Semiring.zero          :: forall a. Semiring a => a
    Unsafe.Coerce.unsafeCoerce  :: forall a b. a -> b

  in the following context:

    array :: Array a0

in value declaration measureArray

where a0 is a rigid type variable

The compiler finds the length function for us (it sources these definitions from the current project). Importantly there exists a monomorphic version that the less adventurous student can pick and run with. They might still be intrigued to try the more scary looking Data.Foldable.length :: forall a b f. Foldable f => Semiring b => f a -> b but they can't go wrong anymore! The compiler has done the work of working out whether or not the constraints are satisfied. Please take a minute to play around with this feature in PureScript's online playground

This works in a wide variety of situations:

• Log an Array of Strings to the console?

• Attempt to parse a Map of Strings into a Map of Numbers?

A version of this is coming to GHC (https://phabricator.haskell.org/D3361) which will find Data.Array.length, but it won't find Data.Foldable.length yet. If this turns out to be useful to teachers, it might be a great project for a student (Or I will finally bite the bullet and try to contribute to GHC).

In Closing,

I fully agree that it's silly to assume a student can take Data.Traversable.traverse :: forall a b m t. Traversable t => Applicative m => (a -> m b) -> t a -> m (t b) and run with it. But that's approaching the problem wrong in the first place. We don't learn from the abstract towards the concrete. Learning always starts with context and a concrete problem. We just need to use our type checkers not only for checking, but also for querying the knowledge that is our wealth of existing functions.

Links and More

1. The attentive reader might've spotted that this is a weaker version of the proof-search available in dependently typed languages like Idris or Agda, but in my experience the PureScript version is more predictable and less magic, which makes it easier to use, but I'm definitely looking to expand the feature set.

2. I implemented Type-Directed-Search for PureScript during the writing of my bachelors thesis. It describes more of the motivation and implementation here: https://www.dropbox.com/s/vfkgafoo3mofvac/bachelor_arbeit_christoph_hegemann.pdf

Great addition to the discussion! 👍