Tony's Wiki

Jun 5 Meeting

13 min read

Subtyping Soundness and Counter-example Investigation [by May 16 discussion on Discord]

Summary of Current Status

The primary goal is to establish the soundness of a “translate subtyping” approach, particularly its relationship with a declarative subtyping system for recursive types. A key challenge has emerged: a specific counter-example demonstrates a subtyping relation that holds in the translate (algorithmic) system but for which a derivation in the declarative system (using transitivity via a middle type) has not been found. This potentially breaks the completeness of the declarative system with respect to the algorithm (algo => decl).

Core Problem: Discrepancy between Algorithmic and Declarative Subtyping

The problematic subtyping relation is: mu a. (mu b. Top -> Int) & mu a. (mu b. a -> Bool) <: Yes (in translate subtyping) mu a. (mu b. (b -> Int) & (a -> Bool))

Issue: It’s proving difficult to find a “middle type” M in the declarative system such that: LHS <: M and M <: RHS where LHS is mu a. (mu b. Top -> Int) & mu a. (mu b. a -> Bool) and RHS is mu a. (mu b. (b -> Int) & (a -> Bool)).

Failed strategies to find a middle type:

  1. “Merge then subtyping”: LHS <: mu a. ((mu b. Top -> Int) & (mu b. a -> Bool)) Then this intermediate type <: No (by nominal unfolding) RHS. (This step is problematic because the negative occurrence of a forbids merging the mu b. binders if they are not equivalent, which they aren’t here due to Top vs a).
  2. “Subtyping then merge”: LHS <: mu a. (mu b. b -> Int) & mu a. (mu b. a -> Bool) (This subtyping holds) Then mu a. (mu b. b -> Int) & mu a. (mu b. a -> Bool) <: mu a. ((mu b. b -> Int) & (mu b. a -> Bool)) (Again, negative a forbids merging mu b.). Then this intermediate type <: No (by nominal unfolding) RHS.

Root Cause of Difficulty: The example involves a combination of:

  • Nested recursive types (mu a. (mu b. ...))
  • A weakly positive comparison (b < Top)
  • A negative comparison (a <: a)
  • Critically, a contravariant occurrence of Top being compared with a contravariant type variable a.

  • Soundness Proof for Type-Directed Casting:

    • If pursuing a direct soundness proof with translate subtyping for a type-directed casting semantics (e.g., BCD-style), issues arise with un-invertible translated types.
    • For instance, in a BCD disjointness rule (B1 <| B |> B2, A*B1, A*B2 ⇒ A*B), if B is a recursive type, splitting it at the translated type level can lead to types that don’t cleanly map back to simpler source types, complicating proofs.
    • Example: Translating mu a. (a -> Int) & (a -> Bool) gives [a. {a:(a->Int)&(a->Bool)}->Int & {a:(a->Int)&(a->Bool)}->Bool]. Splitting this yields components like [a. {a:(a->Int)&(a->Bool)}->Int]. For this to be useful as an intermediate step mapping to the source, it needs to be rewritten/correspond to [a. {a:(a->Int)}->Int] (i.e., mu a. a -> Int).

  • Operational Semantics:

    • Lack of concrete operational semantics makes it hard to determine definitively if the problematic subtyping should hold by constructing terms.

Positive Developments

  • Generalized Structural Unfolding Lemma:
    • A more generalized structural unfolding lemma has been proven, which is simpler than the JFP version, thanks to polarized substitution and translate subtyping.
    • JFP version: If mu a. A <: mu a. C <: mu a. D <: mu a. B then A [a |-> mu a. C] <: B [a |-> mu a. D] (middle types mu a. C, mu a. D must be recursive).
    • New version: If mu a. A <: C <: D <: mu a. B then A [a |-> C] <: B [a |-> D] (no restriction on middle types C, D being recursive). This is beneficial for encoding.

Proposed Paths Forward / What to Try Next

  1. Deeper Dive into the Counter-example:

    • Attempt to find an alternative middle type in the declarative system that was not yet considered.
    • todo Explore coercive semantics (e.g., by trying to write Haskell functions) to gain intuition about whether the subtyping should practically hold.

  2. Modify/Refine the Declarative Subtyping System:

    • Option A: Extend Declarative Rules: Extend Declarative Rules
      • Investigate adding new rules or modifying existing ones (e.g., Amber rules, nominal unfolding) to make the declarative system more powerful to cover the counter-example. This aims to restore algo => decl completeness.
      • Consider developing BCD-style rules for recursive types directly at the source level.
    • Option B: Restrict Subtyping (make it less expressive but potentially more regular):
      • Idea: Identify and exclude “corner cases” that are practically irrelevant but cause theoretical difficulties. The key case is mu a. Top -> a <: mu a. a -> a (or more generally, Top vs. a type variable a in contravariant positions).
      • Mechanism in Nominal Rules: Source Subtyping
        • Augment the mu-sub rule: T |- [{a:A}/a]A <: [{a:B}/a]B Check a A B
        • Check a A B would be a predicate that detects problematic comparisons like a <:- Top (variable a on LHS of subtyping against Top on RHS, in a contravariant context derived from unfolding).
      • Mechanism in Target Type Subtyping (Translate Subtyping):
        • Introduce polarized subtyping (<:+, <:-) and polarized well-formedness (T |-+ A, T |-- A) for target types (which are non-recursive).
        • This would enforce that labelled types (resulting from translating contravariant recursion variables) only appear in negative positions.
        • The subtyping rule {a : A} <:- Top could be rejected by such a polarized system.
      • Impact: This might simplify the system and proofs, but one must verify that essential expressive power and properties like transitivity are not lost.
      • todo play in haskell

  3. Refine the Translation and Target System Properties:

    • Stronger Well-Formedness for Target Types:
      • Develop stricter well-formedness criteria for types in the target language. The goal is to ensure that any type arising during a subtyping derivation in the target language (especially intermediate types from splitting) must correspond to a well-formed source type.
      • This could prevent the generation or use of “ill-formed” intermediate target types (those not invertible to a source type) in proofs that require mapping back to the source system.
      • If a target type T_m is used as a middle type in |A| <: T_m <: |B|, T_m should be “invertible” or correspond to some source type S_m such that A <: S_m <: B could be considered.
      • This could address the “un-invertible types” from splitting, as types like [a. {a:(X&Y)}->Z] (from splitting) might be deemed ill-formed if they can’t be related back to something like [a. {a:X}->Z].

  4. Direct Soundness Proof Strategy:

    • Continue pursuing a direct proof of type soundness using the algorithmic (translate) subtyping, leveraging the new generalized structural unfolding lemma.
    • This path might bypass the need for proving full equivalence with a declarative system if direct soundness can be shown.
    • Requires tackling the issue of un-invertible translated types in the context of the chosen operational semantics (e.g., type-directed casting).

    Also related to Can we use the unfolding lemma to reject this example?

  5. Encoding Considerations:

    • Homogeneity: If the generalized structural unfold rule (with type annotations A+, A-) is necessary for encoding operations like subst, ensure the same generalized strategy is applied consistently for other operations (eval, double) for a “homogeneous” encoding. ( todo Tony to double-check this).
    • Investigate if a similar generalization is needed for fold operations. Current thinking is no, because fold applies to supertypes, while unfold deals with subtypes (like intersections).

Attempts

What is the case in the most general setting? Equi-recursive Amber + distributivity rule

   mu a. (mu b. Top -> Int) & mu a. (mu b. a -> Bool)
<: mu a. (mu b. (b -> Int) & (a -> Bool))


a1 & a2 <: a'
|- (mu b. Top -> Int) & (mu b. a2 -> Bool) <: mu b. (b -> Int) & (a' -> Bool)

a1 & a2 <: a', b1 <: b'
|- (Top -> Int) & (a2 -> Bool) <: (b' -> Int) & (a' -> Bool)

(X) Does not seem to work

Can we use the unfolding lemma to reject this example?

A1 = Top -> Int
A2 = a -> Bool
B1 = b -> Int

   (mu a. (mu b. A1)) & (mu a. (mu b. A2))
<: (mu a. (mu b. B1 & A2))

question, what is the unfolding lemma in the presence of distributive subtyping?

  • Is it the form we have proved?
  • What is the operational semantics?

Cf. Qianyong’s work, is disjointness enforced in the typing rule?

Extend Declarative Rules

Attempt:

--------------- mu-dist
mu a1 ... an. A & mu a1 ... an. B <: mu a1 ... an. A & B

so we could go for subtyping then merge (simultaneously on two binders)
   mu a. (mu b. Top -> Int) & mu a. (mu b. a -> Bool)
<: mu a. (mu b. b -> Int)   & mu a. (mu b. a -> Bool)
<: mu a. (mu b. (b -> Int) & (a -> Bool))


However, the rule is not admissible (unsound) in the translate system
(nested recursion requires the inner translation to be invariant rather than invariant)

also, as the second subtyping is not accepted by the algorithm, the rule should not attempt to include what wasn't included in the algorithm, but rather attempt to accept the original two types on LHS and RHS

Restrict the subtyping

Source Subtyping:

prevent: The key case is mu a. Top -> a <: mu a. a -> a (or more generally, Top vs. a type variable a in contravariant positions)

Source:

A [a |-> {a : A}] <: B [a |-> {a : B}]
Check Pos a A B
----------------------------
mu a. A <: mu a. B



+-----------------+
| Check Pos a A B |
+-----------------+

-----------------------
Check Pos a a <: Top


-----------------------
Check m a b <: Top


Check m a (A[b |-> {b : A}]) (B[b |-> {b : B}])
----------------------- mu?
Check m a (mu b. A) (mu b. B)
  • We have built-in transitivity in the source, so this is not a concern

Target Subtyping:

Target


|-+ A
-----------
A << Top


+--------+
| |-m A  |
+--------+

|-+ A
-------------
|-+ {a : A}


|-m ... for rest of the cases
  • We should be able to prove a stronger regularity lemma for the target subtyping, so transitivity for the target subtyping should also be fine
  • Benefit: since we only modify the well-formed ness, if we manage to prove transitivity, then all the properties (e.g. generalized unfolding lemma) should still hold in the target system
  • Question: is the new rule still sound?
  • Question: it helps with the subtyping, how about the whole completeness proof?
    • we will need to write a stronger polarized substitution lemma
    • The hope: no more a weakpos in A << B, where there could be negative a in B, but we know a in fv_pos(B), so any rewriting for B will be equivalent and we can transfer B back to an invertible type

Encodings

Heterogeneous structural rule

In Encoding CP + negative methods, we propose:

e : A+
A+ <: A- <: mu a. B
--------------------- polarized structural unfolding
unfold [A+, A-] e : B [a+ |-> A+, a- |-> A- ]


B [a+ |-> A+, a- |-> A- ]
=(B [a+ |-> A+]) [a- |-> A-]

a is not free (A)
  (B [a+ |-> A+]) [a- |-> A-]
= (B [a- |-> A-]) [a+ |-> (A+ [a+ |-> A-])]
= (B [a- |-> A-]) [a+ |-> A+]

B [a+ |-> A+, a- |-> A- ]

mu a. A ~~~> [a. A [a- |-> { a : A } ] ] 
trans2 C D ->
trans2 (subst_tt_m mode X C A) (subst_styp_m mode X D B).


    mu a. A [b+ |-> C] 
~~> [a. A [a- |-> { a : A } ] ]  [b+ |-> D]
 == [a. (A [b+ |-> D]) [a- |-> { a : A } [b- |-> D] ]  ]

We could dually, extend:

e : A [a |-> B]
mu a. A <: B
---------------
fold [B] e : B

If mu a. A <: B <: C <: mu a. D
then A[a |-> B] <: D [a |-> D]

to?

e : A [a+ |-> B+, a- |-> B- ]
mu a. A <: B- <: B+
--------------------- polarized structural folding
fold [B+, B-] e : B+

What will the generalized structural unfolding be like?

For reduction: unfold [A+, A-] (fold [B+,B-] v) ----> v

The typing derivation:
v : C [a+ |-> B+, a- |-> B-]
mu a. C <: B- <: B+
------------------
fold [B+, B-] v : B+          B+ <: A+
------------------------------------
fold [B+, B-] v : A+                           A+ <: A- <: mu a. D
-----------------------------------------------------------------------------
unfold [A+, A-] (fold [B+, B-] v) : D [a+ |-> A+, a- |-> A- ]

The lemma should therefore be:

given:
mu a. C <: B- <: B+ <: A+ <: A- <: mu a. D

show: C [a+ |-> B+, a- |-> B-] <: D [a+ |-> A+, a- |-> A- ]

Proof attempt:

by translation:

C [a- |-> {a : C}] <: D [a- |-> {a : D}]

Case 1. 
a is weakly positive in C and D
We can show:
C [a- |-> B-] << D [a- |-> A-]
Moreover, as B+ << A+
We can show:
C [a- |-> B-, a+ |-> B+] << D [a- |-> A-, a+ |-> A+]


trans2 A B ->
trans2 C D ->
trans2 (subst_tt_m mode X C A) ~~> (subst_styp_m mode X D B).





Case 2.
D <: C, C <: D
which implies that
mu a. C == mu a. D

mu a. C <: B+ <: B- <: A+ <: A- <: mu a. D <: mu a. C <: B+ <: B- <: A+ <: A- <: mu a. D
any types are equivalent


We can show:
C [a- |-> B, a+ |-> B] << D [a- |-> A-, a+ |-> A+]
since B, A-, A+ are just equivalent to mu a. C / mu a. D

However, the other dual forms, such as


e : A [a+ |-> B+, a- |-> B- ]
mu a. A <: B+ <: B-
--------------------- polarized structural folding (with B+ <: B-)
fold [B+, B-] e : B-




e : A-
A- <: A+ <: mu a. B
--------------------- polarized structural unfolding (with A- <: A+)
unfold [A+, A-] e : B [a+ |-> A+, a- |-> A- ]

Seems also fine to prove the structural unfolding lemmas (though they are not useful in the encoding)?

  • Maybe what we need is something stronger than the structural unfolding lemma
  • Maybe some dual forms are subsumed by other better ones

Graph View

Backlinks