This page summarizes discussions of the inconsistency arising from the combination of impredicativity, the case analysis on types, and some sort of injectivity of type constructors. System F and System Fw permit impredicative polymorphism and yet are strongly normalizing. Adding the type case analysis and some sort of injectivity of type constructors destroys even the weak normalizability. Without any value- or type-level recursion, we write a non-normalizable term that proves
False
, by encoding Russell
paradox.Matthieu Sozeau has started the discussion on Haskell Cafe on January 27, 2010, describing the divergence in the type checker encountered while encoding a recently found Coq paradox in Haskell, using GADTs and Rank2Types. The follow-up messages have distilled the problem, which turns out different from the one on Coq and Agda. This web page, expanding on the message posted on January 30, 2010, explains the technique of systematically deriving absurd terms and demonstrates it on three examples of type case analysis, with GADTs and with type families. I thank Dan Doel, Daniel Fischer and Martin Sulzmann for their comments during the January 2010 discussion. I am very grateful to Stephanie Weirich for further discussions and especially for her explanations of injectivity in System FC.
absurd
with GADTsabsurd
with standard injectivityabsurd
with data familiesabsurd
with type families
A definition is predicative if it is not circular. An impredicative
definition, in contrast, indirectly refers to the object being defined by
quantifying over the domain that includes the object. Here is an example of
a predicative Haskell definition of the type P
, and of a sample term
prd
of that type:
type P = forall a. a -> [a] prd :: P prd x = [x]The type
P
is polymorphic; the quantified variable a
(implicitly) ranges over non-polymorphic types (monotypes) and therefore
cannot be instantiated with P
. For that reason we cannot
apply prd
to itself. The apparent self-application intprd1 = case prd prd of [f] -> f Trueis illusory: we apply the polymorphic function
prd
not to itself
but to an instance of itself. Therefore, the following definition
is ill-typed:tprd2 = case prd prd of [f] -> (f True, f 'a') Error: Couldn't match expected type `Bool' with actual type `Char'
Haskell also permits impredicative definitions, like the following:
newtype I = I{unI :: forall a. a -> [a]} imprd :: I imprd = I (\x -> [x]) tim = case unI imprd imprd of [I f] -> (f True, f 'a')The type
I
is a monotype and so the quantified type variable a
in I
's definition can be instantiated with I
itself. The well-typed
term tim
demonstrates exactly such an instantiation.
Injectivity of type constructors means that a type constructor
T
(defined by a data
declaration) gives
distinct types when applied to distinct arguments. Contrapositively:
T a ~ T b implies a ~ bwhere
~
is the symbol for type equality in Haskell. For example, if two
lists have the same type, their elements have the same type.Haskell has type functions that do the case analysis on types, extracting their components. Such type functions can be implemented via functional dependencies, GADTs, type or data families. The type family below
type family Elem x :: * type instance Elem [a] = a type instance Elem (Maybe a) = a
extracts the element type from the list or the option type.
Incidentally, Elem
is non-injective: it maps distinct types
[Int]
and Maybe Int
to the same result Int
.
absurd
with GADTsFalse
. For the sake of
explanation, we rely here on a stronger property than injectivity,
namely, System FC's Fst
, which is available in some versions of
GHC. The next section adjusts the derivation to use just the standard
injectivity. Let us first see the result, the complete code for the well-typed
but divergent term absurd
defined without either value or type
recursion.{-# LANGUAGE GADTs, KindSignatures, EmptyDataDecls #-} data False -- No constructors data R :: * -> * where MkR :: (c (c ()) -> False) -> R (c ()) cond_false :: R (R ()) -> False cond_false x@(MkR f) = f x -- May cause divergence in the type checker absurd :: False absurd = cond_false (MkR cond_false) absurd2 :: False absurd2 = let x = MkR cond_false in cond_false xThe term
absurd
may cause the infinite loop in the type checker in
old versions of GHC. The term absurd2
, re-written to thwart aggressive
inlining, is more widely acceptable. The code works with versions of
GHC before 7.4, and may start working again with GHC 7.8.The code was derived as follows. Our goal is to encode Russell paradox by defining a recursive (rather than a mere inductive) data type, such as
data R = MkR (R -> False)The type
R -> False
can be regarded as the negation of R
. The
value of R
then carries the proof of its own non-existence. From a
different point of view, a recursive data type such as R
lets us
express the fixpoint combinator, and hence attain the logical
inconsistency. The above definition of R
however relies on the
type-level recursion, which we want to avoid. We break the recursive
knot, by parameterizing R
:data R c = MkR (c -> False)We hope to instantiate the type variable
c
with R
and
recover the desired recursive type. Impredicativity, defining
the class of types R c
in terms of the class of all types,
which includes R c
itself, is crucial. However, we cannot
instantiate c
with R
since the two have different kinds:
c
has the kind *
and R
is the type constructor, of
the kind *->*
. A naive work-arounddata R c = MkR (c () -> False)fails: although
c
now has the kind *->*
, R
has the kind
(*->*)->*
and not substitutable for c. With the ordinary data types,
we are stuck -- for exactly the same reason that self-application is
not expressible in simply-typed lambda-calculus. Impredicativity per se
does not lead to inconsistency.GADTs come to the rescue, giving us the needed `phase shift'. In the raw GADT notation,
data R c' = c' ~ c () => MkR (c () -> False)Now
c'
, conditioned to be of the form c ()
, is of the kind *
.
The type variable c
is of the kind *->*
; R
is of the same kind
and so is substitutable for c
. Thus the data type instance R (R ())
(when c'
is instantiated with R ()
and c
becomes R
)
has the value MkR (R () -> False)
. That is not quite the paradox:
the value of the type R (R ())
carries the negation of just R ()
.
But the mismatch is easy to fix:data R c' = c' ~ c () => MkR (c (c ()) -> False)Instantiating
c
with R
and noting that R (R ())
coincides with
R c'
when c'
is R ()
give us the desired vicious circle.
In the definition of cond_false
, the argument x
must have the type R (c ())
because it is constructed by the data
constructor MkR
. On the other hand, the type signature of cond_false
ascribes to x
the type R (R ())
. We obtain the equation
R (R ()) ~ R (c ())
, which the injectivity of R
simplifies
to R () ~ c ()
.
To proceed further, we need the System FC property called Fst
:
a x ~ b y
entails a ~ b
, which gives the desired instantiation
R ~ c
. The property Fst
was removed from GHC 7.4, but is reportedly
on its way back. The example will work again then. The error message
by GHC 7.4 is quite informative, validating our analysis:
Could not deduce (c ~ R) from the context (R () ~ c ()) bound by a pattern with constructor MkR :: forall (c :: * -> *). (c (c ()) -> False) -> R (c ()), in an equation for `cond_false'
absurd
with standard injectivityabsurd
term that
witnesses False
using injectivity and the property
Fst
. This section removes the dependence on Fst
. The adjusted code
compiles with any recent version of GHC. Further, Stephanie Weirich showed
that the example can be translated to Coq, with injectivity added
as an axiom.
Recall Fst
means a x ~ b y
entails a ~ b
whereas the weaker,
standard injectivity (which could be called Snd
or Nth
) leads
from T a ~ T b
to a ~ b
. We relied on Fst
to get c ~ R
from c () ~ R ()
. To avoid Fst
and use only injectivity, we need
to ``shift'' c
into the argument position -- for example, replace
c ()
with J c
for some injective type constructor J
. As usual,
the hardest part was stating exactly what we want. Getting it is easy: here
is the complete code.
{-# LANGUAGE GADTs, KindSignatures, EmptyDataDecls #-} data False -- No constructors data J c = J (c ()) data R :: * -> * where MkR :: (c (J c) -> False) -> R (J c) cond_false :: R (J R) -> False cond_false x@(MkR f) = f x absurd :: False absurd = cond_false (MkR cond_false)
In the definition cond_false
, the argument x
must have the type
R (J c)
since it is constructed by MkR
. The ascription of the signature
R (J R)
gives the equality R (J c) ~ R (J R)
, from which we obtain
the desired c ~ R
after two applications of injectivity. Stephanie Weirich
has pointed out that the System FC term for cond_false
in the
output of the GHC simplifier indeed shows two applications of
injectivity-induced coercions (called Nth
).
With Ex Falso Quodlibet, the example can be made more absurd:
{-# LANGUAGE GADTs, KindSignatures #-} data J c = J (c ()) data R :: * -> * -> * where MkR :: (c (J c) -> a) -> R a (J c) cond_false :: R a (J (R a)) -> a cond_false x@(MkR f) = f x absurd :: a absurd = cond_false (MkR cond_false)Truly, every type is populated, and
absurd
is the evidence of it.absurd
with data families{-# LANGUAGE TypeFamilies, EmptyDataDecls #-} data False -- No constructors data J c = J (c ()) data family R c data instance R (J c) = MkR (c (J c) -> False) cond_false :: R (J R) -> False cond_false x@(MkR f) = f x absurd :: False absurd = cond_false (MkR cond_false)
absurd
with type families{-# LANGUAGE TypeFamilies, EmptyDataDecls #-} data False -- No constructors data J c = J (c ()) type family Interpret t :: * type instance Interpret (J c) = c (J c) data R c = MkR (Interpret c -> False) cond_false :: R (J R) -> False cond_false x@(MkR f) = f x absurd :: False absurd = cond_false (MkR cond_false)
As an explanation, let us build the type derivation for False
,
noting where impredicativity, injectivity and type case analysis
come into play. The pattern
x@(MkR f)
in the definition of cond_false
gives the following
type assignments, where a
is a not yet determined type:
x :: R a f :: Interpret a -> FalseThe definition of the class of data types
R c
is impredicative since c
ranges over all
types and can be instantiated with a member of the R
class itself.
The type signature of cond_false
and the term
MkR cond_false
make such an instantiation. The signature
of cond_false
, which ascribes to x
the type R (J R)
, gives
the equality R a ~ R (J R)
. The injectivity of the type constructor R
turns the equality to a ~ J R
. Substituting J R
for a
in the
type of f
gives rise to Interpret (J R)
, which fits the
type family instance and hence improves to R (J R)
. The improvement
had to deconstruct the type J R
and extract its component.
After the improvement, the argument type of f
matches the type of
x
and the type checking of cond_false
succeeds. In
absurd
, the argument type of cond_false
requires that
MkR cond_false
be of the type R (J R)
, yielding by injectivity,
the instantiation of c
to J R
. After applying the type family instance,
the type checker concludes that MkR cond_false
, and absurd
are
well-typed.oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML