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. On Tue, Mar 5, 2013 at 3:54 AM, Shachaf Ben-Kiki <[email protected]> wrote: > 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 > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
