EduardoRFS

Pi-Sigma-Self

The following is a set of syntax-directed rules to typing a dependently type system with self types. This is hopefully decidable given decidable conversion checking.

The main innovation is that all introduction rules propagate the self due to the new type of checking rule. This allows the fixpoint to be transparent to introductions, when combined with pairs, this leads to mutual recursion and the inductive types.

This doesn't define any universe or restriction to fixpoints, as those are more or less orthogonal to the typing issues here.

Syntax

EduardoRFS

(* index when term, level when value *)
type var = int
type index = int
type level = int

type term =
  (* x *)
  | T_var of { var : var }
  (* x = M; N *)
  | T_let of { arg : term; body : term }

EduardoRFS

{
  "name": "Community-Material-Theme-Darker-High-Contrast",
  "type": "dark",
  "tokenColors": [
    {
      "settings": {
        "background": "#212121",
        "foreground": "#ffffff"
      }
    },

EduardoRFS

Set Universe Polymorphism.

Axiom Path : forall (A : Type), A -> A -> Type.
Axiom refl : forall {A x}, Path A x x.
Axiom transport : forall {A x y} (p : Path A x y),
  forall (P : A -> Type), P x -> P y.

Axiom transport_refl : forall {A x y} (p : Path A x y),
  transport p (fun z => Path A x z) refl = p.
Axiom transport_fst : forall {A x y} (p : Path A x y),

EduardoRFS

Induction-recursion in Impredicative Type Theory

When building universes in a type theory, the standard technique relies on induction-recursion, but Kovács points out that the logical consistency of induction-recursion and induction-induction in the context of impredicative type theory is an open question.

Lastly, we do not handle impredicative universes. The main reason for this is that we do not know the consistency of having induction-recursion and impredicative function space together in the same universe, and modeling impredicativity seems to require this assumption in the metatheory.

Here I will not be providing a mechanized proof, as that is still a work in progress, but two techniques to justify mutual definitions in type theories. The running example will be the following mutual definition, where N depends on the value of x.

x : A;

EduardoRFS

Inductive D : bool -> Type :=
  | c0 : D true
  | c1 : D false.

Lemma prove_me_general b : forall (v : D b),
  v =  match b with | true => c0 | false => c1 end.
Proof.
  intros v.
  induction v; reflexivity.
Qed.

EduardoRFS

(*
  Everything here is really ugly as I didn't clean it,
    some bits come from the Coq-HoTT library.

  The main idea is that given funext and any
    h-set with multiple provably distinct elements.

  Univalence is only used to prove s_true_neq_s_false

  Then by funext you can get the induction principle to contract.

EduardoRFS

Require Import List.
Import ListNotations.
Require Import Bool.
Require Import PeanoNat.
Require Import Lia.

Definition Index := nat.
Definition Level := nat.

Inductive Term :=

EduardoRFS

Self Types + Sigma for Induction

This is a different technique that can be used for self types in more traditional MLTT settings, by doing induction through pairs instead of functions.

This idea was inspired by a comment from Ryan Brewer on the PLD Discord server. Paraphrasing it something, something inductive types positives so pairs.

edit: As pointed out by Ryan Brewer, I hallucinated half of the message ...

Self Typed Booleans

EduardoRFS

Positive vs Negative encoded streams

This shows some relations between positively and negatively encoded streams using self types, at the end we conclude that one is definitionally equal to the other if sigma is also encoded as an inductive type with self types.

I would claim that given the relation here, any advantage of one over the other is a matter of ergonomics and the implementation quality.

A nice bit to think later is about extensionalities of those?

So, what did Coq and Agda got wrong?