Injective type formers are inconsistent

[catalin-hritcu]

F* unfortunately still includes injective type formers, although these are known to be inconsistent (and anti-classical). I've ported an inconsistency proof from Lean (https://gist.github.com/leodemoura/0c88341bb585bf9a72e6) to paradoxes/InjectiveTypeFormers.fst.

[catalin-hritcu]

Wednesday, September 9, 2015
[12:07:45 AM] Nikhil Swamy: my longstanding plan for addressing this injectivity issue was to admit it to Z3 for only types indexed by zero-order types and terms. I.e., things of kind (Type -> Type) etc. not (Type -> Type) -> Type
[12:07:58 AM] Nikhil Swamy: losing injectivity for things like ref and list would be a big pain
[12:08:27 AM] Nikhil Swamy: whether we can prove consistency in the presence of this more limited injectivity remains an open question
[12:08:51 AM] Catalin Hritcu: something we could look at in the context of the proof

One thing I don't yet understand is where injectivity of type constructors is exactly assumed in our logical encoding. Looking at the generated smt file wasn't able to find it and I would like to play a bit with this ... e.g. to see what exactly would break if we completely removed it.

All I could find so far is this (in encode.fs):

    let mk_ref : string -> term -> decls_t = fun reft_name _ ->
        let r = ("r", Ref_sort) in
        let aa = ("a", Type_sort) in
        let bb = ("b", Type_sort) in
        let refa = Term.mkApp(reft_name, [mkFreeV aa]) in
        let refb = Term.mkApp(reft_name, [mkFreeV bb]) in
        let typing_pred = Term.mk_HasType x refa in
        let typing_pred_b = Term.mk_HasType x refb in
        [Term.Assume(mkForall_fuel([typing_pred], [xx;aa], mkImp(typing_pred, Term.mk_tester "BoxRef" x)), Some "ref inversion");
         Term.Assume(mkForall_fuel' 2 ([typing_pred; typing_pred_b], [xx;aa;bb], mkImp(mkAnd(typing_pred, typing_pred_b), mkEq(mkFreeV aa, mkFreeV bb))), Some "ref typing is injective")] in

but it seems just for refs ... right?

[catalin-hritcu]

This is currently rejected by the "only Type0" cardinality check, but it will go through with universes.

[mtzguido]

I believe this is a consequence of having a projection operator for type constructors (so, I x = I y ==> I_f (I x) = I_f (I y) ==> x = y). Seems that both data and type constructors are encoded via the same function (constructor_to_decl) which introduces the projector.

Could a fix be only generating such projector for data constructors and not for type constructors? A small test shows that lib/ still typechecks and a big part of examples/ too (not quite sure of the reason it doesn't fully work, I can look but I wanted to check that this is sound first). Obviously, the paradox doesn't typecheck after the change.

[mtzguido]

Looking more closely, it all still breaks down as soon as we type a term with I x. Inversion gives us that it's of the form Mk z with z = x, but since it also has type I y, the same applies for y and then x = y. The paradox still holds after a small tweak.

So it's a consequence of unrestricted inversion and "typing elimination". As Nik suggested, maybe typing elimination should be restricted to lower-kinded types?

[catalin-hritcu]

We tried this in Coq and it indeed seems to be the fault of "typing elimination". In this case typing elimination gives us heterogenous injectivity of Mk, from which we can obtain type constructor injectivity:

Inductive I : (Type -> Type) -> Type :=
  | Mk : forall f:(Type->Type), I f.

Axiom typing_elim : forall a e (x:I a), JMeq x (Mk e) -> e = a.

(* Alternative way of writing this, injectivity for JMeq/Mk:
Axiom typing_elim : forall l r, JMeq (Mk l) (Mk r) -> l = r. *)

Lemma injI' : forall (x:Type->Type) (y:Type->Type) (ex : I x), I x = I y -> x = y.
Proof.
  intros x y ex H.
  assert(X : exists ey : I y, JMeq ex ey). rewrite <- H. now eauto. clear H.
  destruct X as [ey Hexy].
  destruct ex as [ex'].
  destruct ey as [ey'].
  now apply typing_elim in Hexy.
Qed.

So the second fix to this implies restricting "typing elimination". @nikswamy should we start thinking about how to fix these things? :)

[nikswamy]

My default plan was to exclude the problematic injectivity axiom in the Z3 encoding for --universes. But, if you have a better solution by restricting elimination somehow, then sure let's "start thinking about" it. Looks like you guys have already made a nice start, actually : )

[catalin-hritcu]

Unfortunately, there is no injectivity axiom directly assumed in the Z3 encoding (or at least we couldn't find any). Instead, there are at least two "features" of the encoding, each of which allows Z3 to prove injectivity: (1) projection operators for type constructors (#349 (comment)), and (2) unrestricted "typing elimination" (#349 (comment)). We can probably just remove (1) from the encoding without breaking much, but we don't yet have a good fix for (2).

[nikswamy]

We encode all injectivity properties using projectors. So, I see the projection operator for type constructors as the injectivity axiom.

Let's talk ...

[catalin-hritcu]

Here is the original source of this paradox:
https://lists.chalmers.se/pipermail/agda/2010/001526.html

[catalin-hritcu]

For anyone wondering about status, here it goes:

Are injective type formers gone now? The following now fails as it should:

val injI : x:(Type->Type) -> y:(Type->Type) ->
           Lemma (requires (i x == i y)) (ensures (x == y))
let injI (x:Type->Type) (y:Type->Type) = ()

error is

./InjectiveTypeFormers.fst(17,50-17,58): (Error) could not prove post-condition

nik [1 hour ago]
I've made several attempts to remove them. But they are not completely gone

nik [45 minutes ago]
i'd like to reevaluate where we stand currently.

nik [44 minutes ago]
my most recent attempt: https://github.com/FStarLang/FStar/tree/nik_attemping_349 (edited)

nik [44 minutes ago]
is incomplete

catalin [43 minutes ago]
so any idea why the above code fails on master?

nik [3 minutes ago]
i removed some uses of injectivity but not all

[nikswamy]

@aseemr and I came upon this issue again today.

For a year or more now, we no longer encode projectors for type formers. That's good.

But, we still provide equalities between the parameters and indices of an inductive type and the arguments of their data constructors.

E.g.,

Given this,

type vector (a:Type) : nat -> Type =
| Nil : vector a 0
| Cons: hd:a -> n:nat -> vector a n -> vector a (n + 1)

we get:

forall x a n. HasType x (vector a n) ==>
   (Nil? x /\  Nil?.a x == a /\ n == 0) \/
   (Cons? x /\  Cons?.a x == a /\ Cons?.n x + 1 == n)

The inversion axiom has two parts:

1. A case analysis of the constructors (Nil?, Cons?), which is uncontroversial
2. Equalities that relate the arguments of the constructor to
   2 a. the parameters of the inductive type (Nil?.a x == a, Cons?.a x = a)
   2 b. the indices of the inductive type (n==0, Cons?.n x + 1 == n)

This is the code that does it:
https://github.com/FStarLang/FStar/blob/master/src/smtencoding/FStar.SMTEncoding.Encode.fs#L1043-L1044

The most aggressive fix would be to simply drop the part 2 of the axiom (i.e., the equalities), but this would destroy a lot of code. It would essentially prevent us from getting equalities when matching on things like vector, which would be a showstopper.

So, reviving the earlier comment about a restricted inversion axiom, how about we restrict part 2 of the axiom to only to those parameters/indices in which Type appears strictly positively (or does not appear at all)?

Note, I separated part 2 of the axiom into 2a and 2b, since 2a is related also to issue #65. We would need to exclude 2a altogether in case we wanted to support structural subtyping for inductive types.

@mtzguido @catalin-hritcu @kyoDralliam

[catalin-hritcu]

So, reviving the earlier comment about a restricted inversion axiom, how about we restrict part 2 of the axiom to only to those parameters/indices in which Type appears strictly positively (or does not appear at all)?

@nikswamy Unfortunately, I don't understand this restriction. Can you explain?

We would need to exclude 2a altogether in case we wanted to support structural subtyping for inductive types.

Right, 2a is at odds with subtyping for datatypes. In fact, even just having a way to write Nil?.a seems already bad. That's the kind of projection we need to remove for fixing #65.

[nikswamy]

Let's leave the subtyping for datatypes issues aside for now. I'd be happy to discuss that further on #65. But note that Nil?.a x at the source level (really Nil?.a #a x) is perfectly fine and can already be defined by the user. It is just an identity function on its first (implicit) argument.

[nikswamy]

About the restricted inversion:

My understanding of the injective type formers paradox is that it ties a kind of knot where the inductive type former is applied to (a version of) itself.

An even more restrictive variant of my proposal is to exclude the equality axiom for arguments (parameters or indices) that are themselves type functions.

If we can get away with excluding the equality for only functions of type (Type -> Type) (and others similar ones in which Type appears non-strictly positively), so much the better.

Yet another proposal above was to restrict the axiom to universe 0 inductives. But, that also seems ad hoc, and perhaps overly restrictive. Besides, our inductive types are universe polymorphic, so we'd have to restrict the axiom to their universe-0 instantiations ... which is a bit tricky/clumsy to do in the current SMT encoding (which erases universes quite early).

That said, all of these proposals of mine are rather shallow attempts at plugging the hole exposed by the paradox. I don't have a semantic understanding of what enables the paradox and what would be the most liberal condition to exclude it.

[mtzguido]

I was getting confused by the status of this, so here's the updated paradox, still present, in case it helps. The SMT can find it super efficiently it seems. (Funnily enough, I think it depends on not thunking top-level axioms for w, but of course can be made to work without it.)

module Inj

type i (f : Type u#1 -> Type u#0) : Type u#1 =
  | Mkinj : i f

val isInj : x:_ -> y:_ -> w:(i x) -> Lemma (requires (i x == i y)) (ensures (x == y))
let isInj x y _ = ()

let p (x : Type u#1) : Type u#0 =
  exists a. i a == x /\ ~(a x)

let w : i p = Mkinj

let q = i p

val false_of_pq : p q -> Lemma False
let false_of_pq pq = ()

let pq : p q = assert (exists a. i a == q /\ ~(a q))

let falso () : Lemma False = false_of_pq pq

Need to think a bit more about the solutions. Excluding equalities for type functions will definitely reject this (isInj), but I'd like to squint at this some more.

[catalin-hritcu]

Had a quick look at the thread where this paradox was originally reported:
https://lists.chalmers.se/pipermail/agda/2010/001526.html
It seems that at that point there was no semantic justification for the injectivity of inductive type constructors and they were simply removed from Agda. There are a few messages from Andy Pitts later in the thread in which he hypothesizes about cases when such injectivity might be okay:
https://lists.chalmers.se/pipermail/agda/2010/001573.html

[nikswamy]

I've been working on a universe-based criterion to exclude injectivity axioms for some inductive types.

The issue (as also mentioned in that Agda thread) is that the parameters of an inductive type are excluded from its universe check.

That is, although you can write:

type i (f : Type u#1 -> Type u#0) : Type u#1 =
  | Mkinj : i f

You are forced to write

noeq
type j : (Type u#1 -> Type u#0) -> Type u#2 =
  | MkJ : f:(Type u#1 -> Type u#0) -> j f

Note the Type u#2

Injectivity for first type i is questionable since it postulates an injective function from Type u#2 to Type u#1 which doesn't make sense

This particular paradox doesn't work with j (the indexed variant) since the universes don't work out when building the devious diagonal p.

So, in my branch (https://github.com/FStarLang/FStar/tree/nik_attemping_349), I have an SMT encoding patch that omits the injectivity axioms for inductives in case one of its parameters includes a function from a universe that is bigger than the universe of the inductive itself.

This excludes the paradox, although you can (correctly) still derive false by assuming injectivity of i. See examples/paradox/InjectiveTypeFormers.Explicit.fst and InjectiveTypeFormers.SMT.fst, which are variants of Guido's example from above.

I'm running a regression test to see what impact this has on existing code.

Comments most welcome.

[nikswamy]

Update: At least in the F* repo, no code regressed.

[kyoDralliam]

I'm a little late on this thread but I'm a bit puzzled about the parameter vs indexes thing in F*.
Reusing @nikswamy's example

type vector (a:Type) : nat -> Type =
| Nil : vector a 0
| Cons: hd:a -> n:nat -> vector a n -> vector a (n + 1)

I would expect the encoding of this type to acknowledge that a is a parameter (and not to talk about it at all) and n is an index (so there is somewhat one type defined for each indexing element), that is

forall x a n. HasType x (vector a n) ==>
   (n == 0 ==> Nil? x) \/
   (forall n'. n == n' + 1 ==> Cons? x /\  Cons?.n x == n')

Or maybe in a more straightforward fashion

(forall x a. HasType x (vector a 0) ==> Nil? x) /\ 
(forall x a n. HasType x (vector a (n+1)) ==> (Cons? x /\ Cons?.n x == n))

Regarding the paradoxical inductive, I agree with @nikswamy that you have to consider the two "versions" of the inductive, whether you take the function between universes as an index or a parameter.
The indexed version allows you to derive injectivity but as @nikswamy explained universe levels prevent any further paradox.
The parameter version

type i (f : Type u#1 -> Type u#0) : Type u#1 =
  | Mkinj : i f

shouldn't allow you to derive injectivity (after all, it is just a weakening of unit where for some reason we decided to carry around a phantom type) and the encoding should just not provide anything about the parameter. I have the impression it should probably be fine to have the following encoding of inversion for i :

forall x f. HasType x (i f) ==> MkInj? x

[nikswamy]

That's a good suggestion Kenji ... to exclude injectivity for all parameters, period. I'm trying it now.

[nikswamy]

Ok, that doesn't work ... many regressions. Aseem and I considered this on Friday, but rejected it.

This is very intimately related with #65. We might be able to fix them together, some day.

More soon.

[nikswamy]

Closing this for now since we have fixed this paradox.

There could be a potential better fix some day related to #65. If we get to that, let's reopen this issue.