Type Functions Without Type Functions

Haskell has real, honest to God type functions, which let us write whole simple programs completely at type level. PureScript, sadly, doesn’t have those. But we can write simple type-level programs anyway!

Type Families

Haskell’s type functions (called for confusing historical reasons “type families”) are neat. They look almost as regular term-level functions, but are at type level:

type family F a where
  F Int = String
  F (Maybe a) = [a]
  F a = G a 

We can pattern-match, we can construct types, we can call other type-level functions. We can even do recursion! This is a powerful tool for library design.

PureScript, sadly, does not have type-level functions. But we can do the same things anyway! :-)

Functional Dependencies

PureScript, however, has an almost equally neat thing called “functional dependencies”. They are a way to tell the compiler that, when resolving type class instances, it does not necessarily need to look at all of the type variables, but only a subset of them.

class C a b | a -> b where
  ...

If I define the class with a peculiar a -> b syntax, that’s called a “functional dependency”, where b “depends on” a.

The formal definition says that “b is unambiguously determined by a.”

But in plain terms this means telling the compiler that in order to determine which instance of C to use at any particular place, it needs only to determine what a is, because there can never be two different instances with same a, but different bs.

Well, ok, that’s all fine and high-brow, but what the functor does this have to do with type functions (aka type families)?

Functional Dependencies as Type Functions

Well, let’s look closer.

Say I define a class like this and a couple instances:

class F a b | a -> b
instance f1 :: F Int String
instance f2 :: F Boolean Number

And then, say, I write a function signature like this:

f :: F Int x => Json -> x

What is the return type of this function? Well, it’s x of course, but what exactly is x?

Let’s walk through it. First, the compiler sees the constraint F Int x. Ok, thinks the compiler, now I need to find an instance of class F to use. How can I find this instance? Well, I have the first type, Int. Is that enough? Why yes, of course it’s enough! It so happens that the class F has a functional dependency a -> b, which means that I only need to know a, which I do know — it’s Int — so now I can totally pick the instance! And so it picks the instance F Int String. And guess what? Now it knows that the second variable in F is String, and that means that x is String. So the return value of such function is, in fact, String.

See what happened there? I gave the compiler a type, and it was able to use the definition of class F and its instances to figure out another type. Isn’t that what functions do? You give them an input and they return you an output.

So here, my class F is kinda sorta type-level function. You give it a type as an input, and it “returns” you another type as an output. Neat!

Calling Other Functions

Ok, but how do I call other functions?

Let’s say I want to achieve the equivalent of this Haskell code:

type family G a where
   G Int = String
   G Double = Boolean
type family F a where
   F [a] = G a
   F a = [Int]

Ok, I already know how to define function G:

class G a b | a -> b
instance g1 :: G Int String
instance g2 :: G Double Boolean

But how do I define F? How do I call G from F? Well, I can use a constraint:

class F a b | a -> b
instance f1 :: G a b => F (Array a) b
else instance f2 :: F a (Array Int)

See what happens? When the compiler looks for an instance of F, it matches on Array a as the first type, and it doesn’t, for the moment, care about the second type, because remember: the functional dependency means only the first type is required. So the compiler picks f1 as the instance, and once the instance has been determined, the compiler solves the constraint G a b, which then lets it determine what b is, and thus complete the resolution of F.

Inside Out

One can notice that this all looks rather “inside out” compared to normal function definitions:

• the “pattern match” F (Array a) b is on the right, and the “call” to G is on the left
• input and output are next to each other, looking rather like two fellow arguments
• output always has to be named, can’t just be passed to another function straight away

Here is a more involved example demonstrating a complex type function that calls three others, including one with two arguments:

 TYPE-LEVEL                 |      EQUIVALENT TERM-LEVEL
----------------------------+----------------------------------
                            |
class F a b | a -> b        |     f :: Type -> Type
class G a b | a -> b        |     g :: Type -> Type
class H a b c | a b -> c    |     h :: (Type, Type) -> Type
                            |
class C a b | a -> b        |     c :: Type -> Type
instance c1 ::              |
   ( F a x                  |     let x = F a
   , G x y                  |     let y = G x
   , H a y z                |     let z = H a y
   )                        |
   => C a z                 |     <result is> z

This type function C takes its input a and passes it to another type function F, naming its result x; then passes x to a third function G, naming its result y; then passes the original input a together with intermediate type y to a fourth function H, naming its result z, which then becomes the result of C itself.

And it does get much worse with more complicated type-level programs, which may involve non-Type kinds, rows, higher-order types, etc. Here is a real example from thetypelevel-prelude library:

class RowListRemove (label :: Symbol)
                    (input :: RowList)
                    (output :: RowList)
                    | label input -> output 
instance rowListRemoveNil  
  :: RowListRemove label Nil Nil 
instance rowListRemoveCons
  :: ( RowListRemove label tail tailOutput
     , Symbol.Equals label key eq
     , Boolean.If eq
         (RLProxy tailOutput)
         (RLProxy (Cons key head tailOutput))
         (RLProxy output)
     )
  => RowListRemove label (Cons key head tail) output

So clearly, this technique is not for everyday use, or for the faint of heart. But it is at least possible ;-)