James Tan Juan Whei pushed to branch quotient-types at Stefan / Typer
Commits: 61d01f99 by James Tan at 2023-07-19T22:16:16-04:00 Implement `Quotient` formation
- - - - - 1282e0ba by James Tan at 2023-07-19T22:16:16-04:00 Implement `Quotient` introduction
- - - - - 00341dfd by James Tan at 2023-07-19T22:16:17-04:00 Implement `Quotient` elimination
- - - - - 55c38d85 by James Tan at 2023-07-19T22:16:17-04:00 Implement `Eq` constructor for `Quotient`
- - - - - aa04cc68 by James Tan at 2023-07-19T22:16:17-04:00 Improve unification scheme for SLlub (l1, l2) when l1 ≃ l2
- - - - - d00058fa by James Tan at 2023-07-26T19:34:39-04:00 Implement `qcase` macro - Facilitates `Quotient` elimination
- - - - - 48982943 by James Tan at 2023-07-26T19:34:40-04:00 Write some proofs about quotient types
- - - - -
12 changed files:
- btl/builtins.typer - btl/pervasive.typer - + btl/qcase.typer - + samples/qcase_test.typer - + samples/quotient.typer - + samples/quotient_lib.typer - src/debruijn.ml - src/env.ml - src/eval.ml - src/opslexp.ml - src/unification.ml - tests/elab_test.ml
Changes:
===================================== btl/builtins.typer ===================================== @@ -531,4 +531,42 @@ Heap_unsafe-store-cell = Built-in "Heap.store-cell"; Heap_unsafe-load-cell : Int -> Int -> Heap ?t; Heap_unsafe-load-cell = Built-in "Heap.load-cell";
+%% +%% Quotient types +%% +Quotient = Built-in "Quotient" : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> + (A : Type_ l1) -> (R : A -> A -> Type_ l2) -> + Type_ (_∪_ l1 l2); + +Quotient_in : ?A -> Quotient ?A ?R; +Quotient_in = Built-in "Quotient.in"; + +%% FIXME: We want to be able to say the following +%% Quotient_eq : (a : ?) ≡> (a' : ?) ≡> (p : ?R a a') ≡> +%% Eq (Quotient_in (R := R?) a) +%% (Quotient_in (R := R?) a'); +%% But we running into the following issue for now: +%% "Bug in the elaboration of a repeated metavar!" +Quotient_eq : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) ≡> + (R : A -> A -> Type_ l2) ≡> + (a : A) ≡> (a' : A) ≡> (p : R a a') -> + Eq (Quotient_in (R := R) a) + (Quotient_in (R := R) a'); +Quotient_eq = Built-in "Quotient.eq"; + +%% FIXME: We want to be able to say the following +%% Quotient_elim : (f : ?A -> ?B) -> +%% (p : (a : ?) -> (a' : ?) -> ?R a a' -> Eq (f a) (f a')) ≡> +%% (q : Quotient ?A ?R) -> +%% ?B; +%% Same issue as above +Quotient_elim : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (l3 : TypeLevel) ≡> + (A : Type_ l1) ≡> (B : Type_ l2) ≡> + (R : A -> A -> Type_ l3) ≡> + (f : A -> B) -> + (p : (a : A) -> (a' : A) -> R a a' -> Eq (f a) (f a')) ≡> + (q : Quotient A R) -> + B; +Quotient_elim = Built-in "Quotient.elim"; + %%% builtins.typer ends here.
===================================== btl/pervasive.typer ===================================== @@ -690,6 +690,9 @@ depelim = load "btl/depelim.typer"; case_as_return_ = depelim.case_as_return_; case_return_ = depelim.case_return_;
+define-operator "qcase" () 42; +qcase_ = let lib = load "btl/qcase.typer" in lib.qcase_macro; + %%%% Unit tests function for doing file
%% It's hard to do a primitive which execute test file
===================================== btl/qcase.typer ===================================== @@ -0,0 +1,284 @@ +%% Qcase macro +%% Make the syntax cleaner for quotient eliminations +%% +%% qcase (e : A / R) +%% | Quotient_in a => e1 +%% | Quotient_eq a a' r i => e2 +%% +%% `a` is bounded in `e1`, and `a`, `a'`, `r` and `i` are +%% bounded in `e2`. `i` can only be used in an erasable manner. +%% +%% TODO: The annotation is necessary for now, as we need the `R` +%% However, we should make it optional. +is_sym : Sexp -> String -> Bool; +is_sym sexp s = + let + kfalse = K false; + in + Sexp_dispatch sexp + (lambda _ _ -> false) % Nodes + (String_eq s) % Symbol + kfalse % String + kfalse % Integer + kfalse % Float + kfalse; % List of Sexp +%% (build_explicit_arg "name" sexp) yields a +%% (name := sexp) Sexp +build_explicit_arg : String -> Sexp -> Sexp; +build_explicit_arg s sexp = Sexp_node (Sexp_symbol "_:=_") + (cons (Sexp_symbol s) + (cons sexp nil)); +qcase_impl = lambda (sexps : List Sexp) -> + %% For the same example that was given above, we expect + %% `sexps` to represent the following: + %% (_|_ (_:_ e (_/_ A R)) + %% (_=>_ (Quotient_in a) e1) + %% (_=>_ (Quotient_eq a a' r i) e2)) + %% Node : [(_|_ (_:_ e (_/_ A R)) (_=>_ (Qin a) e1) (_=>_ (Qeq a a' r i) e2))] + let + %% (_|_ (_:_ e (_/_ A R)) (_=>_ (Qin a) e1) (_=>_ (Qeq a a' r i) e2)) + head = List_head Sexp_error sexps; + knil = K nil; + kerr = K Sexp_error; + get-list : Sexp -> List Sexp; + get-list node = Sexp_dispatch node + (lambda op lst -> lst) % Nodes + knil % Symbol + knil % String + knil % Integer + knil % Float + knil; % List of Sexp + %% List of: + %% (_:_ e (_/_ A R)) + %% (_=>_ (Qin a) e1) + %% (_=>_ (Qeq a a' r i) e2) + body = get-list head; + elim_targ_sexp = List_nth (Integer->Int 0) body Sexp_error; + elim_fn_sexp = List_nth (Integer->Int 1) body Sexp_error; + elim_compat_sexp = List_nth (Integer->Int 2) body Sexp_error; + %% Triple of the expression to eliminate, the underlying type A + %% and the relation R + %% A and R are optional + elim_expr_details : Triplet Sexp (Option Sexp) (Option Sexp); + elim_expr_details = + let + kerr = K (triplet Sexp_error none none); + extract_from_annotated_e : Sexp -> List Sexp -> + Triplet Sexp (Option Sexp) (Option Sexp); + extract_from_annotated_e _ xs = + if (Int_eq (List_length xs) (Integer->Int 2)) + then + let + e = List_nth (Integer->Int 0) xs Sexp_error; + e_type = List_nth (Integer->Int 1) xs Sexp_error; + extract_type sexp sexps = + if (is_sym sexp "_/_") + then + %% (_/_ A R ) + %% |___| |___| + %% | | + %% a r + let + a = List_nth (Integer->Int 0) sexps Sexp_error; + r = List_nth (Integer->Int 1) sexps Sexp_error; + in + triplet e (some a) (some r) + else + triplet e (some Sexp_error) (some Sexp_error); + kerr' = K (triplet e (some Sexp_error) (some Sexp_error)); + in + Sexp_dispatch e_type + extract_type % Nodes + kerr' % Symbol + kerr' % String + kerr' % Integer + kerr' % Float + kerr' % List of Sexp + else + triplet Sexp_error none none; + extract_targ_from_node : Sexp -> List Sexp -> + Triplet Sexp (Option Sexp) (Option Sexp); + extract_targ_from_node x xs = + %% Check if annotation is present + if (is_sym x "_:_") + then + %% Dissect the sexp to extract, the e, A and R + extract_from_annotated_e x xs + else + %% No annotation was given, return the entire + %% expresson as the elimination target + triplet x none none; + in + Sexp_dispatch elim_targ_sexp + extract_targ_from_node % Nodes + (lambda _ -> triplet elim_targ_sexp + none none) % Symbol + kerr % String + kerr % Integer + kerr % Float + kerr; % List of Sexp + %% The function (`f`) argument + elim_fn : Sexp; + elim_fn = + let + extract_fn : Sexp -> List Sexp -> Sexp; + extract_fn sexp sexps = + %% Check that branch is well formed + if (and (is_sym sexp "_=>_") (Int_eq (List_length sexps) (Integer->Int 2))) + then + let + %% (_=>_ (Quotient_in a) e1 ) + %% |_____________| |_________| + %% | | + %% qin fn_body + qin_sexp = List_nth (Integer->Int 0) sexps Sexp_error; + fn_body_sexp = List_nth (Integer->Int 1) sexps Sexp_error; + bound_var : Sexp; + bound_var = + let + extract_var head args = if (and (is_sym head "Quotient_in") + (Int_eq (List_length args) + (Integer->Int 1))) + then + List_head Sexp_error args + else + %% FIXME: Might be good to have + %% a better way to report this + Sexp_error; + in + Sexp_dispatch qin_sexp + extract_var % Nodes + kerr % Symbol + kerr % String + kerr % Integer + kerr % Float + kerr; % List of Sexp + in + Sexp_node (Sexp_symbol "lambda_->_") + (cons bound_var + (cons fn_body_sexp nil)) + else Sexp_error; + in + Sexp_dispatch elim_fn_sexp + extract_fn % Nodes + kerr % Symbol + kerr % String + kerr % Integer + kerr % Float + kerr; % List of Sexp + %% The proof (`p`) argument + elim_compat : Sexp; + elim_compat = + let + extract_proof : Sexp -> List Sexp -> Sexp; + extract_proof sexp sexps = + %% Check that branch is well formed + if (and (is_sym sexp "_=>_") (Int_eq (List_length sexps) + (Integer->Int 2))) + then + let + %% (_=>_ (Quotient_eq a a' r i) p ) + %% |____________________| |__________| + %% | | + %% qeq proof_exp + qeq_sexp = List_nth (Integer->Int 0) sexps Sexp_error; + proof_exp_sexp = List_nth (Integer->Int 1) sexps Sexp_error; + is_symbol : Sexp -> Bool; + is_symbol sexp = + let + ktrue = K true; + kfalse = K false; + in + Sexp_dispatch sexp + (K kfalse) % Nodes + ktrue % Symbol + kfalse % String + kfalse % Integer + kfalse % Float + kfalse; % List of Sexp + build_proof : Sexp -> List Sexp -> Sexp; + build_proof sexp sexps = + %% Check that the right identifier is used with exactly + %% 4 arguments, also ensure that identifier are symbols + %% TODO: Make it possible to omit the `i`, in which case + %% we expect p to be an equality proof. + if (and (is_sym sexp "Quotient_eq") + (and %% We allow the last parameter `i` to be omitted + (or (Int_eq (List_length sexps) (Integer->Int 3)) + (Int_eq (List_length sexps) (Integer->Int 4))) + (List_foldl (lambda acc sexp -> + and acc (is_symbol sexp)) + true sexps))) + then + let + mklambda : Sexp -> Sexp -> Sexp; + mklambda param body = + Sexp_node (Sexp_symbol "lambda_->_") + (cons param (cons body nil)); + proof_fn = + if (Int_eq (List_length sexps) (Integer->Int 3)) + then + %% `i` is absent, i.e. we expect to be provided + %% with an equality proof. + %% We want to convert Quotient_eq a a' r => e + %% to (lambda a a' r -> e) + quote (uquote (List_foldr mklambda + sexps proof_exp_sexp)) + else + %% Handle the case where `i` is present + %% We have to construct an equality proof + %% from what was given + %% We want to convert Quotient_eq a a' r i => e + %% to (lambda a a' r -> Eq_eq (f := lambda i ≡> e)) + let + erasable_param = List_nth (Integer->Int 3) + sexps Sexp_error; + proof_fn_params = + List_reverse (List_tail (List_reverse sexps nil)) + nil; + eq = quote (Eq_eq (f := + lambda (uquote erasable_param) ≡> + (uquote proof_exp_sexp))); + in + quote (uquote (List_foldr mklambda + proof_fn_params eq)); + in + build_explicit_arg "p" proof_fn + else + Sexp_error; + in + Sexp_dispatch qeq_sexp + build_proof % Nodes + kerr % Symbol + kerr % String + kerr % Integer + kerr % Float + kerr % List of Sexp + else + Sexp_error; + in + Sexp_dispatch elim_compat_sexp + extract_proof % Nodes + kerr % Symbol + kerr % String + kerr % Integer + kerr % Float + kerr; % List of Sexp + qelim_args : List Sexp; + qelim_args = case elim_expr_details + | triplet e a r => + let + res = (cons elim_fn + (cons elim_compat + (cons e nil))); + res' = (case r + | none => res + | some r' => + (cons (build_explicit_arg "R" r') res)); + in + res'; + qelim_sexp = Sexp_node (Sexp_symbol "Quotient_elim") + qelim_args; + in + IO_return qelim_sexp; +qcase_macro = macro qcase_impl;
===================================== samples/qcase_test.typer ===================================== @@ -0,0 +1,50 @@ +%% Defining a total relation on Unit +R : Unit -> Unit -> Type; +R u1 u2 = Unit; + +inQ : Quotient Unit R; +inQ = Quotient_in (); + +e1 : Unit; +e1 = qcase (inQ : Unit / R) + | Quotient_in a => () + | Quotient_eq a a' r i => (); + +e2 : Unit; +e2 = qcase (inQ : Unit / R) + | Quotient_in a => () + | Quotient_eq a a' r => Eq_refl; + +e3 : Unit; +e3 = qcase inQ + | Quotient_in a => () + | Quotient_eq a a' r i => (); + +e4 : Unit; +e4 = qcase inQ + | Quotient_in a => () + | Quotient_eq a a' r => Eq_refl; + +test-elim-to-unit = do { + Test_info "QCASE" "elimination to Unit"; + + r0 <- Test_eq "annotated elim to `Unit` with explicit `I`" e1 (); + r1 <- Test_eq "annotated elim to `Unit` without `I`" e2 (); + r2 <- Test_eq "unannotated elim to `Unit` with explicit `I`" e3 (); + r3 <- Test_eq "unannotated elim to `Unit` without `I`" e4 (); + + success <- IO_return (and (and (and r0 r1) r2) r3); + + if success then + (Test_info "QCASE" "elimination to Unit succeeded") + else + (Test_warning "QCASE" "elimination to Unit failed"); + + IO_return success; +}; + +exec-test = do { + b1 <- test-elim-to-unit; + + IO_return b1; +};
===================================== samples/quotient.typer ===================================== @@ -0,0 +1,116 @@ +Nat : Type; + +type Nat + | zero + | succ Nat; + +_-_ : Nat -> Nat -> Nat; +_-_ x y = case x + | zero => zero + | succ m => case y + | zero => x + | succ n => m - n; + +NatPair = Pair Nat Nat; + +fst p = case p + | pair m _ => m; + +snd p = case p + | pair _ n => n; + +normaliseZ : NatPair -> NatPair; +normaliseZ np = case np + | pair m n => pair (m - n) (n - m); + +equalZ : NatPair -> NatPair -> Type; +equalZ x1 x2 = Eq (normaliseZ x1) (normaliseZ x2); + +%% +%% See definitions of `Quotient` in `builtins.typer` +%% + +%% FIXME: We shouldn't get this error +%% "Requested Built-in "Quotient" does not exist" +%% Z = Quotient NatPair equalZ; + +%% +%% Quotient.eq +%% +%% Proof that quotiented elements are equal when +%% the base elements themselves are related in +%% the underlying type. +𝟙-𝟘 : Quotient NatPair equalZ; +𝟙-𝟘 = Quotient_in (pair (succ zero) zero); + +𝟚-𝟙 : Quotient NatPair equalZ; +𝟚-𝟙 = Quotient_in (pair (succ (succ zero)) (succ zero)); + +𝟙=𝟙 : Eq (t := Quotient NatPair equalZ) 𝟙-𝟘 𝟚-𝟙; +𝟙=𝟙 = Quotient_eq + (R := equalZ) + (a := pair (succ zero) zero) + (a' := pair (succ (succ zero)) (succ zero)) + Eq_refl; + +%% +%% Quotient.elim +%% +%% Elimination of quotients requires a proof that +%% the equality between quotients is respected +NatToInt : Nat -> Int; +NatToInt n = case n + | zero => 0 + | succ n' => 1 + NatToInt n'; + +NatPairToInt' : NatPair -> Int; +NatPairToInt' np = case np + | pair x y => + (case x + | zero => (NatToInt y) * -1 + | succ _ => NatToInt x); + +NatPairToInt : NatPair -> Int; +NatPairToInt np = NatPairToInt' (normaliseZ np); + +%% Proof that NatPairToInt respects the quotient Z +NatPairToIntCompat : (a : NatPair) -> (a' : NatPair) -> + (p : equalZ a a') -> + Eq (NatPairToInt a) (NatPairToInt a'); +NatPairToIntCompat _ _ p = Eq_eq (f := lambda i ≡> + NatPairToInt' (Eq_uneq (p := p) (i := i))); + +%% FIXME: Explicitly providing a value for R should unnecessary, +%% this should be inferred based on the type of `q`. This is +%% because we do not handle residuals during unification for now. +Z_To_Int : Quotient NatPair equalZ -> Int; +Z_To_Int q = Quotient_elim (R := equalZ) NatPairToInt (p := NatPairToIntCompat) q; + +neg2_Z : Quotient NatPair equalZ; +neg2_Z = Quotient_in (pair (succ zero) (succ (succ (succ zero)))); + +neg2_Int : Int; +neg2_Int = Z_To_Int neg2_Z; + +%% FIXME: This could work if we add a reduction rule +%% neg2_refl : Eq neg2_Int (-2 : Int); +%% neg2_refl = Eq_refl; + +%% `qcase` macro to facilitate elimination +Z_To_Int' : Quotient NatPair equalZ -> Int; +Z_To_Int' q = + %% The annotation is optional, but is necessary in + %% this case, since the propagation of type + %% information is insufficient the way things are now. + qcase (q : NatPair / equalZ) + | Quotient_in a => NatPairToInt a + | Quotient_eq a a' r i => NatPairToInt' (Eq_uneq (p := r) (i := i)); + +%% Omitting the `i` parameter by providing an equality proof on the RHS +Z_To_Int'' : Quotient NatPair equalZ -> Int; +Z_To_Int'' q = + qcase (q : NatPair / equalZ) + | Quotient_in a => NatPairToInt a + | Quotient_eq a a' r => NatPairToIntCompat a a' r; + +%% TODO: Define Quotient NatPair equalZ ≃ Int
===================================== samples/quotient_lib.typer ===================================== @@ -0,0 +1,129 @@ +%%%%% Prelude %%%%%% + +%% FIXME : Loading hott.typer doesn't work for some reason +%% due to "[X] Fatal :(internal) lub of two SLsucc" +%% Some definitions will be duplicated for now + +Eq_funext : (f : ? -> ?) => (g : ? -> ?) => + ((x : ?) -> Eq (f x) (g x)) -> + Eq f g; +Eq_funext p = Eq_eq (f := lambda i ≡> lambda x -> Eq_uneq (p := p x) (i := i)); + +HoTT_isProp P = (x : P) -> (y : P) -> Eq x y; + +HoTT_isSet A = (x : A) -> (y : A) -> HoTT_isProp (Eq x y); + +HoTT_isContr = typecons (HoTT_isContr (l ::: TypeLevel) + (A : Type_ l)) + (isContr (a : A) ((a' : A) -> Eq a a')); +isContr = datacons HoTT_isContr isContr; + +%%%%% Prelude END %%%%%% + +%% TODO: Prove dependent version of this after we introduce +%% dependent elim, which will be more interesting and more +%% worthwhile +recProp : (A : Type_ ?) ≡> + (B : Type_ ?) ≡> + (R : A -> A -> Type_ ?) ≡> + (p : HoTT_isProp B) -> + (f : A -> B) -> + (x : Quotient A R) -> B; +recProp = lambda _ _ _ _ _ R ≡> + lambda p f x -> + Quotient_elim (R := R) f (p := lambda a a' r -> p (f a) (f a')) x; + +%% Again, this is not very interesting, unlike its dependent +%% counterpart. +recContr : (A : Type_ ?) ≡> + (B : Type_ ?) ≡> + (R : A -> A -> Type_ ?) ≡> + (p : HoTT_isContr B) -> + (x : Quotient A R) -> B; +recContr = lambda _ _ _ _ _ R ≡> + lambda p x -> case p + | isContr a f => Quotient_elim (R := R) + (lambda _ -> a) + (p := lambda a a' r -> Eq_refl) + x; + +%% FIXME: Quotient_elim should be named Quotient_rec? +%% rec2 : (A : Type_ ?) ≡> +%% (B : Type_ ?) ≡> +%% (C : Type_ ?) ≡> +%% (R : A -> A -> Type_ ?) ≡> +%% (S : B -> B -> Type_ ?) ≡> +%% (C_isSet : HoTT_isSet C) -> +%% (f : A -> B -> C) -> +%% ((a : A) -> (b : A) -> (c : B) -> R a b -> Eq (f a c) (f b c)) -> +%% ((a : A) -> (b : B) -> (c : B) -> S b c -> Eq (f a b) (f a c)) -> +%% Quotient A R -> Quotient B S -> C; +%% rec2 = lambda _ _ _ _ _ A B C R S ≡> +%% lambda C_isSet f feql feqr -> +%% Quotient_elim (R := R) +%% (lambda a -> +%% lambda b -> Quotient_elim (R := S) (f a) +%% (p := feqr a) b) +%% (p := lambda a a' r -> +%% let +%% eqf : (b : B) -> Eq (f a b) (f a' b); +%% eqf b = feql a a' b r; +%% eqf' : Eq (f a) (f a'); +%% eqf' = Eq_funext (f := f a) (g := f a') eqf; +%% p : (x : Quotient B S) -> +%% HoTT_isProp (Eq (Quotient_elim (R := S) (f a) +%% (p := feqr a) x) +%% (Quotient_elim (R := S) (f a') +%% (p := feqr a') x)); +%% p x = C_isSet (Quotient_elim (R := S) (f a) +%% (p := feqr a) x) +%% (Quotient_elim (R := S) (f a') +%% (p := feqr a') x); +%% res : (x : Quotient B S) -> +%% (Eq (Quotient_elim (R := S) (f a) +%% (p := feqr a) x) +%% (Quotient_elim (R := S) (f a') +%% (p := feqr a') x)); +%% res x = Quotient_elim (A := B) +%% %% FIXME: We need depelim here +%% (B := Eq (f a b) (f a' b)) +%% (R := S) +%% eqf +%% (p := lambda u v s -> +%% Eq_eq (f := lambda i ≡> +%% p (Eq_uneq (p := Quotient_eq (R := S) s) (i := i)) +%% (eqf u) (eqf v))) +%% x; +%% in +%% Eq_funext (f := Quotient_elim (R := S) (f a) +%% (p := feqr a)) +%% (g := Quotient_elim (R := S) (f a') +%% (p := feqr a')) +%% res); + +%% Lemma 6.10.2 in HoTT book, to prove this we need to +%% apply propositional truncation on SurjectiveQuotientProof. +%% type SurjectiveQuotientProof (A : ?) (x : Quotient A ?R) +%% | surjectiveQuotientProof (a : A) (Eq (Quotient_in a) x); +%% Quotient_in_surjective : (x : Quotient ?A ?R) -> ||SurjectiveQuotientProof ?A ?R x||₁; + +%% Given a proof that a unary operation preserves the underlying +%% relation, we can apply the operation to the quotiented type. +quotUnaryOp : (A : Type_ ?) ≡> + (R : A -> A -> Type_ ?) ≡> + (op : A -> A) -> + ((a : A) -> (a' : A) -> R a a' -> R (op a) (op a')) -> + Quotient A R -> Quotient A R; +quotUnaryOp = lambda _ _ A R ≡> + lambda op h x -> + let + opPreservesQuotient : (a : A) -> (a' : A) -> R a a' -> + Eq (t := Quotient A R) + (Quotient_in (op a)) + (Quotient_in (op a')); + opPreservesQuotient a a' r = Quotient_eq (R := R) (h a a' r); + in + Quotient_elim (R := R) + (lambda a -> Quotient_in (op a)) + (p := opPreservesQuotient) + x;
===================================== src/debruijn.ml ===================================== @@ -145,7 +145,7 @@ let type_eq_type = let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type)
let builtin_axioms = - ["Int"; "Elab_Context"; "IO"; "Ref"; "Sexp"; "Array"; "FileHandle"; + ["Int"; "Elab_Context"; "IO"; "Ref"; "Sexp"; "Array"; "FileHandle"; "Quotient"; (* From `healp.ml`. *) "Heap"; "DataconsLabel"]
===================================== src/env.ml ===================================== @@ -184,7 +184,12 @@ let value_string_with_type v ltype ctx = (Lexp.to_string left) (Lexp.to_string right) (Lexp.to_string t) - | _ -> value_string v) + | [_; _; (_, t); (_, r)] + when OL.conv_builtin_p ctx e' "Quotient" + -> sprintf "(Quotient.in %s %s)" + (Lexp.to_string t) + (Lexp.to_string r) + | _ -> value_string v) | _ -> value_string v in get_string ltype ctx
===================================== src/eval.ml ===================================== @@ -1027,6 +1027,18 @@ let typelevel_lub loc (_depth : eval_debug_info) (args_val: value_type list) = | [Vint v1; Vint v2] -> Vint(max v1 v2) | _ -> error loc ("`Typlevel.⊔` expects 2 TypeLevel argument2")
+let quotient_elim loc depth args = + let trace_dum = (Var ((epsilon (loc), None), -1)) in + match args with + | [(Closure _) as f; q] -> + eval_call loc trace_dum depth f [q] + | _ -> error loc "Quotient.elim expects 2 arguments" + +let quotient_eq loc _ args = + match args with + | [_] -> Vundefined + | _ -> error loc "Quotient.eq expects 1 argument" + let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ @@ -1084,6 +1096,9 @@ let register_builtin_functions () = ("Test.false" , test_false,2); ("Test.eq" , test_eq,3); ("Test.neq" , test_neq,3); + ("Quotient.in" , nop_fun, 1); + ("Quotient.eq" , quotient_eq, 1); + ("Quotient.elim" , quotient_elim, 2); ] let _ = register_builtin_functions ()
===================================== src/opslexp.ml ===================================== @@ -304,7 +304,9 @@ and eq_cast_whnf ctx args = match args with | _l1 :: _l2 :: _t :: _x :: _y :: (_, p) :: _f :: (_, fx) :: rest -> (match lexp'_whnf p ctx with - | Call (_, eq, _) when conv_builtin_p ctx eq "Eq.eq" + | Call (_, eq, _) + when conv_builtin_p ctx eq "Eq.eq" || + conv_builtin_p ctx eq "Quotient.eq" -> Some (fx, rest) | _ -> None) | _ -> None
===================================== src/unification.ml ===================================== @@ -561,6 +561,10 @@ and unify_sortlvl (matching : scope_level option) -> (* FIXME: This SLlub representation needs to be * more "canonicalized" otherwise it's too restrictive! *) (unify' l11 l21 ctx vs matching)@(unify' l12 l22 ctx vs matching) + | SLlub (l1, l2), other | other, SLlub (l1, l2) + when OL.conv_p ctx l1 l2 + (* Arbitrarily selected `l1` over `l2` *) + -> unify' l1 (mkSortLevel other) ctx vs matching | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]) | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]
===================================== tests/elab_test.ml ===================================== @@ -180,7 +180,7 @@ unify (f Z (S Z)) (f (S Z) Z); |}
let _ = add_elab_test_decl - "WHNF of Eq.cast" + "WHNF of Eq.cast (applied to Eq.eq)" {| x = (4 : Int); y = x; @@ -192,6 +192,28 @@ test : Eq (Eq_cast (p := p) (f := lambda _ -> Unit) ()) (); test = Eq_refl; |}
+let _ = add_elab_test_decl + "WHNF of Eq.cast (applied to Quotient.eq)" + {| +totalRel : Unit -> Unit -> Type; +totalRel u1 u2 = Unit; + +unitQ : Quotient Unit totalRel; +unitQ = Quotient_in unit; + +unitQ' = unitQ; + +unitQ=unitQ' : Eq (t := Quotient Unit totalRel) unitQ unitQ'; +unitQ=unitQ' = Quotient_eq + (R := totalRel) + (a := unit) + (a' := unit) + unit; + +test : Eq (Eq_cast (p := unitQ=unitQ') (f := lambda _ -> Unit) ()) (); +test = Eq_refl; + |} + let _ = add_elab_test_decl "Decidable at the type level" {|
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/bfbff550912f1de9c0b1d61e494c2ac73...
Afficher les réponses par date
Voici quelques commentaires sur les commits sur cette branche (sous la forme de "# FIXME: ..blabla...", quoique c'est pas tous des "fixme").
Stefan
Merci pour les commentaires, je viens de faire les changements nécessaires et c’est déjà poussé sur Git.
James
Le 14 août 2023 à 10:17, Stefan Monnier monnier@iro.umontreal.ca a écrit :
Voici quelques commentaires sur les commits sur cette branche (sous la forme de "# FIXME: ..blabla...", quoique c'est pas tous des "fixme").
Stefancommit 61d01f99e741c75520814dea2e643121bca83374 Author: James Tan james_tan97@outlook.com Date: Sun Jul 2 21:15:55 2023 -0400
Implement `Quotient` formation
diff --git a/btl/builtins.typer b/btl/builtins.typer index 228999b..5ec79b0 100644 --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -531,4 +531,11 @@ Heap_unsafe-store-cell = Built-in "Heap.store-cell"; Heap_unsafe-load-cell : Int -> Int -> Heap ?t; Heap_unsafe-load-cell = Built-in "Heap.load-cell";
+%% +%% Quotient types +%% +Quotient = Built-in "Quotient" : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡>
(A : Type_ l1) -> (R : A -> A -> Type_ l2) ->Type_ (_∪_ l1 l2);%%% builtins.typer ends here. diff --git a/samples/quotient.typer b/samples/quotient.typer new file mode 100644 index 0000000..1108133 --- /dev/null +++ b/samples/quotient.typer @@ -0,0 +1,33 @@ +Nat : Type;
+type Nat
- | zero
- | succ Nat;
# # FIXME: Can we take this from elsewhere instead?
+_-_ : Nat -> Nat -> Nat; +_-_ x y = case x
- | zero => y
- | succ m => case y
| zero => x| succ n => m - n;+NatPair = Pair Nat Nat;
+fst p = case p
- | pair m _ => m;
+snd p = case p
- | pair _ n => n;
+normaliseZ : NatPair -> NatPair; +normaliseZ np = case np
- | pair m n => pair (m - n) (n - m);
+equalZ : NatPair -> NatPair -> Type; +equalZ x1 x2 = Pair (Eq (fst x1) (snd x2)) (Eq (snd x1) (fst x2)); # # FIXME: normaliseZ is not used? # FIXME: Shouldn't we define a generic "Quotient by normalization function" # first and then define Z using that?
+%% FIXME: We shouldn't get this error +%% "Requested Built-in "Quotient" does not exist" +%% Z = Quotient (A := NatPair) equalZ;
+%% TODO: Intro and elim \ No newline at end of file # # FIXME: "No newline at end of file" # diff --git a/src/debruijn.ml b/src/debruijn.ml index c2efce7..255d82b 100644 --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -145,7 +145,7 @@ let type_eq_type = let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type)
let builtin_axioms =
- ["Int"; "Elab_Context"; "IO"; "Ref"; "Sexp"; "Array"; "FileHandle";
- ["Int"; "Elab_Context"; "IO"; "Ref"; "Sexp"; "Array"; "FileHandle"; "Quotient"; (* From `healp.ml`. *) "Heap"; "DataconsLabel"]
commit 1282e0bab0833e9267701dbc4bd4619961c11308 Author: James Tan james_tan97@outlook.com Date: Tue Jul 11 02:01:17 2023 -0400
Implement `Quotient` introduction
diff --git a/btl/builtins.typer b/btl/builtins.typer index 5ec79b0..53c0bce 100644 --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -538,3 +538,6 @@ Quotient = Built-in "Quotient" : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) -> (R : A -> A -> Type_ l2) -> Type_ (_∪_ l1 l2);
+Quotient_in : ?A -> Quotient ?A ?R; +Quotient_in = Built-in "Quotient.in";
# FIXME: Yay! Tous les arguments implicites sont inférés! # %%% builtins.typer ends here. diff --git a/samples/quotient.typer b/samples/quotient.typer index 1108133..a424bf0 100644 --- a/samples/quotient.typer +++ b/samples/quotient.typer @@ -26,8 +26,21 @@ normaliseZ np = case np equalZ : NatPair -> NatPair -> Type; equalZ x1 x2 = Pair (Eq (fst x1) (snd x2)) (Eq (snd x1) (fst x2));
+%% See definition in `builtins.typer` +%% Quotient : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) -> +%% (R : A -> A -> Type_ l2) -> Type_ (TypeLevel_⊔ l1 l2) +%% +%% Quotient_in : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) ≡> +%% A -> (R : A -> A -> Type_ l2) => Quotient A R
%% FIXME: We shouldn't get this error %% "Requested Built-in "Quotient" does not exist" -%% Z = Quotient (A := NatPair) equalZ; +%% Z = Quotient NatPair equalZ;
+Z_To_Int : Quotient NatPair equalZ -> Int; +Z_To_Int q = 5 : Int; # # FIXME: 5, really?
+test : Int; +test = Z_To_Int (Quotient_in (pair zero zero));
-%% TODO: Intro and elim \ No newline at end of file +%% TODO: Elim diff --git a/src/env.ml b/src/env.ml index 2f5f05e..c9781c1 100644 --- a/src/env.ml +++ b/src/env.ml @@ -184,7 +184,12 @@ let value_string_with_type v ltype ctx = (Lexp.to_string left) (Lexp.to_string right) (Lexp.to_string t)
| _ -> value_string v)
| [_; _; (_, t); (_, r)]when OL.conv_builtin_p ctx e' "Quotient"-> sprintf "(Quotient.in %s %s)"(Lexp.to_string t)(Lexp.to_string r) in get_string ltype ctx| _ -> value_string v) | _ -> value_string vdiff --git a/src/eval.ml b/src/eval.ml index 6385605..9d82577 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -1084,6 +1084,7 @@ let register_builtin_functions () = ("Test.false" , test_false,2); ("Test.eq" , test_eq,3); ("Test.neq" , test_neq,3);
("Quotient.in" , nop_fun, 1);.# # FIXME: Yay! # ] let _ = register_builtin_functions ()
commit 00341dfd61751b67fe8672a1736285cb4d67ff6c Author: James Tan james_tan97@outlook.com Date: Wed Jul 12 03:21:06 2023 -0400
Implement `Quotient` elimination
diff --git a/btl/builtins.typer b/btl/builtins.typer index 53c0bce..550773d 100644 --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -541,4 +541,20 @@ Quotient = Built-in "Quotient" : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> Quotient_in : ?A -> Quotient ?A ?R; Quotient_in = Built-in "Quotient.in";
+%% FIXME: We want to be able to say the following +%% Quotient_elim : (f : ?A -> ?B) -> +%% (p : (a : ?) -> (a' : ?) -> ?R a a' -> Eq (f a) (f a')) ≡> +%% (q : Quotient ?A ?R) -> +%% ?B; +%% But we running into the following issue for now: +%% "Bug in the elaboration of a repeated metavar!" +Quotient_elim : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (l3 : TypeLevel) ≡>
(A : Type_ l1) ≡> (B : Type_ l2) ≡>(R : A -> A -> Type_ l3) ≡>(f : A -> B) ->(p : (a : A) -> (a' : A) -> R a a' -> Eq (f a) (f a')) ≡>(q : Quotient A R) ->B;# # FIXME: Try and cut lines right before infix ops rather than right after. # +Quotient_elim = Built-in "Quotient.elim";
%%% builtins.typer ends here. diff --git a/samples/quotient.typer b/samples/quotient.typer index a424bf0..aca5988 100644 --- a/samples/quotient.typer +++ b/samples/quotient.typer @@ -6,7 +6,7 @@ type Nat
_-_ : Nat -> Nat -> Nat; _-_ x y = case x
- | zero => y
- | zero => zero | succ m => case y | zero => x | succ n => m - n;
# # FIXME: Squash this into the original commit that introduces the function. # @@ -24,23 +24,50 @@ normaliseZ np = case np | pair m n => pair (m - n) (n - m);
equalZ : NatPair -> NatPair -> Type; -equalZ x1 x2 = Pair (Eq (fst x1) (snd x2)) (Eq (snd x1) (fst x2)); +equalZ x1 x2 = Eq (normaliseZ x1) (normaliseZ x2); # # FIXME: I think this one as well #
-%% See definition in `builtins.typer` -%% Quotient : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) -> -%% (R : A -> A -> Type_ l2) -> Type_ (TypeLevel_⊔ l1 l2) %% -%% Quotient_in : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) ≡> -%% A -> (R : A -> A -> Type_ l2) => Quotient A R +%% See definitions of `Quotient` in `builtins.typer` +%%
%% FIXME: We shouldn't get this error %% "Requested Built-in "Quotient" does not exist" %% Z = Quotient NatPair equalZ;
+NatToInt : Nat -> Int; +NatToInt n = case n
- | zero => (0 : Int)
- | succ n' => (1 : Int) + NatToInt n' ;
+NatPairToInt' : NatPair -> Int; +NatPairToInt' np = case np
- | pair x y =>
- (case x
| zero => (NatToInt y) * (-1 : Int)| succ _ => NatToInt x);+NatPairToInt : NatPair -> Int; +NatPairToInt np = NatPairToInt' (normaliseZ np);
+%% Proof that NatPairToInt respects the quotient Z +NatPairToIntCompat : (a : NatPair) -> (a' : NatPair) ->
(p : equalZ a a') ->Eq (NatPairToInt a) (NatPairToInt a');+NatPairToIntCompat _ _ p = Eq_eq (f := lambda i ≡>
NatPairToInt' (Eq_uneq (p := p) (i := i)));# # FIXME: Eq_uneq works nicely again, eh?
+%% FIXME: Explicitly providing a value for R should unnecessary, +%% this should be inferred based on the type of `q`. This is +%% because we do not handle residuals during unification for now. Z_To_Int : Quotient NatPair equalZ -> Int; -Z_To_Int q = 5 : Int; +Z_To_Int q = Quotient_elim (R := equalZ) NatPairToInt (p := NatPairToIntCompat) q;
+neg2_Z : Quotient NatPair equalZ; +neg2_Z = Quotient_in (pair (succ zero) (succ (succ (succ zero))));
-test : Int; -test = Z_To_Int (Quotient_in (pair zero zero)); +neg2_Int : Int; +neg2_Int = Z_To_Int neg2_Z;
-%% TODO: Elim +%% FIXME: This could work if we add a reduction rule +%% neg2_refl : Eq neg2_Int (-2 : Int); +%% neg2_refl = Eq_refl; diff --git a/src/eval.ml b/src/eval.ml index 9d82577..c4c9ac5 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -1027,6 +1027,13 @@ let typelevel_lub loc (_depth : eval_debug_info) (args_val: value_type list) = | [Vint v1; Vint v2] -> Vint(max v1 v2) | _ -> error loc ("`Typlevel.⊔` expects 2 TypeLevel argument2")
+let quotient_elim loc depth args =
- let trace_dum = (Var ((epsilon (loc), None), -1)) in
- match args with
| [(Closure _) as f; q] ->eval_call loc trace_dum depth f [q]# # FIXME: Why impose (Closure _)? It could be something else! #
| _ -> error loc "Quotient.elim expects 2 arguments"let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ @@ -1085,6 +1092,7 @@ let register_builtin_functions () = ("Test.eq" , test_eq,3); ("Test.neq" , test_neq,3); ("Quotient.in" , nop_fun, 1);
("Quotient.elim" , quotient_elim, 2); ]let _ = register_builtin_functions ()
commit 55c38d859f79fc86a22fb723b22faaa3fee18810 Author: James Tan james_tan97@outlook.com Date: Wed Jul 12 21:02:28 2023 -0400
Implement `Eq` constructor for `Quotient`
diff --git a/btl/builtins.typer b/btl/builtins.typer index 550773d..120cffd 100644 --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -541,13 +541,25 @@ Quotient = Built-in "Quotient" : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> Quotient_in : ?A -> Quotient ?A ?R; Quotient_in = Built-in "Quotient.in";
+%% FIXME: We want to be able to say the following +%% Quotient_eq : (a : ?) ≡> (a' : ?) ≡> (p : ?R a a') ≡> +%% Eq (Quotient_in (R := R?) a) +%% (Quotient_in (R := R?) a'); # # FIXME: Actually, we want to use ?a and ?a' rather than `(a : ?) ≡> (a' : ?)` # +%% But we running into the following issue for now: +%% "Bug in the elaboration of a repeated metavar!" +Quotient_eq : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) ≡>
(R : A -> A -> Type_ l2) ≡>(a : A) ≡> (a' : A) ≡> (p : R a a') ->Eq (Quotient_in (R := R) a)(Quotient_in (R := R) a');+Quotient_eq = Built-in "Quotient.eq";
%% FIXME: We want to be able to say the following %% Quotient_elim : (f : ?A -> ?B) -> %% (p : (a : ?) -> (a' : ?) -> ?R a a' -> Eq (f a) (f a')) ≡> %% (q : Quotient ?A ?R) -> %% ?B; -%% But we running into the following issue for now: -%% "Bug in the elaboration of a repeated metavar!" +%% Same issue as above Quotient_elim : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (l3 : TypeLevel) ≡> (A : Type_ l1) ≡> (B : Type_ l2) ≡> (R : A -> A -> Type_ l3) ≡> diff --git a/samples/quotient.typer b/samples/quotient.typer index aca5988..156805d 100644 --- a/samples/quotient.typer +++ b/samples/quotient.typer @@ -34,16 +34,40 @@ equalZ x1 x2 = Eq (normaliseZ x1) (normaliseZ x2); %% "Requested Built-in "Quotient" does not exist" %% Z = Quotient NatPair equalZ;
+%% +%% Quotient.eq +%% +%% Proof that quotiented elements are equal when +%% the base elements themselves are related in +%% the underlying type. +𝟙-𝟘 : Quotient NatPair equalZ; +𝟙-𝟘 = Quotient_in (pair (succ zero) zero); # # FIXME: Instead of fancy characters, you could use identifiers like # `q1-0` and `q2-1`. #
+𝟚-𝟙 : Quotient NatPair equalZ; +𝟚-𝟙 = Quotient_in (pair (succ (succ zero)) (succ zero));
+𝟙=𝟙 : Eq (t := Quotient NatPair equalZ) 𝟙-𝟘 𝟚-𝟙; +𝟙=𝟙 = Quotient_eq
(R := equalZ)(a := pair (succ zero) zero)(a' := pair (succ (succ zero)) (succ zero))Eq_refl;# # FIXME: Hmm... indeed we can't infer `a` and `a'` from the type because # we're not allowed to extract the content of the quotient :-(
+%% +%% Quotient.elim +%% +%% Elimination of quotients requires a proof that +%% the equality between quotients is respected NatToInt : Nat -> Int; NatToInt n = case n
- | zero => (0 : Int)
- | succ n' => (1 : Int) + NatToInt n' ;
- | zero => 0
- | succ n' => 1 + NatToInt n';
# # FIXME: Squash this into its original commit
NatPairToInt' : NatPair -> Int; NatPairToInt' np = case np | pair x y => (case x
| zero => (NatToInt y) * (-1 : Int)
| zero => (NatToInt y) * -1# # FIXME: Same here # | succ _ => NatToInt x);
NatPairToInt : NatPair -> Int; @@ -71,3 +95,5 @@ neg2_Int = Z_To_Int neg2_Z; %% FIXME: This could work if we add a reduction rule %% neg2_refl : Eq neg2_Int (-2 : Int); %% neg2_refl = Eq_refl;
+%% TODO: Define Quotient NatPair equalZ ≃ Int diff --git a/src/eval.ml b/src/eval.ml index c4c9ac5..1f25236 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -1034,6 +1034,11 @@ let quotient_elim loc depth args = eval_call loc trace_dum depth f [q] | _ -> error loc "Quotient.elim expects 2 arguments"
+let quotient_eq loc _ args =
- match args with
| [_] -> Vundefined| _ -> error loc "Quotient.eq expects 1 argument"# # FIXME: Why not return the arg (i.e. use `nop_fun`)?
let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ @@ -1092,6 +1097,7 @@ let register_builtin_functions () = ("Test.eq" , test_eq,3); ("Test.neq" , test_neq,3); ("Quotient.in" , nop_fun, 1);
("Quotient.eq" , quotient_eq, 1); ("Quotient.elim" , quotient_elim, 2); ]let _ = register_builtin_functions () diff --git a/src/opslexp.ml b/src/opslexp.ml index 8c1285b..6a1b5ac 100644 --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -304,7 +304,9 @@ and eq_cast_whnf ctx args = match args with | _l1 :: _l2 :: _t :: _x :: _y :: (_, p) :: _f :: (_, fx) :: rest -> (match lexp'_whnf p ctx with
| Call (_, eq, _) when conv_builtin_p ctx eq "Eq.eq"
| Call (_, eq, _)when conv_builtin_p ctx eq "Eq.eq" ||conv_builtin_p ctx eq "Quotient.eq"# # FIXME: :-( Have you tried to make `Quotient.eq` return an `(I ≡> Type)` # rather than an `Eq` so we only need to handle `Eq.eq` here? # I guess it probably just moves the problem elsewhere, tho :-( # -> Some (fx, rest) | _ -> None) | _ -> None diff --git a/tests/elab_test.ml b/tests/elab_test.ml index a3931d7..31e1078 100644 --- a/tests/elab_test.ml +++ b/tests/elab_test.ml @@ -180,7 +180,7 @@ unify (f Z (S Z)) (f (S Z) Z); |}
let _ = add_elab_test_decl
- "WHNF of Eq.cast"
- "WHNF of Eq.cast (applied to Eq.eq)" {|
x = (4 : Int); y = x; @@ -192,6 +192,28 @@ test : Eq (Eq_cast (p := p) (f := lambda _ -> Unit) ()) (); test = Eq_refl; |}
+let _ = add_elab_test_decl
- "WHNF of Eq.cast (applied to Quotient.eq)"
- {|
+totalRel : Unit -> Unit -> Type; +totalRel u1 u2 = Unit;
+unitQ : Quotient Unit totalRel; +unitQ = Quotient_in unit;
+unitQ' = unitQ;
+unitQ=unitQ' : Eq (t := Quotient Unit totalRel) unitQ unitQ'; +unitQ=unitQ' = Quotient_eq
(R := totalRel)(a := unit)(a' := unit)unit;+test : Eq (Eq_cast (p := unitQ=unitQ') (f := lambda _ -> Unit) ()) (); +test = Eq_refl;
- |}
let _ = add_elab_test_decl "Decidable at the type level" {|
commit aa04cc68dfb0aab732b0b87d749309c0214b9a6b Author: James Tan james_tan97@outlook.com Date: Tue Jul 18 20:58:15 2023 -0400
Improve unification scheme for SLlub (l1, l2) when l1 ≃ l2
diff --git a/src/unification.ml b/src/unification.ml index b78d940..d3c76d1 100644 --- a/src/unification.ml +++ b/src/unification.ml @@ -561,6 +561,10 @@ and unify_sortlvl (matching : scope_level option) -> (* FIXME: This SLlub representation needs to be * more "canonicalized" otherwise it's too restrictive! *) (unify' l11 l21 ctx vs matching)@(unify' l12 l22 ctx vs matching)
| SLlub (l1, l2), other | other, SLlub (l1, l2)when OL.conv_p ctx l1 l2(* Arbitrarily selected `l1` over `l2` *) | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]-> unify' l1 (mkSortLevel other) ctx vs matching | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)])commit d00058fa5e90c0c6faa0a633d8183383fde31ecb Author: James Tan james_tan97@outlook.com Date: Wed Jul 26 01:37:49 2023 -0400
Implement `qcase` macro
- Facilitates `Quotient` elimination
diff --git a/btl/pervasive.typer b/btl/pervasive.typer index e28fc8a..7a82db4 100644 --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -690,6 +690,9 @@ depelim = load "btl/depelim.typer"; case_as_return_ = depelim.case_as_return_; case_return_ = depelim.case_return_;
+define-operator "qcase" () 42; +qcase_ = let lib = load "btl/qcase.typer" in lib.qcase_macro;
%%%% Unit tests function for doing file
%% It's hard to do a primitive which execute test file diff --git a/btl/qcase.typer b/btl/qcase.typer new file mode 100644 index 0000000..7bf1bae --- /dev/null +++ b/btl/qcase.typer @@ -0,0 +1,284 @@ +%% Qcase macro +%% Make the syntax cleaner for quotient eliminations +%% +%% qcase (e : A / R) +%% | Quotient_in a => e1 +%% | Quotient_eq a a' r i => e2 +%% +%% `a` is bounded in `e1`, and `a`, `a'`, `r` and `i` are +%% bounded in `e2`. `i` can only be used in an erasable manner. +%% +%% TODO: The annotation is necessary for now, as we need the `R` +%% However, we should make it optional. +is_sym : Sexp -> String -> Bool; +is_sym sexp s =
- let
kfalse = K false;- in
Sexp_dispatch sexp(lambda _ _ -> false) % Nodes(String_eq s) % Symbolkfalse % Stringkfalse % Integerkfalse % Floatkfalse; % List of Sexp+%% (build_explicit_arg "name" sexp) yields a +%% (name := sexp) Sexp +build_explicit_arg : String -> Sexp -> Sexp; +build_explicit_arg s sexp = Sexp_node (Sexp_symbol "_:=_")
(cons (Sexp_symbol s)(cons sexp nil));+qcase_impl = lambda (sexps : List Sexp) ->
- %% For the same example that was given above, we expect
- %% `sexps` to represent the following:
- %% (_|_ (_:_ e (_/_ A R))
- %% (_=>_ (Quotient_in a) e1)
- %% (_=>_ (Quotient_eq a a' r i) e2))
- %% Node : [(_|_ (_:_ e (_/_ A R)) (_=>_ (Qin a) e1) (_=>_ (Qeq a a' r i) e2))]
- let
- %% (_|_ (_:_ e (_/_ A R)) (_=>_ (Qin a) e1) (_=>_ (Qeq a a' r i) e2))
- head = List_head Sexp_error sexps;
- knil = K nil;
- kerr = K Sexp_error;
- get-list : Sexp -> List Sexp;
- get-list node = Sexp_dispatch node
(lambda op lst -> lst) % Nodesknil % Symbolknil % Stringknil % Integerknil % Floatknil; % List of Sexp- %% List of:
- %% (_:_ e (_/_ A R))
- %% (_=>_ (Qin a) e1)
- %% (_=>_ (Qeq a a' r i) e2)
- body = get-list head;
- elim_targ_sexp = List_nth (Integer->Int 0) body Sexp_error;
- elim_fn_sexp = List_nth (Integer->Int 1) body Sexp_error;
- elim_compat_sexp = List_nth (Integer->Int 2) body Sexp_error;
- %% Triple of the expression to eliminate, the underlying type A
- %% and the relation R
- %% A and R are optional
- elim_expr_details : Triplet Sexp (Option Sexp) (Option Sexp);
- elim_expr_details =
letkerr = K (triplet Sexp_error none none);extract_from_annotated_e : Sexp -> List Sexp ->Triplet Sexp (Option Sexp) (Option Sexp);extract_from_annotated_e _ xs =if (Int_eq (List_length xs) (Integer->Int 2))thenlete = List_nth (Integer->Int 0) xs Sexp_error;e_type = List_nth (Integer->Int 1) xs Sexp_error;extract_type sexp sexps =if (is_sym sexp "_/_")then%% (_/_ A R )%% |___| |___|%% | |%% a rleta = List_nth (Integer->Int 0) sexps Sexp_error;r = List_nth (Integer->Int 1) sexps Sexp_error;intriplet e (some a) (some r)elsetriplet e (some Sexp_error) (some Sexp_error);kerr' = K (triplet e (some Sexp_error) (some Sexp_error));inSexp_dispatch e_typeextract_type % Nodeskerr' % Symbolkerr' % Stringkerr' % Integerkerr' % Floatkerr' % List of Sexpelsetriplet Sexp_error none none;extract_targ_from_node : Sexp -> List Sexp ->Triplet Sexp (Option Sexp) (Option Sexp);extract_targ_from_node x xs =%% Check if annotation is presentif (is_sym x "_:_")then%% Dissect the sexp to extract, the e, A and Rextract_from_annotated_e x xselse%% No annotation was given, return the entire%% expresson as the elimination targettriplet x none none;inSexp_dispatch elim_targ_sexpextract_targ_from_node % Nodes(lambda _ -> triplet elim_targ_sexpnone none) % Symbolkerr % Stringkerr % Integerkerr % Floatkerr; % List of Sexp- %% The function (`f`) argument
- elim_fn : Sexp;
- elim_fn =
letextract_fn : Sexp -> List Sexp -> Sexp;extract_fn sexp sexps =%% Check that branch is well formedif (and (is_sym sexp "_=>_") (Int_eq (List_length sexps) (Integer->Int 2)))thenlet%% (_=>_ (Quotient_in a) e1 )%% |_____________| |_________|%% | |%% qin fn_bodyqin_sexp = List_nth (Integer->Int 0) sexps Sexp_error;fn_body_sexp = List_nth (Integer->Int 1) sexps Sexp_error;bound_var : Sexp;bound_var =letextract_var head args = if (and (is_sym head "Quotient_in")(Int_eq (List_length args)(Integer->Int 1)))thenList_head Sexp_error argselse%% FIXME: Might be good to have%% a better way to report thisSexp_error;inSexp_dispatch qin_sexpextract_var % Nodeskerr % Symbolkerr % Stringkerr % Integerkerr % Floatkerr; % List of SexpinSexp_node (Sexp_symbol "lambda_->_")(cons bound_var(cons fn_body_sexp nil))else Sexp_error;inSexp_dispatch elim_fn_sexpextract_fn % Nodeskerr % Symbolkerr % Stringkerr % Integerkerr % Floatkerr; % List of Sexp- %% The proof (`p`) argument
- elim_compat : Sexp;
- elim_compat =
letextract_proof : Sexp -> List Sexp -> Sexp;extract_proof sexp sexps =%% Check that branch is well formedif (and (is_sym sexp "_=>_") (Int_eq (List_length sexps)(Integer->Int 2)))thenlet%% (_=>_ (Quotient_eq a a' r i) p )%% |____________________| |__________|%% | |%% qeq proof_expqeq_sexp = List_nth (Integer->Int 0) sexps Sexp_error;proof_exp_sexp = List_nth (Integer->Int 1) sexps Sexp_error;is_symbol : Sexp -> Bool;is_symbol sexp =letktrue = K true;kfalse = K false;inSexp_dispatch sexp(K kfalse) % Nodesktrue % Symbolkfalse % Stringkfalse % Integerkfalse % Floatkfalse; % List of Sexpbuild_proof : Sexp -> List Sexp -> Sexp;build_proof sexp sexps =%% Check that the right identifier is used with exactly%% 4 arguments, also ensure that identifier are symbols%% TODO: Make it possible to omit the `i`, in which case%% we expect p to be an equality proof.if (and (is_sym sexp "Quotient_eq")(and %% We allow the last parameter `i` to be omitted(or (Int_eq (List_length sexps) (Integer->Int 3))(Int_eq (List_length sexps) (Integer->Int 4)))(List_foldl (lambda acc sexp ->and acc (is_symbol sexp))true sexps)))thenletmklambda : Sexp -> Sexp -> Sexp;mklambda param body =Sexp_node (Sexp_symbol "lambda_->_")(cons param (cons body nil));proof_fn =if (Int_eq (List_length sexps) (Integer->Int 3))then%% `i` is absent, i.e. we expect to be provided%% with an equality proof.%% We want to convert Quotient_eq a a' r => e%% to (lambda a a' r -> e)quote (uquote (List_foldr mklambdasexps proof_exp_sexp))else%% Handle the case where `i` is present%% We have to construct an equality proof%% from what was given%% We want to convert Quotient_eq a a' r i => e%% to (lambda a a' r -> Eq_eq (f := lambda i ≡> e))leterasable_param = List_nth (Integer->Int 3)sexps Sexp_error;proof_fn_params =List_reverse (List_tail (List_reverse sexps nil))nil;eq = quote (Eq_eq (f :=lambda (uquote erasable_param) ≡>(uquote proof_exp_sexp)));inquote (uquote (List_foldr mklambdaproof_fn_params eq));inbuild_explicit_arg "p" proof_fnelseSexp_error;inSexp_dispatch qeq_sexpbuild_proof % Nodeskerr % Symbolkerr % Stringkerr % Integerkerr % Floatkerr % List of SexpelseSexp_error;inSexp_dispatch elim_compat_sexpextract_proof % Nodeskerr % Symbolkerr % Stringkerr % Integerkerr % Floatkerr; % List of Sexp- qelim_args : List Sexp;
- qelim_args = case elim_expr_details
| triplet e a r =>letres = (cons elim_fn(cons elim_compat(cons e nil)));res' = (case r| none => res| some r' =>(cons (build_explicit_arg "R" r') res));inres';- qelim_sexp = Sexp_node (Sexp_symbol "Quotient_elim")
qelim_args;- in
- IO_return qelim_sexp;
+qcase_macro = macro qcase_impl; diff --git a/samples/qcase_test.typer b/samples/qcase_test.typer new file mode 100644 index 0000000..fb4df3c --- /dev/null +++ b/samples/qcase_test.typer @@ -0,0 +1,50 @@ +%% Defining a total relation on Unit +R : Unit -> Unit -> Type; +R u1 u2 = Unit;
+inQ : Quotient Unit R; +inQ = Quotient_in ();
+e1 : Unit; +e1 = qcase (inQ : Unit / R)
- | Quotient_in a => ()
- | Quotient_eq a a' r i => ();
+e2 : Unit; +e2 = qcase (inQ : Unit / R)
- | Quotient_in a => ()
- | Quotient_eq a a' r => Eq_refl;
+e3 : Unit; +e3 = qcase inQ
- | Quotient_in a => ()
- | Quotient_eq a a' r i => ();
+e4 : Unit; +e4 = qcase inQ
- | Quotient_in a => ()
- | Quotient_eq a a' r => Eq_refl;
+test-elim-to-unit = do {
- Test_info "QCASE" "elimination to Unit";
- r0 <- Test_eq "annotated elim to `Unit` with explicit `I`" e1 ();
- r1 <- Test_eq "annotated elim to `Unit` without `I`" e2 ();
- r2 <- Test_eq "unannotated elim to `Unit` with explicit `I`" e3 ();
- r3 <- Test_eq "unannotated elim to `Unit` without `I`" e4 ();
- success <- IO_return (and (and (and r0 r1) r2) r3);
- if success then
- (Test_info "QCASE" "elimination to Unit succeeded")
- else
- (Test_warning "QCASE" "elimination to Unit failed");
- IO_return success;
+};
+exec-test = do {
- b1 <- test-elim-to-unit;
- IO_return b1;
+}; diff --git a/samples/quotient.typer b/samples/quotient.typer index 156805d..2fef29a 100644 --- a/samples/quotient.typer +++ b/samples/quotient.typer @@ -96,4 +96,21 @@ neg2_Int = Z_To_Int neg2_Z; %% neg2_refl : Eq neg2_Int (-2 : Int); %% neg2_refl = Eq_refl;
+%% `qcase` macro to facilitate elimination +Z_To_Int' : Quotient NatPair equalZ -> Int; +Z_To_Int' q =
- %% The annotation is optional, but is necessary in
- %% this case, since the propagation of type
- %% information is insufficient the way things are now.
- qcase (q : NatPair / equalZ)
- | Quotient_in a => NatPairToInt a
- | Quotient_eq a a' r i => NatPairToInt' (Eq_uneq (p := r) (i := i));
+%% Omitting the `i` parameter by providing an equality proof on the RHS +Z_To_Int'' : Quotient NatPair equalZ -> Int; +Z_To_Int'' q =
- qcase (q : NatPair / equalZ)
- | Quotient_in a => NatPairToInt a
- | Quotient_eq a a' r => NatPairToIntCompat a a' r;
%% TODO: Define Quotient NatPair equalZ ≃ Int
commit 489829434030802a9fe918cdfd274340e2cb4bdb Author: James Tan james_tan97@outlook.com Date: Thu Jul 20 23:59:52 2023 -0400
Write some proofs about quotient types
diff --git a/samples/quotient_lib.typer b/samples/quotient_lib.typer new file mode 100644 index 0000000..d6a76cd --- /dev/null +++ b/samples/quotient_lib.typer @@ -0,0 +1,129 @@ +%%%%% Prelude %%%%%%
+%% FIXME : Loading hott.typer doesn't work for some reason +%% due to "[X] Fatal :(internal) lub of two SLsucc" +%% Some definitions will be duplicated for now
+Eq_funext : (f : ? -> ?) => (g : ? -> ?) =>
((x : ?) -> Eq (f x) (g x)) ->Eq f g;+Eq_funext p = Eq_eq (f := lambda i ≡> lambda x -> Eq_uneq (p := p x) (i := i));
+HoTT_isProp P = (x : P) -> (y : P) -> Eq x y;
+HoTT_isSet A = (x : A) -> (y : A) -> HoTT_isProp (Eq x y);
+HoTT_isContr = typecons (HoTT_isContr (l ::: TypeLevel)
(A : Type_ l))(isContr (a : A) ((a' : A) -> Eq a a'));+isContr = datacons HoTT_isContr isContr;
+%%%%% Prelude END %%%%%%
+%% TODO: Prove dependent version of this after we introduce +%% dependent elim, which will be more interesting and more +%% worthwhile +recProp : (A : Type_ ?) ≡>
(B : Type_ ?) ≡>(R : A -> A -> Type_ ?) ≡>(p : HoTT_isProp B) ->(f : A -> B) ->(x : Quotient A R) -> B;+recProp = lambda _ _ _ _ _ R ≡>
lambda p f x ->Quotient_elim (R := R) f (p := lambda a a' r -> p (f a) (f a')) x;+%% Again, this is not very interesting, unlike its dependent +%% counterpart. +recContr : (A : Type_ ?) ≡>
(B : Type_ ?) ≡>(R : A -> A -> Type_ ?) ≡>(p : HoTT_isContr B) ->(x : Quotient A R) -> B;+recContr = lambda _ _ _ _ _ R ≡>
lambda p x -> case p| isContr a f => Quotient_elim (R := R)(lambda _ -> a)(p := lambda a a' r -> Eq_refl)x;+%% FIXME: Quotient_elim should be named Quotient_rec? +%% rec2 : (A : Type_ ?) ≡> +%% (B : Type_ ?) ≡> +%% (C : Type_ ?) ≡> +%% (R : A -> A -> Type_ ?) ≡> +%% (S : B -> B -> Type_ ?) ≡> +%% (C_isSet : HoTT_isSet C) -> +%% (f : A -> B -> C) -> +%% ((a : A) -> (b : A) -> (c : B) -> R a b -> Eq (f a c) (f b c)) -> +%% ((a : A) -> (b : B) -> (c : B) -> S b c -> Eq (f a b) (f a c)) -> +%% Quotient A R -> Quotient B S -> C; +%% rec2 = lambda _ _ _ _ _ A B C R S ≡> +%% lambda C_isSet f feql feqr -> +%% Quotient_elim (R := R) +%% (lambda a -> +%% lambda b -> Quotient_elim (R := S) (f a) +%% (p := feqr a) b) +%% (p := lambda a a' r -> +%% let +%% eqf : (b : B) -> Eq (f a b) (f a' b); +%% eqf b = feql a a' b r; +%% eqf' : Eq (f a) (f a'); +%% eqf' = Eq_funext (f := f a) (g := f a') eqf; +%% p : (x : Quotient B S) -> +%% HoTT_isProp (Eq (Quotient_elim (R := S) (f a) +%% (p := feqr a) x) +%% (Quotient_elim (R := S) (f a') +%% (p := feqr a') x)); +%% p x = C_isSet (Quotient_elim (R := S) (f a) +%% (p := feqr a) x) +%% (Quotient_elim (R := S) (f a') +%% (p := feqr a') x); +%% res : (x : Quotient B S) -> +%% (Eq (Quotient_elim (R := S) (f a) +%% (p := feqr a) x) +%% (Quotient_elim (R := S) (f a') +%% (p := feqr a') x)); +%% res x = Quotient_elim (A := B) +%% %% FIXME: We need depelim here +%% (B := Eq (f a b) (f a' b)) +%% (R := S) +%% eqf +%% (p := lambda u v s -> +%% Eq_eq (f := lambda i ≡> +%% p (Eq_uneq (p := Quotient_eq (R := S) s) (i := i)) +%% (eqf u) (eqf v))) +%% x; +%% in +%% Eq_funext (f := Quotient_elim (R := S) (f a) +%% (p := feqr a)) +%% (g := Quotient_elim (R := S) (f a') +%% (p := feqr a')) +%% res);
+%% Lemma 6.10.2 in HoTT book, to prove this we need to +%% apply propositional truncation on SurjectiveQuotientProof. +%% type SurjectiveQuotientProof (A : ?) (x : Quotient A ?R) +%% | surjectiveQuotientProof (a : A) (Eq (Quotient_in a) x); +%% Quotient_in_surjective : (x : Quotient ?A ?R) -> ||SurjectiveQuotientProof ?A ?R x||₁;
+%% Given a proof that a unary operation preserves the underlying +%% relation, we can apply the operation to the quotiented type. +quotUnaryOp : (A : Type_ ?) ≡>
(R : A -> A -> Type_ ?) ≡>(op : A -> A) ->((a : A) -> (a' : A) -> R a a' -> R (op a) (op a')) ->Quotient A R -> Quotient A R;+quotUnaryOp = lambda _ _ A R ≡>
lambda op h x ->letopPreservesQuotient : (a : A) -> (a' : A) -> R a a' ->Eq (t := Quotient A R)(Quotient_in (op a))(Quotient_in (op a'));opPreservesQuotient a a' r = Quotient_eq (R := R) (h a a' r);inQuotient_elim (R := R)(lambda a -> Quotient_in (op a))(p := opPreservesQuotient)x;