Forbidding injectivity of inductive types with parameters that are too large #1649

nikswamy · 2019-02-13T06:35:01Z

See the discussion in issue #349

@guido

…the suite (thanks @guido)

…her for parameters

… constuctor

This reverts commit 83f48b5.

…ingleton constuctor" This reverts commit 5f4453a.

…, ... the problem being that parameters are still included in the arguments of constructors. This may be more feasible once we solved #65. Revert "trying out a patch where injectivity axioms are just excluded altogether for parameters" This reverts commit e78bf6b.

mtzguido · 2019-02-13T13:54:22Z

Left some minor remarks, here a few higher-level ones.

First, note that this now fails

let isMkInj (x:_) (w:i x) : Lemma (w == Mkinj #x) = ()

I believe since w is Mkinj (Mkinj?.f w) (if one could write that), and we do not know if Mkinj?.f w is x. I feel this could be made work soundly if we didn't have that Mkinj is injective internally. But maybe that is just what Kenji suggested in #349, which caused many regressions? In any case, not sure having this is useful.

Also note some types are not getting injectivity due to how universes are resolved. This one from FStar.Algebra.Monoid, for instance, ends up with a U_name as the universe for a and Type0 as the universe for the type.

type monoid_morphism (#a #b:Type) (f:a -> b) (ma:monoid a) (mb:monoid b) =
  | MonoidMorphism :
    unit:squash (monoid_morphism_unit_lemma f ma mb) ->
    mult:squash (monoid_morphism_mult_lemma f ma mb) ->
    monoid_morphism f ma mb

It can be fixed like this

type monoid_morphism (#a : Type u#aa) (#b : Type u#bb) (f:a -> b) (ma:monoid a) (mb:monoid b) : Type u#(max aa bb) =

Seems to be the only one in ulib/ so this might no be a big deal.

Otherwise looks good to me, the universe check does seem sound. I would also rebase the PR so we have a cleaner history. I could do that if you want.

nikswamy · 2019-02-25T00:19:42Z

Thanks for the comments, Guido.

FWIW, I don't see the "minor remarks" you refer to.

I'm still a bit unsatisfied with the restriction imposed by this patch. It's rather specific in that it excludes injectivity of type formers when they contain function-typed parameters with domain in universes that are too large. That excludes this particular paradox, which is good, and so I'm in favor of this being merged.

OTOH, if the check is really to be justified on cardinality grounds, then a type with any parameter that is in a universe too large (not just those with function-typed parameters with too-large domains) should not be injective. But, that doesn't seem to be feasible at all, since it would exclude many simple parameterized inductive types.

I'm inclined to merge this patch now, so that we forbid at least the paradox we know about.
And then to return to this and provide a more comprehensive solution perhaps in conjunction with a solution to #65. That should also address your example with MkInj #x not being equal to w : i x.

nikswamy · 2019-02-25T00:21:47Z

Also, not sure about the rebasing. We've generally not being doing that ... so why should this PR require it?

mtzguido · 2019-02-13T13:11:12Z

src/smtencoding/FStar.SMTEncoding.Encode.fs

+             let _, k = U.arrow_formals k in //don't care about indices here
+             let tps, env_tps, _, us = TcTerm.tc_binders env tps in
+             let u_k =
+                match (SS.compress k).n with


Could we call env.universe_of here?

Not really, that would compute one universe too high.

In this case, we have, for instance, type t : Type u#0 = ... where k = Type u#0 and we want u_k to be u#0 not its successor.

I agree that this code is more syntactic than ideal. But, fwiw, the typechecking rules for inductices in TcInductive really enforce that the result type of an inductive is a Tm_type or eqtype.

True, sorry, I meant TcTerm.level_of_type

mtzguido · 2019-02-13T13:12:19Z

src/smtencoding/FStar.SMTEncoding.Encode.fs

+                | _ -> failwith (BU.format1 "Impossible: Type of inductive is %s" (Print.term_to_string k))
+             in
+             //BU.print2 "Universe of tycon: %s : %s\n" (Ident.string_of_lid t) (Print.univ_to_string u_k);
+             let rec universe_leq u v =


Maybe this function should live somewhere else, such as Syntax.Util

I didn't want to put this in Syntax.Util since I didn't want it to be used outside of a context (e.g., in the typechecker) where universe unification variables may still be around. This boolean function may give the wrong result when called on universe terms with U_unif terms. The proper way of checking of enforcing universe inequalities in the typechecker would be to call FStar.TypeChecker.Rel to register and solve universe inequality constraints.

Note, within the SMT encoding, we really ought to not have U_unif anymore ... I suppose I could assert that here.

OTOH, when this function returns false, the is_injective flag is false ... i.e., erring conservatively.

I indeed interpreted as a conservative leq, where returning false means "I don't know". It might be useful somewhere else, but we could factor it out when the need arises.

mtzguido · 2019-02-25T01:36:24Z

Sorry, I missed to hit "submit" on the review again. I also think we should merge this for the time being, even if we're not so certain about it.

I'm fine with not rebasing. I only like it to have a cleaner git history to bisect or find out how something evolved.

nikswamy added 14 commits February 10, 2019 15:35

cf #349; exclude injectivity assumptions for type-function arguments

dc57fa8

snap

9133104

a universe-based criterion for forbidding injectivity of type formers

332d41c

adding a couple of variants of the injective type formers paradox to …

840abd2

…the suite (thanks @guido)

snap

eb22031

Merge remote-tracking branch 'origin/master' into nik_attemping_349

3696dd0

snap

0a0c822

trying out a patch where injectivity axioms are just excluded altoget…

e78bf6b

…her for parameters

fixing a regression in DependentMap, by removing a needless singleton…

5f4453a

… constuctor

snap

83f48b5

Revert "snap"

874e42d

This reverts commit 83f48b5.

Revert "fixing a regression in DependentMap, by removing a needless s…

8e405a5

…ingleton constuctor" This reverts commit 5f4453a.

Merge remote-tracking branch 'origin/master' into nik_attemping_349

3ed5379

nikswamy requested a review from mtzguido February 13, 2019 06:35

nikswamy added 2 commits February 12, 2019 22:43

merging

b68e7fe

snap

8daaadc

merging master in

589589a

snap

2368a95

mtzguido reviewed Feb 25, 2019

View reviewed changes

nikswamy added 3 commits February 24, 2019 20:45

incorporating some feedback from @mtzguido from the PR

c64a8a5

snap

dc2ec2d

snap

0bc950e

nikswamy merged commit 953aa38 into master Feb 25, 2019

catalin-hritcu deleted the nik_attemping_349 branch March 15, 2019 16:15

catalin-hritcu mentioned this pull request Mar 24, 2020

Polarities: subtyping for datatypes #65

Closed

nikswamy mentioned this pull request Apr 17, 2024

Injectivity of inductive types revisited #3253

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Forbidding injectivity of inductive types with parameters that are too large #1649

Forbidding injectivity of inductive types with parameters that are too large #1649

nikswamy commented Feb 13, 2019

mtzguido commented Feb 13, 2019

nikswamy commented Feb 25, 2019

nikswamy commented Feb 25, 2019

mtzguido Feb 13, 2019

nikswamy Feb 25, 2019

mtzguido Feb 25, 2019

mtzguido Feb 13, 2019

nikswamy Feb 25, 2019

nikswamy Feb 25, 2019

nikswamy Feb 25, 2019

mtzguido Feb 25, 2019

mtzguido commented Feb 25, 2019

Forbidding injectivity of inductive types with parameters that are too large #1649

Forbidding injectivity of inductive types with parameters that are too large #1649

Conversation

nikswamy commented Feb 13, 2019

mtzguido commented Feb 13, 2019

nikswamy commented Feb 25, 2019

nikswamy commented Feb 25, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mtzguido commented Feb 25, 2019