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

[Shachaf Ben-Kiki]

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
extension you would need to add on top of RankNTypes to make it work?
GADTs seems way too big.

Shachaf

_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Dan Doel]

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,
but if you don't specify any properties at all, anything goes (and you
can't really prove anything about the action of Leibniz or any other
equality in GHC anyhow, so it can't contradict anything there).

i don't really know the answer to whether TypeFamilies/GADTs is merely
sufficient or necessary, though.