The --without-K option is too restrictive

[UlfNorell]

From andres.s...@gmail.com on May 31, 2013 15:08:11

(See related discussion in http://thread.gmane.org/gmane.comp.lang.agda/4671/focus=5257 )

The following code is rejected using the --without-K option:

infixl 7 * infixl 6 + infix 4 ≡ infixr 1 ⊎

data ≡ {A : Set} : A → A → Set where refl : ∀ {a} → a ≡ a

data ⊎ (A B : Set) : Set where inj₁ : (x : A) → A ⊎ B inj₂ : (y : B) → A ⊎ B

data ℕ : Set where zero : ℕ suc : (n : ℕ) → ℕ

+ : ℕ → ℕ → ℕ zero + n = n suc m + n = suc (m + n)

* : ℕ → ℕ → ℕ zero * n = zero suc m * n = n + m * n

foo : ∀ m n → m * n ≡ zero → m ≡ zero ⊎ n ≡ zero foo zero n h = inj₁ refl foo (suc m) zero h = inj₂ refl foo (suc m) (suc n) ()

-- The indices -- suc (n₁ + m₁ * suc n₁) -- zero -- are not constructors (or literals) applied to variables (note that -- parameters count as constructor arguments) -- when checking that the clause foo (suc m) (suc n) () has type -- (m n : ℕ) → m * n ≡ zero → m ≡ zero ⊎ n ≡ zero

bar : ∀ m n → zero ≡ m * n → m ≡ zero ⊎ n ≡ zero bar zero n h = inj₁ refl bar (suc m) zero h = inj₂ refl bar (suc m) (suc n) ()

-- The indices -- zero -- suc (n₁ + m₁ * suc n₁) -- are not constructors (or literals) applied to variables (note that -- parameters count as constructor arguments) -- when checking that the clause bar (suc m) (suc n) () has type -- (m n : ℕ) → zero ≡ m * n → m ≡ zero ⊎ n ≡ zero

Original issue: http://code.google.com/p/agda/issues/detail?id=865

[UlfNorell]

From andreas....@gmail.com on June 02, 2013 08:50:53

Labels: Type-Enhancement WithoutK

[UlfNorell]

From nils.anders.danielsson on June 03, 2013 02:43:35

This is a regression, right?

Labels: -Type-Enhancement Type-Defect Priority-High Milestone-2.3.4

[UlfNorell]

From nils.anders.danielsson on June 03, 2013 02:47:56

AFAICT the code above type checks using both Agda 2.3.2 and the current development version of Agda. However, the library available at http://www.cse.chalmers.se/~nad/repos/equality/ provides an example of a regression (see Fin.agda).

[UlfNorell]

From andres.s...@gmail.com on June 03, 2013 08:53:42

This is a regression, right?

No. There is a regression related to the equality

data ≡ {A : Set}(a : A) : A → Set where refl : a ≡ a

but I didn't report it.

[UlfNorell]

From andres.s...@gmail.com on June 03, 2013 08:54:57

AFAICT the code above type checks using both Agda 2.3.2 and the current development version of Agda.

Did you use the --without-K option?

[UlfNorell]

From nils.anders.danielsson on June 03, 2013 10:11:03

Did you use the --without-K option?

Ah. :) Please include {-# OPTIONS --without-K #-} in the bug report if you find more bugs related to --without-K.

This is a regression, right?

No.

Oh. I see that the regression that you reported in one of your Agda list posts used another definition of equality.

[UlfNorell]

From andreas....@gmail.com on June 03, 2013 12:55:42

The regression #3 is due to information loss in the presence of modules. I will try to improve the situation.

However, to address the original enhancement request, some systematic thinking is required...

Owner: andreas....@gmail.com

[UlfNorell]

From andres.s...@gmail.com on June 03, 2013 19:26:30

The regression #3 is due to information loss in the presence of modules. I will try to improve the situation.

Please remember there is also a regression in the following example, where the equality used is different to the one used in the original report.

{-# OPTIONS --without-K #-}

module Bug where

infixl 7 * infixl 6 + infix 4 ≡ infixr 1 ⊎

data ≡ {A : Set}(a : A) : A → Set where refl : a ≡ a

data ⊎ (A B : Set) : Set where inj₁ : (x : A) → A ⊎ B inj₂ : (y : B) → A ⊎ B

data ℕ : Set where zero : ℕ suc : (n : ℕ) → ℕ

+ : ℕ → ℕ → ℕ zero + n = n suc m + n = suc (m + n)

* : ℕ → ℕ → ℕ zero * n = zero suc m * n = n + m * n

foo : ∀ m n → m * n ≡ zero → m ≡ zero ⊎ n ≡ zero foo zero n h = inj₁ refl foo (suc m) zero h = inj₂ refl foo (suc m) (suc n) ()

-- The indices -- suc (n₁ + m₁ * suc n₁) -- zero -- are not constructors (or literals) applied to variables (note that -- parameters count as constructor arguments) -- when checking that the clause foo (suc m) (suc n) () has type -- (m n : ℕ) → m * n ≡ zero → m ≡ zero ⊎ n ≡ zero

[UlfNorell]

From andreas....@gmail.com on June 03, 2013 23:35:10

I do not consider this as regression, but as rectification. The previous situation was not symmetric. Why should it succeed for m * n == zero, but fail for zero == m * n ?

[UlfNorell]

From nils.anders.danielsson on June 04, 2013 01:46:18

Why should it succeed for m * n == zero, but fail for zero == m * n ?

Because one argument is a parameter, and the other an index?

I realise now that I misunderstood the following comment: "Non-linear parameters are treated just as indices." I thought this had something to do with constructor parameters, not data type parameters. Can you please write something more precise in the release notes? I would also prefer to see the complete rule, not just the delta.

And please also document that you see level parameters as big. (Is this sound?)

[UlfNorell]

From andreas....@gmail.com on June 04, 2013 03:03:43

Now without-K works better with modules. Nisse, please check your equality library again, my machine runs out of memory. At least the Fin.agda does check now.

Documented the new rules in the release notes.

I am downgrading this as feature request now, please reopen if you find more bugs in my fix.

Owner: ---
Labels: -Type-Defect -Priority-High -Milestone-2.3.4 Type-Enhancement Priority-Medium

[UlfNorell]

From nils.anders.danielsson on June 04, 2013 05:22:00

Documented the new rules in the release notes.

Several things are unclear to me. (For instance, "Parameters that occur in constructor indices are classified as `non-linear' and treated just as indices" is a recursive definition.) Let me try to interpret you; let me know if I made some mistake:

Specification of --without-K:

Parameters that are mentioned in any of the data type's constructors' target indices are classified as /non-linear/. The indices may contain constructor applications. Constructors are usually not applied to parameters, but for the purposes of this check [NON-BIG?] constructor parameters are treated as other arguments. [TODO: Or are all parameters ignored?]

A parameter p that is not non-linear and satisfies either of the following requirements is classified as /big/:

• The parameter declaration is p : Level, where Level is the type of universe levels.

  [TODO: Why is this OK?]

• The data type's index telescope has the form … → Set ℓ, and p : A, where A : Set ℓ′ for some ℓ′ > ℓ.

  [TODO: What if ℓ is not in scope at p's declaration site?]

  If the --without-K flag is activated, then Agda only accepts certain case-splits. Let us assume that the type of the variable to be split is D ts, where D is a data (or record) type, let ixs denote the expressions in ts corresponding to non-linear parameters as well as indices, and let pars denote the remaining expressions. Then the following requirement must be satisfied for the case-split to be accepted:

  The elements in ixs must have the form

  i ∷= x | c i … i,

  where x stands for variables, and c for constructors or literals. No variable x can be used more than a single time in all these expressions, and no variable x may be free in pars. Constructors are usually not applied to parameters, but for the purposes of this check non-big constructor parameters are treated as other arguments. (Big parameters are ignored.)

Nisse, please check your equality library again, my machine runs out of memory.

The library still fails to type check (see Bag-equivalence.agda; with a 32-bit build 2GB should suffice to check this file).

I think that the problem now is your treatment of non-linear parameters. I would prefer a rule that does not break existing code. What about the following rule, in which non-linearity is only used to exclude certain parameters from being big?

If the --without-K flag is activated, then Agda only accepts certain case-splits. If the type of the variable to be split is D pars ixs, where D is a data (or record) type, pars the parameters, and ixs the indices, then the following requirement must be satisfied:

The elements in ixs must have the form

 i ∷= x | c i … i,

where x stands for variables, and c for constructors or literals. No variable x can be used more than a single time in all these expressions, and no variable x may be free in pars. Constructors are usually not applied to parameters, but for the purposes of this check non-big constructor parameters are treated as other arguments. (Big parameters are ignored.)

Would this break anything?

Owner: andreas....@gmail.com
Labels: -Type-Enhancement -Priority-Medium Type-Defect Priority-High Milestone-2.3.4

[UlfNorell]

From andreas....@gmail.com on June 04, 2013 08:03:52

1. [NON-BIG?] Yes. (I wrote "small" in the rel.notes)
2. [TODO: level ok?] I do not see how information could flow from the indices into a linear level parameter.
3. [TODO: big ok?] If Agda cannot see that a parameter is big, it defaults to "small". This is why it should be safe in the case you outlined.
4. The failure in Bag-equivalence is now of the form also complained about Andres. My question to you is why equality should not be symmetric. Why would the lhs be a parameter and the rhs an index, such that you have to orient the equality in the right way to pass --without-K? This seems unintuitive.

To fix this, the bigger question is how you arrived at your criterion in the first place. If I understood this, then maybe we could find a generalization that accepts harmless cases where the constructor indices are not entirely patterns.

[UlfNorell]

From andreas....@gmail.com on June 04, 2013 09:38:29

With the linearity check, it seems like the condition that

the variables that are free in the indices (and non-lin parameters) may not be free in the parameters

is superfluous. If I remove this check then the failing test cases WithoutK7 and WithoutK10 pass, but nothing bad (that is only provable with K) happens in these files.

Maybe you needed this criterion to avoid the non-linear situations, which are now avoided differently.

[UlfNorell]

From andres.s...@gmail.com on June 04, 2013 12:28:19

I don't understand your comment for the test case WithoutK10: "that is only provable with K".

If in Foo I replaced the constructor d by a variable, then the test case type-checks:

Foo : ∀ {A} {x : A} → D (let f = λ { unit → x } in f) x → Set₁ Foo h = Set

[UlfNorell]

From nils.anders.danielsson on June 06, 2013 14:06:10

1. [NON-BIG?] Yes. (I wrote "small" in the rel.notes)

You didn't specify clearly whether constructor arguments are reconstructed in the /linearity/ check, as opposed to the /well-formed index/ check. Are they? (My specification above claims that they are.)

Note that your positive answer to this question implies that the definitions of linearity and size are mutually recursive. Is this intended?

[TODO: big ok?]

What does this refer to? The following TODO note?

TODO: What if ℓ is not in scope at p's declaration site?

I do not see how information could flow from the indices into a linear level parameter.

In this case, why does size matter at all? The Level type can be used just like any other type.

My question to you is why equality should not be symmetric.

The Paulin-Mohring definition of equality isn't (syntactically) symmetric, so why should this (very syntactic) check treat both arguments in the same way?

To fix this, the bigger question is how you arrived at your criterion in the first place. If I understood this, then maybe we could find a generalization that accepts harmless cases where the constructor indices are not entirely patterns.

If you don't understand the condition, why do you change it? I prefer the 2.3.2 condition to your new one, for the following reasons:

• The new condition seems to be much more complicated. Its description is at least a lot longer, and I have trouble understanding it.
• I have less trust in the new condition's correctness.
• The new condition is not (yet?) backwards-compatible with the old one.

I think that we should stick to a fairly simple condition.

[UlfNorell]

From andreas....@gmail.com on June 07, 2013 04:31:11

To arrive at a criterion that captures the essence of pattern matching without K, we need to clarify the role of parameters and indices from a semantic stand-point. The syntactic distinction in current Agda is just an approximation, and it has its issues (like big indices). For an attempt:

A parameter is a datatype argument that is not determined (nor constrained) by pattern matching at this type. An index is a non-parameter datatype argument.

With this definition, in Id A a b, A is a parameter and a,b are indices, no matter which syntactic definition of Id you give (Paulin-Mohring or the other, symmetric one).

For heterogeneous equality, HId A a B b, all four arguments are indices.

The distinction between parameters and indices is established at time of the data definition, by analyzing the constructor types. The current analysis just turns non-linear syntactic parameters into (semantic) indices, [but does not turn syntactic indices that are actually not matched on or do not involve nonlinearity into semantic parameters].

During the without-K check, we have to reconstruct all semantic indices that are syntactically parameters.

Of course, the problem cries for a real systematic solution where we prove that the criterion (whatever it will look like in the end) really allows matching without requiring K. I have the suspicion that maybe we should look which unifications are performed during matching, rather than restricting the type at which we allow to match.

[UlfNorell]

From guillaum...@gmail.com on June 07, 2013 10:24:57

What’s wrong with the following definitions?

parameter = an argument before the colon index = an argument after the colon

In particular for Id A a b, A is a parameter, b is an index, and a is an index in the Martin-Löf (symmetric) definition and a parameter in the Paulin-Mohring definition. I don’t see the fact that the Paulin-Mohring identity type is not symmetric and more powerful than the Martin-Löf identity type as a flaw, it’s expected.

The Martin-Löf identity type defines, given a type A, a binary relation =ML on A with constructor reflML : (a : A) -> a =ML a. The Paulin-Mohring identity type defines, given a type A and an element a : A, a unary relation a=PL_ on A with constructor reflPL : a=PL a.

The idea between the two is quite different, they shouldn’t be identified.

[UlfNorell]

From andreas....@gmail.com on June 09, 2013 06:39:35

Wrong is that these definitions are referring to syntax artefacts, not to semantics or intention. In my explanation above, I refer to these concepts as "syntactic parameter" and "syntactic index".

I would be convinced that Martin-Loef identity and Paulin-Mohring identity should be distingished, if you presented me a theorem that separates them, like "this fact holds for MLid but not for PMid" or vice versa.

[UlfNorell]

From andres.s...@gmail.com on June 09, 2013 07:38:54

I would be convinced that Martin-Loef identity and Paulin-Mohring identity should be distingished, if you presented me a theorem that separates them, like "this fact holds for MLid but not for PMid" or vice versa.

I guess this theorem doesn't exist because MLid x y -> PMid x y and PMid x y -> MLid x y.

[UlfNorell]

From guillaum...@gmail.com on June 10, 2013 04:57:40

Wrong is that these definitions are referring to syntax artefacts, not to semantics or intention. In my explanation above, I refer to these concepts as "syntactic parameter" and "syntactic index".

But the intention is different. The Martin-Löf identity type is the initial type-valued reflexive binary relation on A, whereas the Paulin-Mohring identity type defines for every a : A the singleton type associated to a (the initial predicate on A true over a). The fact that they turn out to be equivalent is almost by accident.

Now if your intention is to have a well-behaved identity type, my opinion is that neither the Martin-Löf nor the Paulin-Mohring identity type is the correct answer. The correct answer is the identity type from homotopy type theory. Unfortunately, nobody has managed to give homotopy type theory a computational content yet (so in some sense homotopy type theory is not yet compatible with type theory), but I would suggest that until then we stick with a theory that we understand.

[UlfNorell]

From nils.anders.danielsson on August 29, 2013 07:43:18

I have pushed a patch called "Reverted to the old --without-K semantics." that, hopefully, gives us the 2.3.2 semantics for --without-K. I am not saying that we shouldn't change the meaning of --without-K, which is ad-hoc and not sufficiently well understood. However, I don't think that 2.3.4 should be released with another ad-hoc and not sufficiently well understood rule that is, in addition, not backwards-compatible.