Partially Applied Types in Haskell

Question

Based on this question, in this code

data Promise a b =  Pending (a -> b) | Resolved b | Broken

instance Functor (Promise x) where
    fmap f (Pending g) = Pending (f . g)

---

IF

g :: a -> b

then

Pending g :: Promise a b

also

f :: b -> c

because of the existence of f . g.

That means

Pending (f . g) :: Promise a c`.

Wrapping up

fmap :: (b -> c) -> Promise a b -> Promise a c

---

Now fmap alone has this signature (adapted to the above)

fmap :: Functor f => (b -> c) -> f b -> f c

This only conforms if you assume that f = Promise a. While the end product seems reasonable, how do you interpret the type of f or equivalently what it the type of a partially applied promise Promise a?

Answer 1

At the type level you have another programming language, almost-Haskell. In particular, you can view types as having constructors and being able to be partially applied.

To view this a bit more rigorously, we introduce "types of types" called "kinds". For instance, the type constructor Int has kind

Int ::: *

where I write (:::) to read "has kind", though this isn't valid Haskell syntax. Now we also have "partially applied type constructors" like

Maybe ::: * -> *

which has a function type just like you'd expect at the value level.

---

There's one really important concept to the notion of kinds—values may instantiate types only if they are kind *. Or, for example, there exist no values of type Maybe

x :: Maybe
x = -- .... what!

In fact, it's not possible to even express a type of kind other than * anywhere where we'd expect that type to be describing a value.

This leads to a certain kind of restriction in the power of "type level functions" in Haskell in that we can't just universally pass around "unapplied type constructors" since they don't always make much sense. Instead, the whole system is designed such that only sensible types can ever be constructed.

But one place where these "higher kinded types" are allowed to be expressed is in typeclass definitions.

---

If we enable KindSignatures then we can write the kinds of our types directly. One place this shows up is in class definitions. Here's Show

class Show (a :: *) where
  show :: a -> String
  ...

This is totally natural as the occurrences of the type a in the signatures of the methods of Show are of values.

But of course, as you've noted here, Functor is different. If we write out its kind signature we see why

class Functor (f :: * -> *) where
  fmap :: (a -> b) -> f a -> f b

This is a really novel kind of polymorphism, higher-kinded polymorphism, so it takes a minute to get your head all the way around it. What's important to note however is that f only appears in the methods of Functor being applied to some other types a and b. In particular, a class like this would be rejected

class Nope (f :: * -> *) where
  nope :: f -> String

because we told the system that f has kind (* -> *) but we used it as though it could instantiate values, as though it were kind *.

---

Normally, we don't have to use KindSignatures because Haskell can infer the signatures directly. For instance, we could (and in fact do) write

class Functor f where
  fmap :: (a -> b) -> f a -> f b

and Haskell infers that the kind of f must be (* -> *) because it appears applied to a and b. Likewise, we can fail "kind checking" in the same was as we fail type checking if we write something inconsistent. For instance

class NopeNope f where
  fmap :: f -> f a -> a

implies that f has kind * and (* -> *) which is inconsistent.