0
$\begingroup$

I'm working through Programming Language Foundations in my free time. In the subtyping chapter, I am greeted by the following exercise, where TF P := P \/ ~ P:

Theorem formal_subtype_concepts_tfh:
  TF (exists f : nat -> ty,
         (forall i j, i <> j -> f i <> f j) /\
         (forall i, f i <: f (S i))).

This is my type system:

Inductive ty : Set :=
    Ty_Top : ty
  | Ty_Bool : ty
  | Ty_Base : string -> ty
  | Ty_Arrow : ty -> ty -> ty
  | Ty_Unit : ty
  | Ty_Prod : ty -> ty -> ty.

where Top is the type that all types are a subtype of.

I believe this statement is false (the right branch, ~P is provable). My logic for this is that the second condition in the conjunction,

forall i, f i <: f (S i)

states that the output of (f i) is a subtype, or more specific than the output of (f (S i)). This would mean that (f 0) would have to be the most specific type in a series, which should not be possible given just product and arrow types (both of which have an unbounded, finite size).

So, the contradiction should arise from a statement I've already proven:

Theorem no_least_type : 
    ~ (exists S, forall T, S <: T).

The difficulty I'm having is generalizing this concept without a definition for f. I want to say that to satisfy the first branch of the conjunction, f must use either T_Arrow, T_Prod or T_Base as the output of the successor case of its input. And because there are no such arrow, product, or base types that satisfy the second branch of the conjunction, the statement must be false. Unfortunately, my attempts at these lemmas quickly blow up beyond what seems reasonable.

I've also attempted to directly specialize no_least_type with f i to solve the problem, but applying that to a False goal obligates me to prove that

forall f i T, (f i <: f (S i)) -> (f i <: T)

which is going in the wrong direction to be provable. This does seem like a promising direction for the proof though, because any induction on either a type or piece of subtyping evidence would quickly blow up, which Pierce seems to avoid in exercises.

Is there any fundamental insight I'm missing here?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

There's a flaw in your reasoning that this should follow from no_least_type. That there is no subtype of all types does not imply that there is no subtype of an infinity of types.

For a similar example, consider the real interval (0,1] (closed on the right so that there is also a top element), and adapt your properties by replacing ty with (0,1] and <: with <.

~ (exists S : (0,1], forall T, S < T)

is true. Yet you can certainly construct an infinite increasing sequence.

exists f : nat -> (0,1],
         (forall i j, i <> j -> f i <> f j) /\
         (forall i, f i < f (S i))

is also true.

Improve this answer
$\endgroup$
6
  • $\begingroup$ I understand the logic for reals, but with this typing example, wouldn’t the subtype of an infinity of types have the most constructors out of all of them? Therefore, to satisfy that no two outputs are the same, the number of constructors per output of f would decrease, meaning that there could not be an infinite number of them. $\endgroup$
    – Charles Averill
    Commented Mar 15 at 18:33
  • $\begingroup$ Because of the function type, it's also not true that if S is a subtype of T, S has more constructors than T. $\endgroup$
    – Li-yao Xia
    Commented Mar 15 at 18:59
  • $\begingroup$ I think I'm starting to understand, but it still hasn't clicked. The subtyping relation has three relevant rules: "S <: Top," "S1->S2 <: T1->T2 if T1<:S1 and S2<:T2," and "S1*S2 <: T1*T2 if S1<:T1 and S2<:T2." The other rules are reflexivity (not helpful because of the req that outputs are different) and transitivity, which should just route to the other three rules. Of those three rules, arrow and product imply that ordered subtyping requires an increase in the number of constructors. How could you get around this with just the Top rule? $\endgroup$
    – Charles Averill
    Commented Mar 15 at 21:40
  • $\begingroup$ I've looked at something like f 0 = Top * Base 0, f 1 = Base 1 * Top, f 2 = Top * Base 3 etc., but without a way to subtype Bases the inductive step fails. This feels like it's closer to the right track that you've implied, because there are an unbounded number of Bases, so terms can be instantiated without an increase in constructors as the input increases. However, with both the arrow and product rules placing all four of their subcomponents in a subtyping relation, this doesn't seem like a viable approach. $\endgroup$
    – Charles Averill
    Commented Mar 15 at 21:44
  • 1
    $\begingroup$ This series of hints was amazing. I just solved it, definitely overthinking too much. Thank you for your help! The critical realization was that the left side of an arrow in a chain of arrows can be generated to become more specific over time, and the right side doesn’t matter because of reflexivity. $\endgroup$
    – Charles Averill
    Commented Mar 16 at 13:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.