Computing with Impossible Types

Edward Kmett recently posted a puzzling gist seemingly showing that at the type level, the () kind has more than one inhabitant. The goal of this post is to explain what's going on.

Stuck Type Expressions

Here is a simple type family.

{-# LANGUAGE TypeFamilies, UndecidableInstances #-}

type family F a where
  F (Maybe a) = [F a]
  F a         = a

Since F (Maybe Int) and [F Int] both evaluate to [Int], the following type-checks.

-- |
-- >>> :kind! F (Maybe Int) -> [F Int]
-- F (Maybe Int) -> [F Int] :: *
-- = [Int] -> [Int]
runFMaybeInt :: F (Maybe Int) -> [F Int]
runFMaybeInt = id

We didn't use any Int-specific code, so let's make the type more polymorphic.

-- |
-- >>> :set -XRankNTypes
-- >>> :kind! forall b. F (Maybe b) -> [F b]
-- forall b. F (Maybe b) -> [F b] :: *
-- = [F b] -> [F b]
runFMaybe :: Proxy b -> F (Maybe b) -> [F b]
runFMaybe _ = id

Notice that F (Maybe b) and [F b] both evaluate to [F b], not to [b]! That's because we don't yet know whether b is going to be instantiated with a Maybe something or not, so unlike F Int, the type expression F b cannot be simplified further. The evaluation of F b is stuck, and will remain so until we learn more information about b. The code still type-checks though, because even though we don't know which concrete type F b will expand to, we do know that [F b] and [F b] will expand to the same type because they are the same type expression.

Pattern-Matching on the Shape

Here is another type family.

type family G a where
  G (f a) = [G a]
  G a     = Double

This time, the type family isn't pattern-matching on whether or not its input type is a Maybe something, but on whether or not it is a type which, like Maybe Int, consists of a type constructor applied to a type. Let's look at a concrete example:

-- |
-- >>> :kind! G (Maybe Int) -> [G Int]
-- G (Maybe Int) -> [G Int] :: *
-- = [Double] -> [Double]
runGMaybeInt :: G (Maybe Int) -> [G Int]
runGMaybeInt = id

No surprises there. Let's make the type more polymorphic:

-- |
-- >>> :kind! forall g b. G (g b) -> [G b]
-- forall g b. G (g b) -> [G b] :: *
-- = [G b] -> [G b]
runGMaybe :: Proxy (g b) -> G (g b) -> [G b]
runGMaybe _ = id

As before, the type expression G b is stuck because we don't yet know whether b is going to be instantiated to a type with the right shape such as Maybe Int, or to a type with a different shape such as Int. But regardless of which one it is, [G b] and [G b] will both expand to the same type, so the implementation type-checks.

One last example:

>>> :kind! forall b. G (G b) -> [G b]
forall b. G (G b) -> [G b] :: *
= G (G b) -> [G b]

Note that G (G b) did not simplify! G b might look like it has the right shape to match g b, but it doesn't, because G is a type family, not a type constructor. It's a good thing it doesn't match, because if it did, evaluating type expressions like G (G Int) wouldn't be confluent! If we evaluate the outer application first, we get [G Int] and then [Double], whereas if we evaluate the inner application first, we get G Double and then Double.

To be clear, evaluating the outer application first doesn't work because we don't yet know whether the type expression G Int will evaluate to something of the form f a or not. So the inner application is evaluated first, and G (G Int) evaluates to Double.

Two Arrow-Like Kinds

G and Maybe both seem to have kind * -> *:

>>> :kind! G
G :: * -> *
>>> :kind! Maybe
Maybe :: * -> *

But that's misleading, because there are some circumstances in which a type of kind * -> * is expected but only Maybe will be accepted:

class MyMonad (m :: * -> *)

-- ok
instance MyMonad Maybe

-- error: The type family ‘G’ should have 1 argument,
--        but has been given none
instance MyMonad G

And there are other circumstances in which both G and Maybe will be accepted:

{-# LANGUAGE DataKinds, TypeOperators #-}

-- |
-- >>> :kind! FMap Maybe '[Int, Double]
-- FMap Maybe '[Int, Double] :: [*]
-- = '[Maybe Int, Maybe Double]
--
-- >>> :kind! FMap G '[Int, Double]
-- FMap G '[Int, Double] :: [*]
-- = '[Double, Double]
type family FMap (f :: * -> *) as where
  FMap f '[]       = '[]
  FMap f (a ': as) = (f a ': FMap f as)

So I prefer to pretend that there are two different arrow-like kind constructors:

1. (-->) for type functions which can be applied to a type argument. G and Maybe both have kind * --> *. Just like it isn't possible to pattern-match on a type variable, it is not possible to pattern-match on a type expression whose head is a (-->), we must instead apply the type function and pattern-match on the result.
2. (->) for type constructors which can be pattern-matched on. Maybe has kind * -> *, but G does not. Clearly, (->) is a subtype of (-->).

Now we can make sense of the previous examples. Instance resolution works by pattern-matching on types, so MyMonad expects a * -> *, not a * --> *. Since G has the wrong kind, it cannot be given a MyMonad instance. FMap, on the other hand, only needs to apply its f to various as, so it expects an * --> * such as G. Since * -> * is a subtype of * --> *, FMap can also be applied to Maybe.

edit:
Apparently :kind! is misleading here. Outside of :kind!, FMap accepts Maybe but not G. So the situation is simpler than I thought: (-->) is for type families, (->) is for type constructors, and those are completely different arrow kinds, there is no subtyping relationship between the two. There is no way to ask for an argument of kind * --> *, because if we try to pass an "unsaturated" argument with that kind, G for example, GHC will complain that G is missing arguments. So MyMonad and FMap both expect an argument of kind * -> *, not * --> *.

Unusual Type Families

Here are a few surprising, yet legal type families.

-- |
-- >>> :kind! H1 ('Just '())
-- H1 ('Just '()) :: * -> *
-- = Maybe
type family H1 (a :: Maybe ()) :: * -> * where
  H1 ('Just a) = Maybe
  H1 'Nothing  = IO

H1's input has kind Maybe (), not *, and its output has kind * -> *, not *. Note that it's really * -> *, not * --> *, so G is not a valid output. Overall, the kind of H1 is thus Maybe () --> * -> *.

-- |
-- >>> :kind! H2
-- H2 :: *
-- = Int
type family H2 where
  H2 = Int

H2 has no type parameters, so it's kind is *, not * --> *. If it returned Maybe instead of Int, its kind would be * -> * instead. A type family's kind can be either * --> * or * -> * depending on how it's defined, so it's not as simple as "type constructors use (->), type families use (-->)".

Combining both ideas together:

type family J :: () -> Maybe () where
  J = 'Just

J's kind is () -> Maybe (), so it has to return a type constructor which accepts a type of kind () and produces a type of kind Maybe (). There are only two types which have the kind Maybe (): the type 'Nothing, and the type 'Just '(). 'Nothing has the wrong kind, since it doesn't accept a type of kind (), but 'Just is just right.

One last complication:

-- |
-- >>> :kind! H3 Int
-- H3 Int :: *
-- = H3 Int
type family H3 a where

H3 has no equations defining what happens when it is applied to a type argument. As a result, the type expression H3 Int remains stuck even though it doesn't contain any type variables.

Combining everything together:

type family Succ :: () -> () where

Succ pretends that it can produce a type constructor which accepts a type of kind () and produces a type of kind (). This is ridiculous! We know that '() is the only type of kind (), and like 'Nothing, it has the wrong kind because it doesn't accept a type of kind (). There are no valid types which Succ could return, so unsurprisingly it has no equations, and so Succ is a type expression which always remains stuck.

Ignoring Impossible Types

The type expression Succ '() is stuck, but well-kinded. It has kind ().

That's the kind which 'Just :: () -> Maybe () expects. Thus, 'Just (Succ '()) is also stuck and well-kinded. It has kind Maybe ().

That's the kind which our H1 :: Maybe () --> * -> * type family from earlier expects. Is H1 ('Just (Succ '())) stuck as well?

>>> :kind! H1 ('Just (Succ '()))
H1 ('Just (Succ '())) :: * -> *
= Maybe

Not stuck! That's because H1 ignores the part which is stuck. Its pattern is ('Just a), so it pattern-matches on the 'Just constructor, but it ignores its argument. If its pattern was ('Just '()) instead, it would have been stuck.

Here comes the clever part: it is possible to write a type family which pattern-matches on the '() but ignores the stuck Succ part.

-- |
-- >>> :kind! IsSucc (Succ '())
-- IsSucc (Succ '()) :: Bool
-- = 'True
--
-- >>> :kind! IsSucc '()
-- IsSucc '() :: Bool
-- = 'False
type family IsSucc (a :: ()) :: Bool where
  IsSucc (succ '()) = 'True
  IsSucc '()        = 'False

The trick is to do like G and pattern-match on the shape, not the contents.

Computing with Impossible Types

It is also possible to distinguish the two inhabitants using a typeclass instead of a type family:

{-# language FlexibleInstances #-}
import Data.Proxy

-- |
-- >>> isSucc (Proxy :: Proxy (Succ '()))
-- True
-- >>> isSucc (Proxy :: Proxy '())
-- False
class IsSucc (a :: ()) where
  isSucc :: Proxy a -> Bool

instance IsSucc (succ '()) where
  isSucc _ = True

instance IsSucc '() where
  isSucc _ = False

The fact that this works is surprising, because () is supposed to be a closed kind with only one inhabitant, '(), and yet here we seemingly have a second inhabitant, Succ '(), which can be distinguished from '() even though it is stuck. And as you might surmise from its name, we can manufacture many more inhabitants: Succ (Succ '()), Succ (Succ (Succ '())), etc.

{-# language ScopedTypeVariables #-}

-- |
-- >>> countSuccs (Proxy :: Proxy '())
-- 0
-- >>> countSuccs (Proxy :: Proxy (Succ '()))
-- 1
-- >>> countSuccs (Proxy :: Proxy (Succ (Succ (Succ '()))))
-- 3
class CountSuccs (a :: ()) where
  countSuccs :: Proxy a -> Int

instance CountSuccs '() where
  countSuccs _ = 0

instance CountSuccs a => CountSuccs (succ a) where
  countSuccs _ = 1 + countSuccs (Proxy :: Proxy a)

Those examples show how to compute booleans and integers from a stuck type expression containing Succs. Using polymorphic recursion, it is also possible to go the other way, from an integer to a stuck type expression containing that many Succs:

{-# language RankNTypes #-}

-- |
-- >>> mkSuccs 42 countSuccs
-- 42
mkSuccs :: Int -> (forall a. CountSuccs a => Proxy a -> r) -> r
mkSuccs 0 cc = cc (Proxy :: Proxy '())
mkSuccs n cc = mkSuccs (n - 1) $ \(Proxy :: Proxy a)
            -> cc (Proxy :: Proxy (Succ a))

Since Haskell doesn't have dependent types, the output type is independent of the integer, so we cannot directly return the stuck type as an output. Instead, we use continuation-passing-style to accept a polymorphic continuation which produces an r regardless of which stuck type we instantiate it at.

When we use countSuccs as the continuation, this r is an integer, and the integer it computes is the number of Succs. So we start with n, we convert it to a stuck type containing n Succs, and then we count those Succs and get n back. This is a very simple example of a computation which relies on the existence of those seemingly-impossible non-'() inhabitants of () in order to compute its result: if there was only one type of kind (), the integer would be lost during the conversion to Proxy (a :: ()), and we would not be able to get that same integer back at the end.

Full Circle

Now that we have seen and understood each of the pieces individually, we are now ready to marvel at Kmett's creation:

{-# language PolyKinds #-}

import Data.Proxy

class KnownUnit (k :: ()) where
   reflect :: Proxy k -> Int

instance KnownUnit '() where
  reflect _ = 0

instance KnownUnit x => KnownUnit (f x) where
  reflect _ = 1 + reflect (Proxy :: Proxy x)

type family Succ :: k -> k

-- |
-- >>> reify 23 reflect
-- 23
reify :: Int -> (forall k. KnownUnit k => Proxy k -> r) -> r
reify 0 f = f (Proxy :: Proxy '())
reify n f = reify (n - 1) $ \(Proxy :: Proxy k)
         -> f (Proxy :: Proxy (Succ k))

Neat!

...or worrisome?

Accepting Impossible Types

We Haskellers like to use precise types in order to make illegal states unrepresentable. We accept, reluctantly, that ⊥ inhabits all types, so () doesn't really have exactly one possible value. But it does have exactly one possible total value, and if we write a function whose type signature expects a (), that's the value which this function expects to receive. And so, most functions don't document what their behaviour is on ⊥ inputs, and nobody complains, because they know they're not supposed to use ⊥ inputs.

DataKinds allows us to use precise kinds, and thus to make illegal types unrepresentable. We don't often think about them, but stuck type expressions also inhabit all kinds, so there isn't really only one type of kind (). Today we saw that some of those extra inhabitants are really weird. That's an interesting quirk of Haskell's type system, but ultimately, I don't think those weird inhabitants are any more worrisome than their less exotic cousins, the stuck type expressions which contain type variables. After all, there is only one total type of kind (), and when we write a type-level function (or an instance) which expects a (), that's the type we expect.