CODEWITHSUNDEEP
haskell
Cristian Garcia
Cristian Garcia

Reputation: 9859

Partially Applied Types in Haskell

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?

Upvotes: 5

Views: 1806

Answers (3)

twitu
twitu

Reputation: 625

I wanted to add to @J. Abrahamson's fantastic answer. A lot of my understanding from Haskell's kind system is from this diogo castro's blog which I highly recommend.

Coming to the question of Partially Applied Types. Apart from type classes it's also possible to use them in type constructors. Taking an example from the blog.

data NonEmpty f a = MkNonEmpty { head :: a, tail :: f a }
:k NonEmpty
-- NonEmpty :: (* -> *) -> * -> *
:t MkNonEmpty { head = (3 :: Int), tail = Maybe 3 }
-- :: NonEmpty Maybe Int

This is an old question so this might be a recent addition to Haskell. It can be summarized as type constructors can take types and type constructors as arguments.

Upvotes: 0

J. Abrahamson
J. Abrahamson

Reputation: 74344

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.

Upvotes: 11

Tobias Brandt
Tobias Brandt

Reputation: 3413

You are only missing the equations for Resolved and Broken. The only reasonable implementation I can think of is

fmap f (Resolved x) = Resolved (f x)
fmap _ Broken = Broken

Other than that, your code is fine.

Upvotes: 0

Related Questions