Shachaf Ben-Kiki | 5 Mar 09:54 2013

Haskell + RankNTypes + (forall p. p Char -> p Bool) sound?

I was trying to figure out a way to write absurd :: (forall p. p Char
-> p Bool) -> Void using only rank-n types. Someone suggested that
Haskell with RankNTypes and a magic primitive of type (forall p. p
Char -> p Bool) might be sound (disregarding the normal ways to get ⊥,
of course).

Is that true? Given either TypeFamilies or GADTs, you can write
absurd. But it doesn't seem like you can write it with just
RankNTypes. (This is related to GeneralizedNewtypeDeriving, which is
more or less a version of that magic primitive.)

This seems like something that GADTs (/TypeFamilies) give you over
Leibniz equality: You can write

  data Foo a where
    FooA :: Foo Char
    FooB :: Void -> Foo Bool

  foo :: Foo Bool -> Void
  foo (FooB x) = x

Without any warnings. On the other hand

  data Bar a = BarA (Is a Char) | BarB (Is a Bool) Void

  bar :: Bar Bool -> Void
  bar (BarB _ x) = x
  bar (BarA w) = -- ???

Doesn't seem possible. If it's indeed impossible, what's the minimal
(Continue reading)

Dan Doel | 5 Mar 16:15 2013

Re: Haskell + RankNTypes + (forall p. p Char -> p Bool) sound?

Just because you can't use the 'magic primitive' in question to
produce an element of the empty type doesn't mean the system is sound
(nor does type soundness have anything to do with proving 'false').

The question is what the primitive is supposed to do. If it's supposed
to work as a witness of equality between Char and Bool, then (sym prim
. prim :: p Char -> p Char) must be refl, the identity function. But
then if we choose p = Identity, we have f :: Char -> Char via
round-trip through Bool that must be the identity. In a sufficiently
capable language, that can be shown impossible via the pigeonhole
principle, but I'm not sure if 'just rank-n types' is up to the task.

Some other food for thought is that 'true = false' (true and false
beeing booleans) is not sufficient to derive false in dependent type
theory _unless_ there is some kind of large elimination, either
directly or via universes. Without those, type theory admits trivial
models in which every type denotes a set of at most one element. One
can see then that it might take the ability to do case analysis on
types to gain a contradiction from 'Char = Bool' in GHC (the
pigeonhole route doesn't seem like it'd be feasible), although I don't
know that that's the case.

Anyhow, soundness is with respect to a model. In the usual model of
Haskell, every domain is nonempty, including the one for p Char -> p
Bool. So if you don't specify anything about the primitive, it could
be undefined, and there'd be no problem with type soundness. And it
may also be the case that you can introduce a primitive that is not
parametric in p, and arbitrarily applies functions f :: Char -> Bool,
g :: Bool -> Char in the right places for each particular p definable
in the language. That will fail the properties of an equality witness,
(Continue reading)