Stefan pushed to branch master at Stefan / Typer

Commits: 634f6df0 by Stefan Monnier at 2019-10-22T21:58:25Z Allow "impredicative" universe polymorphism

* samples/hurkens.typer (𝓅): Make it universe-polymorphic.

* src/elab.ml (infer_level): New function. (sform_type): Use it.

* src/log.ml (log_fatal): Set print_at_log before calling log_msg so the message is printed before raising the exception, otherwise it's lost.

* src/opslexp.ml (deep_universe_poly): New const. (sort_compose): Add one more context for k2. Fix k2 scoping. Obey deep_universe_poly.

- - - - -

6 changed files:

- samples/hurkens.typer - src/builtin.ml - src/elab.ml - src/lexp.ml - src/log.ml - src/opslexp.ml

Changes:

===================================== samples/hurkens.typer ===================================== @@ -12,19 +12,21 @@

%%% Code:

+* = Type_ (s z); +□ = Type_ (s (s z)); + ⊥ : Type; ⊥ = (p : Type) ≡> p;

¬ : (ℓ : TypeLevel) ≡> Type_ ℓ -> Type_ ℓ; -¬ t = t -> ⊥; - -* = Type; -□ = Type1; +¬ t = t -> ⊥ ;

%% 𝓅 is the "powerset". -%% 𝓅 S = (S -> *); FIXME: internal error! -𝓅 : □ -> □; -𝓅 (S : □) = (S -> *); +%% 𝓅 S = (S -> *); +𝓅 : (ℓ : TypeLevel) => Type_ (s ℓ) -> Type_ (s ℓ); +%% FIXME: `?` instead of `ℓ` below leads to a type error because it +%% infers a type `Type_ (s (ℓ ∪ ℓ))` instead of `Type_ (s ℓ)` :-( +𝓅 S = (S -> Type_ ℓ); 𝓅𝓅 S = 𝓅 (𝓅 S);

%%%% A "powerful" universe (U, σ, τ).

===================================== src/builtin.ml ===================================== @@ -1,6 +1,6 @@ (* builtin.ml --- Infrastructure to define built-in primitives * - * Copyright (C) 2016-2018 Free Software Foundation, Inc. + * Copyright (C) 2016-2019 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types.

===================================== src/elab.ml ===================================== @@ -1504,7 +1504,7 @@ let rec sform_lambda kind ctx loc sargs ot = * so auto-add a corresponding Lambda wrapper! * FIXME: This should be moved to a macro. *) -> (* FIXME: Here we end up adding a local variable `v` whose - * name is lot lexically present, so there's a risk of + * name is not lexically present, so there's a risk of * name capture. We should make those vars anonymous? *) let nctx = ectx_extend ctx v Variable lt1 in (* FIXME: Don't go back to sform_lambda, but use an internal @@ -1556,6 +1556,16 @@ let sform_letin ctx loc sargs ot = match sargs with | _ -> sexp_error loc "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc

+let rec infer_level ctx se : lexp = + match se with + | Symbol (_, "z") -> mkSortLevel SLz + | Symbol _ -> check se type_level ctx + | Node (Symbol (_, "s"), [se]) + -> mkSortLevel (SLsucc (infer_level ctx se)) + | _ -> let l = (sexp_location se) in + (sexp_error l ("Unrecognized TypeLevel: " ^ sexp_string se); + newMetavar (ectx_to_lctx ctx) dummy_scope_level (l, None) type_level) + (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) * But it would be less efficient (such a lambda can't be passed as argument @@ -1564,11 +1574,11 @@ let sform_letin ctx loc sargs ot = match sargs with * allow such a lambda. *) let sform_type ctx loc sargs ot = match sargs with - | [l] -> let l, _ = infer l ctx in - (mkSort (loc, Stype l), - Inferred (mkSort (loc, Stype (SortLevel (mkSLsucc l))))) - | _ -> sexp_error loc "##Type_ expects one argument"; - sform_dummy_ret ctx loc + | [se] -> let l = infer_level ctx se in + (mkSort (loc, Stype l), + Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l))))) + | _ -> (sexp_error loc "##Type_ expects one argument"; + sform_dummy_ret ctx loc)

let sform_debruijn ctx loc sargs ot = match sargs with

===================================== src/lexp.ml ===================================== @@ -218,7 +218,7 @@ let mkSLlub' (e1, e2) = match (e1, e2) with let mkSLsucc e = match e with | SortLevel _ | Var _ | Metavar _ | Susp _ -> SLsucc e - | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level" + | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level "

(********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp.

===================================== src/log.ml ===================================== @@ -159,7 +159,7 @@ let set_typer_log_level_str str = with _ -> set_typer_log_level (level_of_string str)

-let increment_log_level () = +let increment_log_level () : unit = typer_log_config.level |> int_of_level |> (+) 1 @@ -189,6 +189,7 @@ exception Stop_Compilation of string let stop_compilation s = raise (Stop_Compilation s)

let log_fatal ?section ?print_action ?loc m = + typer_log_config.print_at_log <- true; log_msg Fatal ~kind:"[X] Fatal " ?section ?print_action ?loc m; internal_error "Compiler Fatal Error" let log_error = log_msg Error ?kind:None

===================================== src/opslexp.ml ===================================== @@ -44,9 +44,14 @@ let warning_tc = Log.log_warning ~section:"TC" (* `conv_erase` is supposed to be safe according to the ICC papers. *) let conv_erase = true (* Makes conv ignore erased terms. *)

-(* The safety of `impredicative_erase` is unknown. But I like the idea. *) +(* `impredicative_erase` is inconsistent: as shown in samples/hurkens.typer + * it allows the definition of an inf-looping expression of type ⊥. *) let impredicative_erase = true (* Allows erasable args to be impredicative. *)

+(* The safety of `deep_universe_poly` is unknown. + * But I also like the idea. *) +let deep_universe_poly = true (* Assume arg is TypeLevel.z when erasable. *) + (* Lexp context *)

let lookup_type = DB.lctx_lookup_type @@ -343,19 +348,24 @@ type sort_compose_result | SortK1NotType | SortK2NotType

-let sort_compose ctx l ak k1 k2 = +let sort_compose ctx1 ctx2 l ak k1 k2 = (* BEWARE! Technically `k2` can refer to `v`, but this should only happen - * if `v` is a TypeLevel, and in that case sort_compose - * should ignore `k2` and return TypeOmega anyway. *) - let k2 = mkSusp k2 (S.substitute impossible) in - match (lexp_whnf k1 ctx, lexp_whnf k2 ctx) with + * if `v` is a TypeLevel. *) + match (lexp_whnf k1 ctx1, lexp_whnf k2 ctx2) with | (Sort (_, s1), Sort (_, s2)) - (* FIXME: fix scoping of `k2` and `s2`. *) -> (match s1, s2 with | (Stype l1, Stype l2) -> if ak == P.Aerasable && impredicative_erase - then SortResult k2 - else SortResult (mkSort (l, Stype (mkSLlub ctx l1 l2))) + then SortResult (mkSusp k2 (S.substitute impossible)) + else let l2' = (mkSusp l2 (S.substitute impossible)) in + SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) + | (StypeLevel, Stype l2) + when ak == P.Aerasable && deep_universe_poly + (* The safety/soundness of this rule is completely unknown. + * It's pretty powerful, e.g. allows tuples containing + * level-polymorphic functions, and makes impredicative-encoding + * of data types almost(just?) as flexible as inductive types. *) + -> SortResult (mkSusp k2 (S.substitute DB.level0)) | (StypeLevel, Stype _) | (StypeLevel, StypeOmega) (* This might be safe, but I don't think it adds much power. @@ -483,7 +493,7 @@ let rec check'' erased ctx e = -> (let k1 = check_type erased ctx t1 in let nctx = DB.lexp_ctx_cons ctx v Variable t1 in let k2 = check_type (DB.set_sink 1 erased) nctx t2 in - match sort_compose ctx l ak k1 k2 with + match sort_compose ctx nctx l ak k1 k2 with | SortResult k -> k | SortInvalid -> error_tc ~loc:l "Invalid arrow: inner TypelLevel argument"; @@ -805,7 +815,7 @@ let rec get_type ctx e = -> (let k1 = get_type ctx t1 in let nctx = DB.lexp_ctx_cons ctx v Variable t1 in let k2 = get_type nctx t2 in - match sort_compose ctx l ak k1 k2 with + match sort_compose ctx nctx l ak k1 k2 with | SortResult k -> k | _ -> mkSort (l, StypeOmega)) | Lambda (ak, ((l,_) as v), t, e)

View it on GitLab: https://gitlab.com/monnier/typer/commit/634f6df0a52c10ba036f99e3cee3f7be47a3...