Ids instance for explicitly typed terms

[radeusgd]

I base the issue on the following assumption: Assumption 1: In the explicitly typed calculus, terms that are contained within other terms are also explicitly typed.

Example: ((fun: A -> B) (arg: A)): B - in this instance of applying fun to arg, not only is the whole Application annotated with types but also the terms that are "inside" are in their annotated versions. An example contradicting Assumption 1: (fun arg): B - in this instance the "inner" terms are still untyped.

Am I right that for the explicitly-typed variant of the calculus, Assumption 1 should hold?

Conjecture 1: It is impossible to derive a meaningful instance of the Ids typeclass for a explicitly typed terms.

Context: Ids (termType: Type) is a typeclass requiring to provide a function ids : var -> termType. If I understand correctly, that function should be an 'identity substitution' which is equivalent to a variable constructor (ref: page 2).

Given Assumption 1, to create a proper Var, we need not only its index but its target type, which is not available in the given context.

We could realize the function with ids (x: var) := Var x TNat which would assign by default type Nat to all variables. But this sounds like simply a wrong thing to do.

I'm however not exactly sure how the Ids instance is used, because I think it may still work for closed terms.

[radeusgd]

For the following program:

Require Import List Omega.
Require Import Autosubst.Autosubst.
Require Import Context.

Inductive type :=
| TNat
| TAbs (t1: type) (t2: type)
| TBox (t: type).

Inductive term :=
| Nat (n : nat) (typ: type)
| Var (x : var) (typ: type)
| Lam (ebody : {bind term}) (typ: type)
| App (e1 e2 : term) (typ: type)
| Lift (e: term) (typ: type)
.

Instance Ids_term : Ids term. constructor 2.
exact H.
exact TNat.
Defined.
Instance Rename_term : Rename term. derive. Defined.
Instance Subst_term : Subst term. derive. Defined.
(* Instance SubstLemmas_term : SubstLemmas term. derive. Defined. *)

Compute (Var 0 (TBox TNat)).[ids].

The computation results in Var 0 TNat but we would expect Var 0 (TBox TNat) - we have erased the type by mistake.

I'm afraid this may make it impossible to use autosubst in the project, unless Assumption 1 was false.

P.S. Moreover the SubstLemmas instance is also not derived automatically and I think that is what autosubst was meant for in the first place, so even if we could derive Ids somehow correctly, it wouldn't help much.

[liufengyun]

The assumption 1 is correct. For conjecture 1, I think you have an insight here, I'm not sure whether it works or not.

In the paper, the term languages have t and u, which are mutually recursive. If we look at u, x is a syntactic form of it, without type. Maybe there is still a chance.

It's not clear why Compute (Var 0 (TBox TNat)).[ids]. returns Var 0 TNat instead of Var 0 (TBox TNat). Do you need someting like the follows:

Instance hsubst_term : HSubst type term. derive. Defined.

[radeusgd]

This sounds like a good idea for a workaround. I cannot define Ids for typedterm, as that would require knowing the type, but maybe I may not need it.

I tried the following definition:

Inductive type :=
| TNat
| TAbs (t1: type) (t2: type)
| TBox (t: type).

Inductive typedterm :=
| TypedTerm (u: term) (t: type)
with
term :=
| Nat (n : nat)
| Var (x : var)
| Lam (argT: type) (ebody : {bind typedterm})
| App (e1 e2 : typedterm)
| Lift (e: term)
.

Instance Ids_term : Ids term. derive. Defined.
Instance Rename_term : Rename term. derive. Defined.
Instance Subst_term : Subst term. derive. Defined.
Instance SubstLemmas_term : SubstLemmas term. derive. Defined.

(* Instance Ids_typedterm : Ids typedterm. derive. Defined. *)
Instance Rename_typedterm : Rename typedterm. derive. Defined.
Instance Subst_typedterm : Subst typedterm. derive. Defined.
(* Instance SubstLemmas_typedterm : SubstLemmas typedterm. derive. Defined. *)

Instance HSubst_termtypedterm : HSubst term typedterm. derive. Defined.
Instance HSubst_termtypedterm2 : HSubst typedterm term. derive. Defined.

Unfortunately:

Compute (TypedTerm (App (TypedTerm (Var 1) (TAbs TNat TNat)) (TypedTerm (Var 0) TNat)) TNat).|[Nat 42/].

yields

TypedTerm
         (App (TypedTerm (Var 1) (TAbs TNat TNat))
            (TypedTerm (Var 0) TNat)) TNat

and not the expected

TypedTerm
         (App (TypedTerm (Var 0) (TAbs TNat TNat))
            (TypedTerm (Nat 42) TNat)) TNat

I may have to experiment further with how to handle this mutual recursion and if it is even possible to make it work with autosubst.

Unfortunately I couldn't find any examples of using autosubst with a mutually recursively defined type.

I conjecture that HSubst is meant for simple nesting but likely not for more complex case of mutual recursion.

For example:

Compute (TypedTerm (Var 0) TNat).|[Nat 42/].

correctly yields

TypedTerm (Nat 42) TNat

I think the issue is the hsubst only visits the term structure inside of the typedterm looking for replacements but it is unable to detect that actually the term can contain other typedterms that should be unpacked recursively.

[radeusgd]

I forgot to answer the issue

t's not clear why Compute (Var 0 (TBox TNat)).[ids]. returns Var 0 TNat instead of Var 0 (TBox TNat).

It is actually expected in terms of how things are defined (although of course not what we need).

t.[ids] is a term with the ids substitution applied ids substitution is a substitution that is supposed to not change the term, but it works by replacing Var N with a fresh instance of Var N (I think that is done mostly for simplifying composability with other substitutions). As ids is defined as a function var -> term where var is just a nat corresponding to the DeBruijn index.

As in our case Var also needs a type, the automatic derivation of Ids instance failed. So we provided it with an implementation that always returns type TNat (as we had to put something here). Of course it is not a good solution as the type will not always be TNat, but we can't do better as the only thing the ids function being defined "knows" is the DeBruijn index which is not enough to deduce the type.

Even if we somehow manage to use the HSubst with the new mutually recursive definition, we can't use ids in subst for the TypedTerm version (but I guess we could use it in the hsubst with ids taken from the untyped version).

[radeusgd]

The workaround suggested by @liufengyun applied with the DbLib library seems to do the trick. We can have an instance of nat -> term that generates untyped VAR and we do substitution of terms inside a context of a typed term.