subtyping

Subtyping

Define a subtyping relationship <:.

Type T1 is a subtype of T2 is denoted as T1 <: T2 or, in MeTTa format

(<: T1 T2)

Algebraic Laws

The subtyping relationship is:

• Reflexive:

  ⊢ T <: T
  

• Transitive:

  T1 <: T2
  T2 <: T3
  ⊢
  T1 <: T3
  

• Contravariant over inputs and covariant over outputs:

  T1 <: S1
  S2 <: T2
  ⊢
  S1 -> S2 <: T1 -> T2
  

Relationships between Subtyping and Typing

There are two variants of relationship between subtyping and type, one using explicit coercion, the other using implicit coercion.

Explicit Coercion

For explicit coercion, the inference rule is the coercion function itself, see coerce defined in rule-base.metta.

Implicit Coercion

Because MeTTa supports non-determinism we can also do implicit type coercion. In that case the typing relationship is treated itself as type, and its witness is an inference rule, not a coercion function, see STImplCoer defined in rule-base.metta.

Conclusion

From that experiment we can conclude the following:

1. Subtyping is possible with MeTTa.
2. Explicit coercion allows to treat programs (in that case coercion functions) on the same level as proofs, in a Curry-Howard correspondence fashion.
3. Implicit coercion has the advantage of not requiring a coercion function, but does not treat functions on the same level as proofs.