Haskell type-level lambda calculus error (or lack thereof)

Question

I have been reading the page in the Haskell wiki on type arithmetic and have had a little trouble with the section on the lambda calculus embedded in the type system. From that section, I gathered that the following code should not work with GHC/GHCi - apparently GHC shouldn't be able to determine the type signature of g.

{-# OPTIONS -fglasgow-exts #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}

data X
data App t u
data Lam t

class Subst s t u | s t -> u
instance Subst X u u
instance (Subst s u s', Subst t u t') => Subst (App s t) u (App s' t')
instance Subst (Lam t) u (Lam t)

class Apply s t u | s t -> u
instance (Subst s t u, Eval u u') => Apply (Lam s) t u'

class Eval t u | t -> u
instance Eval X X
instance Eval (Lam t) (Lam t)
instance (Eval s s', Apply s' t u) => Eval (App s t) u

f :: Eval (App (Lam X) X) u => u
f = undefined
g :: Eval (App (Lam (App X X )) (Lam (App X X ))) u => u
g = undefined

Note that I had to add FlexibleContexts and UndecidableInstances, since the given code doesn't seem to compile without these extensions. However, when I run this with GHCi (version 8.0.2), I get the following results:

*Main> :t f
f :: X
*Main> :t g
g :: u

This is especially strange to me, because the type u hasn't been defined anywhere. Is this a result of the two language extensions above interacting with each other and glasgow-exts? If so, how?

Daniel Wagner Daniel Wagner · Accepted Answer · 2017-07-26T02:27:06

The type u is just a lone type variable -- just like the a in undefined :: a.

To really boil this down to its bare essentials, consider this alternate file:

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}

class Loopy a
instance Loopy a => Loopy a

x :: Loopy a => a
x = undefined

If you ask for the type of x in ghci, it will tell you it has type a, with no context. That may seem a bit magical; you simply have to realize that instance resolution in GHC is perfectly well allowed to be recursive, and the implementation goes to great lengths to support this.

We can follow along in detail with what's happening in your example, if you like, but it is very analogous to the above file. Here are the details.

So, we'd like to see if we're allowed to have this instance:

Eval (App (Lam (App X X)) (Lam (App X X))) u

We know

instance (Eval s s', Apply s' t u) => Eval (App s t) u

so we're allowed to have it whenever we have both of these:

Eval (Lam (App X X)) s'
Apply s' (Lam (App X X)) u

The first one is easy, since:

instance Eval (Lam t) (Lam t)

So we're allowed to have our cake when we have:

Apply (Lam (App X X)) (Lam (App X X)) u

Since

instance (Subst s t u, Eval u u') => Apply (Lam s) t u'

to find our cake, we should check under these two rocks:

Subst (App X X) (Lam (App X X)) u
Eval u u'

From

instance (Subst s u s', Subst t u t') => Subst (App s t) u (App s' t')

we learn we can have cake when

Subst X (Lam (App X X)) s'
Subst X (Lam (App X X)) t'
Eval (App s' t') u'

which is easy to make progress on, since:

instance Subst X u u

Therefore, we can have our original instance whenever:

Eval (App (Lam (App X X)) (Lam (App X X))) u'

But, hey presto! This is the original instance we were looking for. So in summary we can have our original instance whenever we can have our original instance. So we declare that we can have our original instance, and then we can have our original instance! Isn't that peachy.

Haskell type-level lambda calculus error (or lack thereof)

1 Answers