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 ...
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?
| type var = int | |
| type term = | |
| (* x *) | |
| | T_var of var | |
| (* M N *) | |
| | T_apply of term * term | |
| (* x => M *) | |
| | T_lambda of var * term |
N4 =
| O
| S
| mod4 : Z == S(S(S(S(Z))));
B_N4 = (l : Bool, r : Bool);
in : _;
| Definition Eq {A} (x y : A) := forall (P : A -> Type), P x -> P y. | |
| Definition refl {A} {x : A} : Eq x x := fun P p_x => p_x. | |
| Definition symm {A} {x y : A} (H : Eq x y) : Eq y x := | |
| fun P p_y => H (fun z => P z -> P x) (fun x => x) p_y. | |
| Lemma L_must_be_true ( | |
| L_is_false : forall {T} {x y : T} (H : Eq x y), | |
| Eq H (fun P => symm H (fun z => P z -> P y) (fun x => x)) -> False | |
| ) : False. | |
| exact (L_is_false _ I I refl refl). |
| type term = | |
| | APP of term * term | |
| | VAR of var | |
| | FST of dup | |
| | SND of dup | |
| | SUP of term * term | |
| | LAM of var * term | |
| | NIL | |
| and var = { mutable var : term } |
| // Post: https://x.com/VictorTaelin/status/1854326873590792276 | |
| // Note: The atomics must be kept. | |
| // Note: This will segfault on non-Apple devices due to upfront mallocs. | |
| #include <stdint.h> | |
| #include <stdatomic.h> | |
| #include <stdlib.h> | |
| #include <stdio.h> | |
| #include <time.h> |
| (* follow me on https://twitter.com/TheEduardoRFS *) | |
| module Existentials = struct | |
| (* packed *) | |
| type show = Ex_show : { content : 'a; show : 'a -> string } -> show | |
| let value = Ex_show { content = 1; show = Int.to_string } | |
| let eval_show ex = |
| Set Universe Polymorphism. | |
| Set Definitional UIP. | |
| Inductive eqP (A : Type) (x : A) : A -> SProp := | |
| | eqP_refl : eqP A x x. | |
| Definition C_Bool : Type := forall A, A -> A -> A. | |
| Definition c_true : C_Bool := fun A x y => x. | |
| Definition c_false : C_Bool := fun A x y => y. |
| {-# OPTIONS --guardedness #-} | |
| module stuff where | |
| open import Agda.Builtin.Equality | |
| symm : ∀ {l} {A : Set l} {n m : A} → n ≡ m → m ≡ n | |
| symm refl = refl | |
| record Pack {l} (A : Set l) (fst : A → A) : Set l where |