Simon Génier pushed to branch simon-genier at Stefan / Typer

Commits: 71ec8850 by Stefan Monnier at 2019-10-22T16:41:34-04:00 * src/elab.ml (sform_lambda): Rename the type's var

This should fix some deBruijn errors for cases like:

x : (y : T1) -> T2 y; x z = e;

since the (dependent) type of `e` will use the name `z` rather than `y`. Apparently it doesn't fix all our deBruijn name check errors, tho :-(

* sample/hurkens.typer: Unrelated cosmetic changes.

- - - - - c3706c38 by Stefan Monnier at 2019-10-22T16:45:23-04:00 Merge branch 'master' of gitlab.com:monnier/typer into trunk

- - - - - 634f6df0 by Stefan Monnier at 2019-10-22T17:58:25-04:00 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.

- - - - - 6cbc6ee8 by Simon Génier at 2019-12-28T16:56:34-05:00 Judge if an expression is positive in a variable.

- - - - -

11 changed files:

- samples/hurkens.typer - src/builtin.ml - src/elab.ml - src/lexp.ml - + src/list.ml - src/log.ml - src/opslexp.ml - + src/option.ml - + src/positivity.ml - src/util.ml - + tests/positivity_test.ml

Changes:

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

%%% Code:

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

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

%% 𝓅 is the "powerset". -%% 𝓅 S = (S -> *); FIXME: internal error! -𝓅 : \square -> \square; -𝓅 (S : \square) = (S -> Type); +%% 𝓅 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, σ, τ). @@ -38,11 +40,11 @@ %% %% where * is ...

-U : \square; -U = (X : \square) ≡> (𝓅𝓅 X -> X) -> 𝓅𝓅 X; % Uses the (▵,□,□) rule! +U : □; +U = (X : □) ≡> (𝓅𝓅 X -> X) -> 𝓅𝓅 X; % Uses the (▵,□,□) rule!

τ : 𝓅𝓅 U -> U; -τ t = lambda (X : \square) +τ t = lambda (X : □) ≡> lambda (f : (𝓅𝓅 X) -> X) -> lambda (p : 𝓅 X) -> t (lambda (y : U) -> p (f ((y (X := X) f)))); @@ -91,5 +93,10 @@ boom2 = lambda (p : 𝓅 U) %%boom : ⊥; %%boom = boom1 boom2;

+%% Summary: +%% U = (X : □) ≡> (𝓅𝓅 X → X) → 𝓅𝓅 X +%% Δ .. (y : U) = (p : U → *) ≡> σ y p → p (τσ y) +%% wf = (p : U → *) ≡> ((y : U) ≡> σ y p → p y) → p Ω +

%%% hurkens.typer ends here.

===================================== 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 ===================================== @@ -1466,6 +1466,14 @@ let rec sform_lambda kind ctx loc sargs ot =

let mklam lt1 olt2 = let nctx = ectx_extend ctx arg Variable lt1 in + let olt2 = match olt2 with + | None -> None + (* Apply a "dummy" substitution which replace #0 with #0 + * in order to account for the fact that `arg` and `v` + * might not be the same name! *) + | Some lt2 + -> let s = S.cons (mkVar (arg, 0)) (S.shift 1) in + Some (mkSusp lt2 s) in let (lbody, alt) = elaborate nctx sbody olt2 in (mkLambda (kind, arg, lt1, lbody), match alt with @@ -1496,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 @@ -1548,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 @@ -1556,17 +1574,17 @@ 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 | [Integer (l,i)] -> if i < 0 || i > get_size ctx then - (sexp_error l "##DeBruijn indiex out of bounds"; + (sexp_error l "##DeBruijn index out of bounds"; sform_dummy_ret ctx loc) else let lxp = mkVar ((loc, None), i) in (lxp, Lazy)

===================================== 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/list.ml ===================================== @@ -0,0 +1,38 @@ +(* list.ml --- + * + * Copyright (C) 2019 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. + * + * -------------------------------------------------------------------------- *) + +include Stdlib.List + +let rec find_map (f : 'a -> 'b option) (l : 'a list) : 'b option = + match l with + | head :: tail -> Option.or_else (f head) (fun () -> find_map f tail) + | [] -> None + +let rec try_fold (f : 'a -> 'b -> 'a option) (i : 'a) (l : 'b list) : 'a option = + match l with + | head :: tail -> begin + match f i head with + | Some x -> try_fold f x tail + | None -> None + end + | [] -> Some i

===================================== src/log.ml ===================================== @@ -119,9 +119,10 @@ let maybe_color_string color_opt str = let string_of_log_entry {level; kind; section; loc; msg} = let color = if typer_log_config.color then (level_color level) else None in let parens s = "(" ^ s ^ ")" in - (option_default "" (option_map string_of_location loc) - ^ maybe_color_string color (option_default (string_of_level level) kind) ^ ":" - ^ option_default "" (option_map parens section) ^ " " + let open Option in + (unwrap_or (map string_of_location loc) "" + ^ maybe_color_string color (unwrap_or kind (string_of_level level)) ^ ":" + ^ unwrap_or (map parens section) "" ^ " " ^ msg)

let print_entry entry = @@ -159,7 +160,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 +190,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)

===================================== src/option.ml ===================================== @@ -0,0 +1,47 @@ +(* option.ml --- + * + * Copyright (C) 2019 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. + * + * -------------------------------------------------------------------------- *) + +let map (f : 'a -> 'b) (o : 'a option) : 'b option = + match o with + | Some x -> Some (f x) + | None -> None + +let and_then (o : 'a option) (f : 'a -> 'b option) : 'b option = + match o with + | Some x -> f x + | None -> None + +let or_else (o : 'a option) (f : unit -> 'a option) : 'a option = + match o with + | Some x -> Some x + | None -> f () + +let unwrap_or (o : 'a option) (d : 'a) : 'a = + match o with + | Some x -> x + | None -> d + +let unwrap_or_else (o : 'a option) (f : unit -> 'a) : 'a = + match o with + | Some x -> x + | None -> f ()

===================================== src/positivity.ml ===================================== @@ -0,0 +1,111 @@ +(* positivity.ml --- + * + * Copyright (C) 2019 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. + * + * -------------------------------------------------------------------------- *) + +type db_index = Util.db_index +type lexp = Lexp.lexp + +(** Computes if the judgement x ∉ fv(τ) holds. *) +let rec absent index lexp = + let fv, _ = Opslexp.fv lexp in + not (Debruijn.set_mem index fv) + +let rec absent_in_bindings index bindings = + match bindings with + | [] -> true + | (_, _, tau) :: bindings + -> absent index tau && absent_in_bindings (index + 1) bindings + +(** Computes if the judgement x ⊢ e pos holds. *) +let rec positive (index : db_index) (lexp : lexp) : bool = + (* + * x ∉ fv(e) + * ─────────── + * x ⊢ e pos + *) + absent index lexp || positive' index lexp + +and positive' index lexp = + match lexp with + | Lexp.Arrow (_, _, tau, _, e) + (* + * x ⊢ e pos x ∉ fv(τ) + * ────────────────────── + * x ⊢ (y : τ) → e pos + *) + -> absent index tau && positive' (index + 1) e + + | Lexp.Call (f, args) + (* + * x ∉ fv(e⃗) + * ────────────── + * x ⊢ x e⃗ pos + *) + -> begin + match Lexp.nosusp f with + | Lexp.Var (_, index') when Int.equal index index' + -> List.for_all (fun (_, arg) -> absent index arg) args + | _ + (* If x ∈ fv(f e⃗), but f ≠ x, then x must occur in e⃗. *) + -> false + end + + | Lexp.Inductive (_, _, vs, cs) + (* + * The rules for μ-types and union types are respectively + * + * x ⊢ e pos x ∉ fv(τ) x ⊢ τ₀ pos x ⊢ τ₁ pos + * ────────────────────── ──────────────────────── + * x ⊢ μy:τ.e pos x ⊢ τ₀ ∪ τ₁ pos + * + * Since the two are not separate in Typer, this rule combines both. + *) + -> absent_in_bindings index vs + && let index = index + List.length vs in + Util.SMap.for_all (fun _ c -> positive_in_constructor index c) cs + + | Lexp.Lambda (_, _, _, e) -> positive index e + + | Lexp.Susp (e, s) -> positive index (Lexp.push_susp e s) + + | Lexp.Var _ + (* + * Since we know that x ∈ fv(e), this must be our variable. The same rule + * as the Call applies as a degenerate case with no arguments. + *) + -> true + + | Lexp.Case _ | Lexp.Cons _ | Lexp.Let _ | Lexp.Sort _ | Lexp.SortLevel _ + (* There are no rules that have these synctactic forms as a conclusion. *) + -> false + + | Lexp.Builtin _ | Lexp.Imm _ + -> failwith "must never happen since we already know that x ∈ fv(e)" + + | Lexp.Metavar _ + -> failwith "positivity must be checked after metavariables instanciation" + +and positive_in_constructor index vs = + match vs with + | [] -> true + | (_, _, tau) :: vs + -> positive index tau && positive_in_constructor (index + 1) vs

===================================== src/util.ml ===================================== @@ -58,8 +58,6 @@ let string_sub str b e = String.sub str b (e - b) * `String.uppercase_ascii` is not yet available in Debian stable's `ocaml`. *) let string_uppercase s = String.uppercase s

-let opt_map f x = match x with None -> None | Some x -> Some (f x) - let str_split str sep = let str = String.trim str in let n = String.length str in @@ -106,13 +104,3 @@ let padding_left (str: string ) (dim: int ) (char_: char) : string = let diff = (dim - string_width str) in let lpad = max diff 0 in (String.make lpad char_) ^ str - -let option_default (default : 'a) (opt : 'a option) : 'a = - match opt with - | None -> default - | Some x -> x - -let option_map (fn : 'a -> 'b) (opt : 'a option) : 'b option = - match opt with - | None -> None - | Some x -> Some (fn x)

===================================== tests/positivity_test.ml ===================================== @@ -0,0 +1,101 @@ +(* positivity_test.ml --- + * + * Copyright (C) 2019 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. + * + * -------------------------------------------------------------------------- *) + +open Utest_lib +open Positivity + +type lexp = Lexp.lexp +type vname = Util.vname + +exception WrongPolarity of vname + +type polarity = + | Positive + | Negative + +let print_lexp lexp = ut_string 3 ((Lexp.lexp_string lexp) ^ "\n") + +let assert_polarity polarity lexp vname = + match (polarity, positive 0 lexp) with + | (Positive, false) | (Negative, true) -> raise (WrongPolarity vname) + | _ -> () + +let lexp_decl_str (source : string) : (vname * lexp) list = + let (decls, _) = Elab.lexp_decl_str source Elab.default_ectx in + assert (List.length decls > 0); + List.map (fun (vname, lexp, _) -> print_lexp lexp; (vname, lexp)) (List.flatten decls) + +(** + * Check that all the values declared in the source have the given polarity. + * + * Only declarations are checked, you may introduce variables with any polarity + * in the bindings of let or lambda expressions. + *) +let rec check_polarity (polarity : polarity) (source : string) : int = + let decls = lexp_decl_str source in + try + List.iter (fun (vname, lexp) -> assert_polarity polarity lexp vname) decls; + success () + with + | WrongPolarity _ -> failure () + +let add_polarity_test polarity name sample = + add_test "POSITIVITY" name (fun () -> check_polarity polarity sample) + +let add_positivity_test = add_polarity_test Positive + +let add_negativity_test = add_polarity_test Negative + +let () = add_positivity_test "a variable is positive in itself" {| + x : Type; + x = x; +|} + +let () = add_positivity_test "a variable is positive in some other variable" {| + y : Type; + y = Int; + x : Type; + x = y; +|} + +let () = add_positivity_test "an arrow is positive in a variable that appears in its right hand side" {| + x : Type; + x = Int -> x; +|} + +let () = add_negativity_test "an arrow is negative in a variable that appears in its left hand side" {| + x : Type; + x = x -> Int; +|} + +let () = add_positivity_test "an application of a variable is positive if it does not occur in its arguments" {| + GoodList : Type -> Type; + GoodList = typecons (GoodList (a : Type)) (good_nil) (good_cons (GoodList a)); +|} + +let () = add_negativity_test "an application of a variable is negative if it occurs in its arguments" {| + EvilList : Type -> Type; + EvilList = typecons (EvilList (a : Type)) (evil_nil) (evil_cons (EvilList (EvilList a))); +|} + +let () = run_all ()

View it on GitLab: https://gitlab.com/monnier/typer/compare/94b782eff7a934fad1e9823c28a8aad168d...