Comments for sigma-types

[fredokun]

I have commented the sigma-types proposal (cf. commit https://github.com/latte-central/latte-kernel/commit/6993ce4d25814fe238b5245ccc9d1f4fc74e2b80) cf. https://nextjournal.com/a/LRd1LDA1MM6fzs3AAVuES

[zampino]

Hello, thanks for the comments on the article! Until we get proper commenting feature in nextjournal (it's on the roadmap) I'll answer here.

I think the lambda should be reduced inside the pair ... the types are identical, but we did not reach the normal form in the first case.

Should l/term give a normalised form via unparsing? Could you give an example where this is visible?

When computing the type of pair of the form (pair (lam arg) v) the type of (lam arg) is normalised, hence we're getting the same types in your two examples, right?

Normalisation is still relevant when computing the type of projections. By normalising the projectand we can assert:

  (l/type-check?
    [A :type][B :type]
    [a A][b B]
    (pr2 ((λ [t A] (pair t b)) a))
    B) ; => true

as opposed to situations where the projectand doesn't normalise to a pair.

  (l/type-of
    [T :type][P (==> T :type)][p (Σ [t T] (P t))]
    (pr2 p)) ;=> [P (pr1 p)]

On the other hand it would be maybe interesting to treat normalisation of redexes of functions from dependent pairs in (Σ [t T] (P t)) i.e. (f (pair x y)) as (f x y) provided f : (Π[t T] (==> (P t) B)) like we actually do in the ex elimination proof via sigma types. I wouldn't be sure how/when to enforce the constraints on the type of functions involved, i.e. how to define (==> (Σ [t T] (P t)) B) as (Π[t T] (==> (P t) B)).

but after that only the intro and elim rules will be used so I do not see a strong argument in favor of sigma types for only encoding the existential

I agree with that and I guess the book is against pairs because it introduces some undesired complexity, but if we can keep that complexity under control in LaTTe, maybe we can leave pairs as a sort of hidden feature which shouldn't impact on the core functionalities (we could raise or warn you can't do that with a pair yet ?).

In general what I'm mostly interested in is using sigma types for formalising quotients. Starting from a structure (M, *, ~, c) with say a binary operation * and an equivalence relation ~ compatible with * and given c a canonical coherent choice of representatives for ~ classes, following [@CohenCyril, Pragmatic Quotient Types] we can define Quot(M, ~) := (Σ [m M] (equal m (c m))). In this way we can project * onto the quotient like (*/~ (pair x x') (pair y y')) := (pair (c (* x y)) idm ) where idm is a proof of idempotency for c. This should yield a simpler treatment wrt handling equivalence classes as sets.

Also re structs

provided as a sort of syntactic sugar above the current theory

yes that would be really nice. Say we'd have something like

(defstruct Monoid "A monoid over a type"
  [[T :type]]
  :id T
  :m (magma T)
  :assoc (associative T :m)
  :left-id (left-identity T :m :id))

Then we could try alternative definitions via prop/and* or via nested sigma types. Having a term [M (Monoid T)] then selection of fields e.g. (:assoc M) should be possible (keywords are not yet used in LaTTe syntax, perhaps?) by means of either prop/and-elim* or by means of a composition of left/right projections ( I guess this is what you call "peeling"?). Then we can compare implementations and chose the one which is more easy to reason about or yields simpler proofs? I'll have a look at Z schemas :-).

[zampino]

@fredokun I'm a bit lost around how to approach (Leibniz?) equality for terms of sigma types at the present stage of the branch. Would you have a suggestion or some references in this regard? In case we define Leibniz equality (provided we define functions from sigma types), is there a relation between Leibniz equality of a pair wrt the equality of the first components?

Should it be a component-wise equality?

[fredokun]

Hi @zampino sorry I'm a little bit busy... Part of my relative "fear" of sigma-types (beyond the fact that in the absence of realizability, they are redundant with subtypes+Pi) is that of axiom K (https://stackoverflow.com/questions/39239363/what-is-axiom-k/39256457), which I think relates to your question (not sure though ...)... Leibniz equality operates on predicates and sigma types are no predicates. (will investigate some more ...)

[fredokun]

Well, not sure K is involved because with second order encoding of equality you don't have a constructor for equality proofs... Maybe you need functional extensionality ? cf. https://stackoverflow.com/questions/27079513/prove-equality-on-sigma-types

[CohenCyril]

Hi! I got tagged in this conversation, hence I get notified about your conversation. I have no idea what you are doing but your sigma type questions raised my attention. Please ignore me if my input is irrelevant or unnecessary. But in case it helps, in Coq, Leibniz equality on a sigma type is equivalent to a dependent pair of equalities where the first equality is equality of first components and and the second is equality of the second components modulo a "transport" using the first equality. The proof is done without K or UIP, and relies on dependent elimination of equality. More precisely:

From Coq Require Import ssreflect ssrfun ssrbool.

Lemma eq_sigma A (B : A -> Type) (x y : {a : A & B a}) :
  x = y <-> {p : projT1 x = projT1 y & eq_rect _ B (projT2 x) _ p = projT2 y}.
Proof.
split=> [->|]; first by exists erefl.
case: x y => [xa xb] [ya yb]/= [p <-].
by pose dep P Pxx y p : P y p := ecast y (P y _) p Pxx; elim/dep: _ / p.
Qed.

[fredokun]

@CohenCyril this is very relevant thx ! I'm not very well versed into sigma types though, so I may say silly things. The way we define Leibniz equality in LaTTe is the textbook def. :

(definition equality
  [[T :type] [x T] [y T]]
  (forall [P (==> T :type)]
          (<=> (P x) (P y))))

@zampino Can we easily have an eq_sigma lemma like this based on your implementation ?

[zampino]

@CohenCyril thank you for your input! Although I'm not really familiar with Coq, the statement of the lemma does makes sense to me. Any suggestion for where could I read more about dependent elimination of equality?

@fredokun

Can we easily have an eq_sigma lemma like this based on your implementation?

I'll try that. If I understand eq_sigma correctly, the left-hand type is Leibniz equality, and in order to state that, we'll need to first define functions (==> (Σ [t T] (P t)) :type) as commented above.

The right hand type, if I understand the definition of eq_rect, seems to be constructed via something like the substitution principle, i.e. in LaTTe

(defthm eq-subst-thm
  "Substitutivity property of equality. This is the main elimination rule."
  [[T :type] [P (==> T :type)] [x T] [y T]]
  (==> (equal x y)
       (P x)
       (P y)))

@CohenCyril what does *_rect hint at in Coq?

But if the proof of the lemma uses some form of induction, I fear we cannot do that in LaTTe yet.

[CohenCyril]

@CohenCyril what does *_rect hint at in Coq?

In Coq eq_rect seems to be like your LaTTe eq-subst-thm (this is also called non-dependent elimination).

But if the proof of the lemma uses some form of induction, I fear we cannot do that in LaTTe yet.

Yes indeed, the Coq proof relies on eq being an inductive type for which dependent elimination holds, i.e. forall (T : Type) (x : T) (P : forall y, x = y -> Type), P x (refl x) -> forall (y : T) (e : x = y), P y e holds : in other word, any proof of equality is actually reflexivity, provided you substitute the right hand side by the left hand side everywhere, and not the "textbook definition" which only states substitution under any context (non-dependent elmination, i.e. eq_rect/eq-subst-thm).

The historical reference for dependent elimination in Coq is Inductive definitions in the system Coq rules and properties by Christine Paulin-Mohring and a nice description of path induction is in the HoTT book (https://homotopytypetheory.org/book/) section 1.12.1 Path induction

[zampino]

@CohenCyril thanks a lot for the hints, I fear I have a lot to read. This HoTT stuff shows up at every corner :-).

[fredokun]

I have been thinking a little bit about sigma types, and also discussed them with @pedagand. The syntax you use @zampino for pairs (pair a b) corresponds to a curry-style encoding. If you know that a is of type A and b is of type C, then you cannot directly synthesize a type (Σ [x A] B) because you don't know how to form B from a and C. We know that C should be equal to B{a/x} but then you would have to find all occurrences of a (an arbitrary term of type A) in C in order to recover B. So in order to code dependent pairs, you have to use a Church-style syntax, something like

(pair a [x A] b B)

or

(pair a [x] b B)

would be enough because A can be inferred from a ...

[fredokun]

Also @zampino I guess projections must be beta-normalized,

(proj1 (pair a b [x] B)) should be the same as the a I think this is important is proofs...

[fredokun]

Also slightly related but one of the use cases for sigma-types is the encoding of dependent records, and in many cases just to have non-dependent records. I think non-dependent records would be an interesting extension of the kernel. Dependencies can always be encoded using pi-types.

[zampino]

Thanks for the comments :-)

(pr1 (pair a b [x] B)) should be the same as a

I guess this means \beta-equivalent as per latte-kernel.norm/beta-eq? and in fact atm

(latte/term-eq?
 [T :type][P (==> T :type)]
 (pr1 (pair a b))
 a)

gives false.

you cannot directly synthesize a type (Σ [x A] B) because you don't know how to form B from a and C.

Oh, I see. So far I've been doing a naive substitution:

https://github.com/latte-central/latte-kernel/blob/430dd3c7cbf36c11c9361eeeaca375224f390995/src/latte_kernel/typing.cljc#L252-L268

Introducing a fresh variable x and trying to replace all occurrences of a in B with x to retrive B' and synthesise (sigma [x A] B').

As outlined in this article the problem with the above substitution is (also) normalisation. So as a first step I'll normalize both B and a before doing the substitution.

But could you give an example where the type could not be rebuilt just by substitution? What would be the relation of the binding x with a and B in the syntax (pair a [x A] b B)?

[pedagand]

x = (pair true 1) and y = (pair false "foo") are of type (sigma [x Bool] (if x then Int else String)) but how could we infer this type given only x or y?

This is addressed if you're explicit about the type of the second component in the constructor: (pair true [x] 1 (if x then Int else String)).

[zampino]

@pedagand thank you for the example, I see the point in general.

Trying to reproduce a similar test case in LaTTe, I don't understand how to immediately apply the above scenario to LaTTe typing. If you give x or y upfront in LaTTe, you'd need to exhibit a context in which true, false and 1 are typed. So that e.g. (pair true 1) will have type (sigma [t Bool] Int). Unless you mean (pair true 1) would have both the non-dependent pair type and the dependent one contradicting type unicity (maybe a stupid question)?

I think both type checks will pass in LaTTe on the sigma branch.

(type-check?
  [Int *][Bool *][true Bool][1 Int]
  (pair true 1)
  (sigma [u Bool] Int))

or (whatever the encoding of if):

(defaxiom Bool [] *)
(definition select  [[A *][B *]]
  (lambda [t Bool] (if t A B)))

(type-check?
  [a Bool][b (select a)]
  (pair a b)
  (sigma [u Bool] (select u)))

i.e. the reduction of (select a) seems irrelevant here. Is something missing?

[pedagand]

To draw a parallel: you need an annotation on the pair constructor for the same reason that you need an annotation on the lambda.

The reason is that you want type-synthesis to be stable under reduction. In the scheme you describe, (pair true 1) would have type (sigma [t Bool] Int) whereas (pair true (if true then 1 else "Foo")) would have type (sigma [t Bool] (if t then Int else String)) while we have (pair true 1) == (pair true (if true then 1 else "Foo")).

Besides (and perhaps more crucially), generalizing the type of the second component by anti-substituting the term of the first component is a very fragile business: what tells you that every occurrence of true in the second component is meant to refer to the first component? conversely, what if true has been substituted by f(bar) which reduces to true? This is way too syntactic a criteria to work in practice.

[zampino]

The reason is that you want type-synthesis to be stable under reduction

Yes I'm getting that, we'd get 2 different types for the same term. Thank you for the explanation.

what tells you that every occurrence of true in the second component is meant to refer to the first component?

and yes, I agree the current strategy is pretty weak.

If we annotate the role of the first component, we'd know exactly what to substitute, but in the explicit notation typing of a pair would become trivial and not need any substitution, right?

In the simplest case, would be a matter of rewriting.

(type-of
  [T *][P (==> T *)][a T][b (P t)]

  (pair a [t T] b (P t))
  (sigma [t T] (P t)) 

And it would become trivial to understand if we're in presence of an actual dependency or if the two components are type independent.