Higher Kinded Types in PureScript

We’ve seen how we can create simple types in Purescript. PureScripts allows us to take these types even further. We can have types that can take parameters that allow us to create new types.

For example, in the previous post we had the Planet type :

data Planet = Mars | Neptune | Uranus

Supposing we then had the requirement to represent no planet at all. After all, some aliens just roam around the Galaxy without coming from any particular planet. We could just add NoPlanet to the available options :

data Planet = Mars | Neptune | Uranus | NoPlanet

That would capture the requirement, but it doesn’t really fully capture the sematics. NoPlanet is really its own concept that is distinct from the other planets. Really, we want something more like :

data Planet = Mars | Neptune | Uranus
data Home 
    = NoPlanet
    | SomePlanet Planet
    
data Customer = Human String String
              | Alien Home String String String 
 
    
let onkonk = Alien (SomePlanet Mars) "Onk" "Onk" "Gonk"

This pattern we something is either a concrete value or nothing is found all over the place. So Purescript has given us the Maybe type to encapsulate the concept.

data Maybe a 
    = Nothing 
    | Just a

Note the a in Maybe a. We can replace this with any type we need. So we can represent our planets as a Maybe Planet.

data Customer = Human String String
              | Alien (Maybe Planet) String String String 
 
    
let onkonk = Alien (Just Mars) "Onk" "Onk" "Gonk"
let roameroftheuniverse = Alien Nothing "Orkle" "Wanderer" "Erk"

Technically Maybe is not a type, it is a type constructor. We can’t do anything concrete with just a Maybe, we need to know what the a is. Maybe Planet is a concrete type that we can use. Very similar to a function which, for example may have a type toString :: Int -> String, Maybe has what is known as a kind of Type -> Type. As we can see in the Repl :

> import Data.Maybe
> :kind Maybe
Type -> Type
> :kind Maybe Int
Type

Why is this at all useful?

If you find yourself writing the same code everywhere, it is often helpful to be able to extract this code out into it’s own function. Then rather than duplicating the code you can just call this function instead. This makes your code easier to maintain and understand. Higher kinded types takes this concept and brings it to the type level.

Now it is possible to take patterns that we find in our types and abstract them into their own Type constructors. It is then possible to write code that runs against these higher kinded types and we can share amongst any of the concrete instances instances in our code.

So for example, supposing we were displaying an input field in Halogen. We wanted to display an error message if the value is not filled in. We could write something like :

    displayPlanetError :: Maybe Planet -> H.ComponentHTML Action () m
    displayPlanetError planet = case planet of
                                   Just _ -> HH.text "All good"
                                   Nothing -> HH.text "Error: invalid value"
    
    displayRocketError :: Maybe Rocket -> H.ComponentHTML Action () m
    displayRocketError rocket :: = case rocket of
                                     Just _ -> HH.text "All good"
                                     Nothing -> HH.text "Error: invalid value"

But of course there is a lot of duplicate code there. Since both are working with Maybe a we can extract this out into a single function :

    displayError :: forall a . Maybe a -> H.ComponentHTML Action () m
    displayError maybe = case maybe of
                            Just _ -> HH.text "All good"
                            Nothing -> HH.text "Error: invalid value"

Note the forall a . in the function type declaration. It means what it says, for all values of Type a, our parameter is a Maybe of that type. (Technically there should also be a forall m in the definition too, but I’ve just dropped it to emphasise the a here..)

Higher kinded types are used all over the place in Purescript and its constant search for more succinct levels of abstraction, so it’s well worth getting comfortable with them.

At the minute there isn’t much we can do with the a from the previous example. We need to explore Type Classes in order to make the most of our higher kinded types.