This implementation not only uses higher-order abstract syntax in specifying the types, but we will exploit extensively the power of parametric and hypothetical judgment. As a benefit we do not need to implement a narrowing lemma separately, but get it "for free".
First, we define or type tp
with higher-order abstract syntax in LF as follows:
LF tp : type =
| top : tp
| arr : tp → tp → tp
| forall : tp → (tp → tp) → tp;
--name tp T
We do not give a general reflexivity and transitivity rule for type variables, but instead we provide for each type variable its own reflexivity and transitivity version. In other words, our rule for polymorφc types implements the following: $$\frac{\Gamma \vdash T_1 <: S_1 \qquad \Gamma,tr:a <: U \rightarrow U <: T \rightarrow a <: T, w:a <: T, ref : a <: a \vdash S_2 <: T_2 }{\Gamma \vdash \forall a:S_1.S_2(a) <: \forall a:T_1.T_2(a)}$$
We use (<:) to denote algorithmic subtyping.
LF sub : tp → tp → type =
| sa_top : sub S top
| sa_arr : sub T1 S1 → sub S2 T2 → sub (arr S1 S2) (arr T1 T2)
| sa_all : sub T1 S1 → ({a : tp} (({U : tp} ({T : tp} (sub a U → sub U T → sub a T))) → sub a T1 → sub a a → sub (S2 a) (T2 a))) → sub (forall S1 S2) (forall T1 T2);
We specify the structure of the context using context schema s_ctx
as follows:
schema s_ctx = some [u : tp] block (a:tp, tr:{U : tp} {T : tp} (sub a U → sub U T → sub a T), w:sub a u, ref:sub a a);
The reflexivity Theorem is simply described as {g:s_ctx} {T: [g ⊢ tp]} [g ⊢ sub T T]
in computational-level in Beluga. Context variable g
and term T
are written explicitly using curly brackets {g:s_ctx}
and {T: [g ⊢ tp]}
. We do case analysis on the term T
of type [g ⊢ tp]
, which is written as [g ⊢ T]
.
rec refl : {g : s_ctx} {T : [g ⊢ tp]} [g ⊢ sub T T] =
mlam g ⇒ mlam T ⇒ case [g ⊢ T] of
| [g ⊢ #p.1] ⇒ [g ⊢ #p.4]
| [g ⊢ top] ⇒ [g ⊢ sa_top]
| [g ⊢ arr T1 T2] ⇒
let [g ⊢ S1] = refl [g] [g ⊢ T1] in
let [g ⊢ S2] = refl [g] [g ⊢ T2] in [g ⊢ sa_arr S1 S2]
| [g ⊢ forall T1 (λa. T2)] ⇒
let [g ⊢ S1] = refl [g] [g ⊢ T1] in
let [g, b : block (a:tp, tr:{u' : tp} {t' : tp} (sub a u' → sub u' t' → sub a t'), w:sub a T1[…], ref:sub a a) ⊢ S2[…, b.1, b.2, b.3, b.4]] =
refl [g, b : block (a:tp, tr:{u' : tp} {t' : tp} (sub a u' → sub u' t' → sub a t'), w:sub a T1[…], ref:sub a a)] [g, b ⊢ T2[…, b.1]] in
[g ⊢ sa_all S1 (λa. λtr. λw. λref. S2)];
The transitivity Theorem is described as (g:s_ctx){Q:[g ⊢ tp]}[g ⊢ sub S Q] → [g ⊢ sub Q T] → [g ⊢ sub S T]
. The context variable is written implicitly in round bracket as (g:s_ctx)
. We do case analysis on the derivation of type [g ⊢ sub S Q]
. In some cases we need to provide extral type annotation for the branch. For example, in the case [g ⊢ sa_arr D1 D2 ]
, which uses sa_arr
rule for the last step of derivation d1
, we add type annotation [g ⊢ sub (arr S1 S2) (arr Q1 Q2) ]
to obtain terms Q1
and Q2
, which are later used as arguments. We use the same technique in the branch of sa_all
. We also need to specify the type of some variables when we don't have enough information on them. For example, in the case [g ⊢ #p.2 U' T' D1 D2]
, we need to specify the type of parameter variable #p
and the type of D1
.
rec trans : (g:s_ctx) {Q : [g ⊢ tp]} [g ⊢ sub S Q] → [g ⊢ sub Q T] → [g ⊢ sub S T] =
mlam Q ⇒ fn d1 ⇒ fn d2 ⇒ case d1 of
| [g ⊢ #p.3] ⇒ let [g ⊢ D2] = d2 in [g ⊢ #p.2 Q _ #p.3 D2]
| [g ⊢ #p.4] ⇒ d2
| {#p : [g ⊢ block (a:tp, tr:{u' : tp} {t' : tp} (sub a u' → sub u' t' → sub a t'), w:sub a U'[…], ref:sub a a)]}
{D1 : [g ⊢ sub #p.1 U']} [g ⊢ #p.2 U' T' D1 D2] ⇒
let [g ⊢ F1] = trans [g ⊢ T'] [g ⊢ D2] d2 in trans [g ⊢ U'] [g ⊢ D1] [g ⊢ F1]
| [g ⊢ sa_top] ⇒ let [g ⊢ sa_top] = d2 in [g ⊢ sa_top]
| [g ⊢ sa_arr D1 D2] : [g ⊢ sub (arr S1 S2) (arr Q1 Q2)] ⇒
case d2 of
| [g ⊢ sa_arr E1 E2] ⇒
let [g ⊢ F1] = trans [g ⊢ Q1] [g ⊢ E1] [g ⊢ D1] in
let [g ⊢ F2] = trans [g ⊢ Q2] [g ⊢ D2] [g ⊢ E2] in [g ⊢ sa_arr F1 F2]
| [g ⊢ sa_top] ⇒ [g ⊢ sa_top]
| [g ⊢ sa_all D1 (λa. λtr. λw. λref. D2)] : [g ⊢ sub (forall S1 (λa. S2)) (forall Q1 (λa. Q2))] ⇒
case d2 of
| [g ⊢ sa_top] ⇒ [g ⊢ sa_top]
| [g ⊢ sa_all E1 (λa. λtr. λw. λref. E2)] : [g ⊢ sub (forall Q1 (λa. Q2)) (forall T1 (λa. T2))] ⇒
let [g ⊢ F1] = trans [g ⊢ Q1] [g ⊢ E1] [g ⊢ D1] in
let [g, b : block (a:tp, tr:{u' : tp} {t' : tp} (sub a u' → sub u' t' → sub a t'), w:sub a T1[…], ref:sub a a) ⊢ F2[…, b.1, b.2, b.3, b.4]] =
trans [g, b : block (a:tp, tr:{u' : tp} {t' : tp} (sub a u' → sub u' t' → sub a t'), w:sub a T1[…], ref:sub a a) ⊢ Q2[…, b.1]] [g, b ⊢ D2[…, b.1, b.2, (b.2 T1[…] Q1[…] b.3 E1[…]), b.4]] [g, b ⊢ E2[…, b.1, b.2, b.3, b.4]] in
[g ⊢ sa_all F1 (λa. λtr. λw. λref. F2)];
We only mark out this special case:
if d1 : [g ⊢ sub (forall S1 (λa.S2)) (forall Q1 (λa.Q2))]
and d2 : [g ⊢ sub (forall Q1 (λa.Q2)) (forall T1 (λa.T2))]
then f : [g ⊢ sub (forall S1 (λa.S2) (forall T1 (λa.T2))]
.
By inversion on d1
, we have:
D1 : [g ⊢ sub Q1 S1]
D2 : [g, b : block (a:tp, tr:{u':tp}{t':tp} sub a u' → sub u' t' → sub a t', w: sub a Q1[…], ref: sub a a ) ⊢ sub S2[… b.1] Q2[…,b.1]]
By inversion on E:
E1 : [g ⊢ sub T1 Q1]
E2 : [g, b : block (a:tp, tr:{u':tp}{t':tp} sub a u' → sub u' t' → sub a t', w: sub a T1, ref: sub a a ) ⊢ sub (Q2 b.1) (T2 b.1)]
By i.h. on E1 and D1 we can obtain a derivation F1 : [g ⊢ sub T1 S1]
.
We would like to obtain another derivation F2 : [g, b : block (a:tp, tr:{u':tp}{t':tp} sub a u' → sub u' t' → sub a t', w: sub a T1[…], ref: sub a a ) ⊢ sub S2[… ,b.1] T2[ … ,b.1]]
. However, applying the induction hypothesis on D2
and E2
will not work
because D2
depends on the assumption w: sub a Q1
while E2
depends
on the assumption w: sub a T1
. We need to first create a derivation D2'
which depends on w: sub a T1[…]
. Recall D2
is a parametric and hypothetical derivation which can be viewed as a function which expects as inputs tr: sub a u' → sub u' t' → sub a t', ref: sub a a
, and an object of type sub a Q1[…]
. In other words, we need to turn a function which expects sub a Q1
into a function which expects an object of type sub a T1
. We use b.2 T1[…] Q1[…] b.3 E1[…]
to achieve this transformation.
LF subtype : tp → tp → type =
| subtype_top : subtype T top
| subtype_refl : subtype T T
| subtype_trans : subtype T1 T2 → subtype T2 T3 → subtype T1 T3
| subtype_arrow : subtype T1 S1 → subtype S2 T2 → subtype (arr S1 S2) (arr T1 T2)
| subtype_forall : subtype T1 S1 → ({x : tp} (subtype x T1 → subtype (S2 x) (T2 x))) → subtype (forall S1 S2) (forall T1 T2);
In order to prove soundness and completeness, we define a new context which includes both algorithmic subtyping and declarative subtyping.
schema ss_ctx = some [u : tp] block (a:tp, tr:{U : tp} {T : tp} (sub a U → sub U T → sub a T), w:sub a u, ref:sub a a, w':subtype a u);
rec sound : (g:ss_ctx) [g ⊢ sub T S] → [g ⊢ subtype T S] =
fn d ⇒ case d of
| [g ⊢ sa_top] ⇒ [g ⊢ subtype_top]
| [g ⊢ sa_arr D1 D2] ⇒
let [g ⊢ E1] = sound [g ⊢ D1] in
let [g ⊢ E2] = sound [g ⊢ D2] in [g ⊢ subtype_arrow E1 E2]
| [g ⊢ sa_all D1 (λa. λtr. λw. λref. D2)] : [g ⊢ sub (forall S1 (λa. S2)) (forall T1 (λa. T2))] ⇒
let [g ⊢ E1] = sound [g ⊢ D1] in
let [g, b : block (a:tp, tr:{u' : tp} {t' : tp} (sub a u' → sub u' t' → sub a t'), w:sub a T1[…], ref:sub a a, w':subtype a T1[…]) ⊢ E2[…, b.1, b.5]] =
sound [g, b : block (a:tp, tr:{u' : tp} {t' : tp} (sub a u' → sub u' t' → sub a t'), w:sub a T1[…], ref:sub a a, w':subtype a T1[…]) ⊢ D2[…, b.1, b.2, b.3, b.4]] in
[g ⊢ subtype_forall E1 (λa. λw. E2)]
| [g ⊢ #p.3] ⇒ [g ⊢ #p.5]
| [g ⊢ #p.4] ⇒ [g ⊢ subtype_refl]
| {#p : [g ⊢ block (a:tp, tr:{u' : tp} {t' : tp} (sub a u' → sub u' t' → sub a t'), w:sub a U'[…], ref:sub a a, w':subtype a U'[…])]}
{D1 : [g ⊢ sub #p.1 U']} [g ⊢ #p.2 U' T' D1 D2] ⇒
let [g ⊢ E1] = sound [g ⊢ D1] in
let [g ⊢ E2] = sound [g ⊢ D2] in [g ⊢ subtype_trans E1 E2];
rec complete : (g:ss_ctx) [g ⊢ subtype T S] → [g ⊢ sub T S] =
fn d ⇒ case d of
| [g ⊢ #p.5] ⇒ [g ⊢ #p.3]
| [g ⊢ subtype_top] ⇒ [g ⊢ sa_top]
| [g ⊢ subtype_refl] ⇒ refl [g] [g ⊢ _]
| [g ⊢ subtype_trans E1 E2] ⇒
let [g ⊢ D1] = complete [g ⊢ E1] in
let [g ⊢ D2] = complete [g ⊢ E2] in trans [g ⊢ _] [g ⊢ D1] [g ⊢ D2]
| [g ⊢ subtype_arrow E1 E2] ⇒
let [g ⊢ D1] = complete [g ⊢ E1] in
let [g ⊢ D2] = complete [g ⊢ E2] in [g ⊢ sa_arr D1 D2]
| [g ⊢ subtype_forall E1 (λx. λy. E2)] : [g ⊢ subtype (forall S1 (λa. S2)) (forall T1 (λa. T2))] ⇒
let [g ⊢ D1] = complete [g ⊢ E1] in
let [g, b : block (a:tp, tr:{u' : tp} {t' : tp} (sub a u' → sub u' t' → sub a t'), w:sub a T1[…], ref:sub a a, w':subtype a T1[…]) ⊢ D2[…, b.1, b.2, b.3, b.4]] =
complete [g, b : block (a:tp, tr:{u' : tp} {t' : tp} (sub a u' → sub u' t' → sub a t'), w:sub a T1[…], ref:sub a a, w':subtype a T1[…]) ⊢ E2[…, b.1, b.5]] in
[g ⊢ sa_all D1 (λa. λtr. λw. λref. D2)];