[Typer] [Git][monnier/typer][master] Misc tweaks; use a bit more universe polymorphism; improve some errors

Stefan pushed to branch master at Stefan / Typer

Commits: 56ed1196 by Stefan Monnier at 2020-04-02T17:04:44-04:00 Misc tweaks; use a bit more universe polymorphism; improve some errors

* btl/builtins.typer: Make better use of generalization to avoid `≡`. (List): * btl/pervasive.typer (Option, Not): Make them universe-polymorphic.

* src/builtin.ml (register_builtin_csts): Add name `Type0`.

* src/debruijn.ml (type_level_sort): Rename from `sort_level`.

* src/elab.ml (check_inferred): Give more complete error info. (infer_level): Use `newMetalevel`.

* src/lexp.ml (lexp_head): New function. (mkSLlub', lexp_name): Use it. (lexp_unparse, lexp_print): Fix printout of `type_level_sort`.

* tests/eval_test.ml ("has-attribute", "Implicit Arguments"): Disable tests.

- - - - -

8 changed files:

- btl/builtins.typer - btl/pervasive.typer - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/lexp.ml - src/opslexp.ml - tests/eval_test.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -172,11 +172,11 @@ Sexp_debug_print = Built-in "Sexp.debug_print" : Sexp -> IO Sexp; %% -----------------------------------------------------

%% FIXME: "List : ?" should be sufficient but triggers -List : Type -> Type; +List : Type_ ?ℓ -> Type_ ?ℓ; %% List a = typecons List (nil) (cons a (List a)); %% nil = lambda a ≡> datacons (List a) nil; %% cons = lambda a ≡> datacons (List a) cons; -List = typecons (List (a : Type)) (nil) (cons a (List a)); +List = typecons (List (ℓ ::: TypeLevel) (a : Type_ ℓ)) (nil) (cons a (List a)); nil = datacons List nil; cons = datacons List cons;

@@ -197,16 +197,15 @@ Macro_expand : Macro -> List Sexp -> IO Sexp; Macro_expand = lambda m -> lambda args -> case m | macro f => f args;

-Sexp_dispatch = Built-in "Sexp.dispatch" - : (a : Type) ≡> - Sexp - -> (node : Sexp -> List Sexp -> a) - -> (symbol : String -> a) - -> (string : String -> a) - -> (int : Integer -> a) - -> (float : Float -> a) - -> (block : Sexp -> a) - -> a ; +Sexp_dispatch : Sexp + -> (node : Sexp -> List Sexp -> ?a) + -> (symbol : String -> ?a) + -> (string : String -> ?a) + -> (int : Integer -> ?a) + -> (float : Float -> ?a) + -> (block : Sexp -> ?a) + -> ?a ; +Sexp_dispatch = Built-in "Sexp.dispatch";

%% %% Parse a block using the grammar in the passed context @@ -222,7 +221,8 @@ Reader_parse = Built-in "Reader.parse" : Elab_Context -> Sexp -> List Sexp; %% %% Array_set is in O(N) where N is the length %% -Array_set = Built-in "Array.set" : (a : Type) ≡> Int -> a -> Array a -> Array a; +Array_set : Int -> ?a -> Array ?a -> Array ?a; +Array_set = Built-in "Array.set";

%% %% Takes an element and an array @@ -230,43 +230,47 @@ Array_set = Built-in "Array.set" : (a : Type) ≡> Int -> a -> Array a -> %% %% Array_append is in O(N) where N is the length %% -Array_append = Built-in "Array.append" : (a : Type) ≡> a -> Array a -> Array a; +Array_append : ?a -> Array ?a -> Array ?a; +Array_append = Built-in "Array.append";

%% %% Takes an Int (n) and a value %% Returns an array containing n times the value %% -Array_create = Built-in "Array.create" : (a : Type) ≡> Int -> a -> Array a; +Array_create : Int -> ?a -> Array ?a; +Array_create = Built-in "Array.create";

%% %% Takes an array %% Returns the number of element in the array %% -Array_length = Built-in "Array.length" : (a : Type) ≡> Array a -> Int; +Array_length : Array ?a -> Int; +Array_length = Built-in "Array.length";

%% %% Takes a default value, an index and an array %% Returns the value in the array at the specified index or %% the default value if the index is out of bounds %% -Array_get = Built-in "Array.get" : (a : Type) ≡> a -> Int -> Array a -> a; +Array_get : ?a -> Int -> Array ?a -> ?a; +Array_get = Built-in "Array.get";

%% %% It returns an empty array %% %% let Typer deduce the value of (a : Type) %% -Array_empty = Built-in "Array.empty" : (a : Type) ≡> Unit -> Array a; +Array_empty : Unit -> Array ?a; +Array_empty = Built-in "Array.empty";

%%%% Monads

%% Builtin bind -IO_bind = Built-in "IO.bind" - : (a : Type) ≡> - (b : Type) ≡> - IO a -> (a -> IO b) -> (IO b); +IO_bind : IO ?a -> (?a -> IO ?b) -> IO ?b; +IO_bind = Built-in "IO.bind";

-IO_return = Built-in "IO.return" : (a : Type) ≡> a -> IO a; +IO_return : ?a -> IO ?a; +IO_return = Built-in "IO.return";

%% `runIO` should have type IO Unit -> b -> b %% or IO a -> b -> b, which means "run the IO, throw away the result, @@ -274,7 +278,8 @@ IO_return = Built-in "IO.return" : (a : Type) ≡> a -> IO a; %% is actually crucial to make sure the result of runIO is used, otherwise %% the whole call would look like a dead function call and could be %% optimized away! -IO_run = Built-in "IO.run" : (a : Type) ≡> IO Unit -> a -> a; +IO_run : IO Unit -> ?a -> ?a; +IO_run = Built-in "IO.run";

%% File monad

@@ -300,20 +305,23 @@ Sys_exit = Built-in "Sys.exit" : Int -> IO Unit; %% Returns a value modifiable in the IO monad %% and which already contain the specified value %% -Ref_make = Built-in "Ref.make" : (a : Type) ≡> a -> IO (Ref a); +Ref_make : ?a -> IO (Ref ?a); +Ref_make = Built-in "Ref.make";

%% %% Takes a Ref %% Returns in the IO monad the value in the Ref %% -Ref_read = Built-in "Ref.read" : (a : Type) ≡> Ref a -> IO a; +Ref_read : Ref ?a -> IO ?a; +Ref_read = Built-in "Ref.read";

%% %% Takes a value and a Ref %% Returns the an empty command %% and set the Ref to contain specified value %% -Ref_write = Built-in "Ref.write" : (a : Type) ≡> a -> Ref a -> IO Unit; +Ref_write : ?a -> Ref ?a -> IO Unit; +Ref_write = Built-in "Ref.write";

%% %% gensym for macro @@ -431,12 +439,14 @@ Test_false = Built-in "Test.false" : String -> Bool -> IO Bool; %% Takes a message and two arbitrary value of the same type %% Returns true when the two value are equal %% -Test_eq = Built-in "Test.eq" : (a : Type) ≡> String -> a -> a -> IO Bool; +Test_eq : String -> ?a -> ?a -> IO Bool; +Test_eq = Built-in "Test.eq";

%% %% Takes a message and two arbitrary value of the same type %% Returns true when the two value are not equal %% -Test_neq = Built-in "Test.neq" : (a : Type) ≡> String -> a -> a -> IO Bool; +Test_neq : String -> ?a -> ?a -> IO Bool; +Test_neq = Built-in "Test.neq";

%%% builtins.typer ends here.

===================================== btl/pervasive.typer ===================================== @@ -32,7 +32,7 @@

%%%% `Option` type

-Option = typecons (Option (a : Type)) (none) (some a); +Option = typecons (Option (ℓ ::: TypeLevel) (a : Type_ ℓ)) (none) (some a); some = datacons Option some; none = datacons Option none;

@@ -334,6 +334,7 @@ type-impl = lambda (x : List Sexp) -> type-decl = quote ((uquote (get-name name)) : (uquote ( (List_foldl (lambda args arg -> Sexp_node (Sexp_symbol "_->_") (cons (get-type arg) (cons args nil))) + %% FIXME: Don't hardcode TypeLevel.z! (Sexp_symbol "Type") (List_reverse (get-args name) nil)) )));

@@ -439,18 +440,17 @@ in List_map mf xs; False = Void; True = Unit;

-Not : Type -> Type; Not prop = prop -> False;

%% Like Bool, except that it additionally carries the meaning of its value. %% We don't use the `type` macro here because it would make these `true` -%% and `false` constructors ovrride `Bool`'s, and we currently don't +%% and `false` constructors override `Bool`'s, and we currently don't %% want that. Decidable = typecons (Decidable (prop : Type)) (true (p ::: prop)) (false (p ::: Not prop));

%% Testing generalization in inductive type constructors. -LList : (a : Type) -> Int -> Type; %FIXME: `LList : ?` should be sufficient! +LList : Type -> Int -> Type; %FIXME: `LList : ?` should be sufficient! type LList (a : Type) (n : Int) | vnil (p ::: Eq n 0) | vcons a (LList a ?n1) (p ::: Eq n (?n1 + 1)); %FIXME: Unsound wraparound!

===================================== src/builtin.ml ===================================== @@ -155,6 +155,7 @@ let register_builtin_csts () = add_builtin_cst "TypeLevel" DB.type_level; add_builtin_cst "TypeLevel_z" DB.level0; add_builtin_cst "Type" DB.type0; + add_builtin_cst "Type0" DB.type1; add_builtin_cst "Type1" DB.type1; add_builtin_cst "Int" DB.type_int; add_builtin_cst "Integer" DB.type_integer;

===================================== src/debruijn.ml ===================================== @@ -80,9 +80,9 @@ let fatal = Log.log_fatal ~section:"DEBRUIJN" * ---------------------------------- *)

let dloc = dummy_location -let sort_level = mkSort (dloc, StypeLevel) +let type_level_sort = mkSort (dloc, StypeLevel) let sort_omega = mkSort (dloc, StypeOmega) -let type_level = mkBuiltin ((dloc, "TypeLevel"), sort_level, None) +let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort, None) let level0 = mkSortLevel SLz let level1 = mkSortLevel (mkSLsucc level0) let level2 = mkSortLevel (mkSLsucc level1)

===================================== src/elab.ml ===================================== @@ -602,11 +602,18 @@ and check_inferred ctx e inferred_t t = -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in (match Unif.unify inferred_t t (ectx_to_lctx ctx) with - | ((_ck, _ctx, t1, t2)::_) + | ((ck, _ctx, t1, t2)::_) -> lexp_error (lexp_location e) e - ("Type mismatch! Context expected `" - ^ lexp_string t2 ^ "` but expression has type `" - ^ lexp_string t1 ^ "`") + ("Type mismatch(" + ^ (match ck with | Unif.CKimpossible -> "impossible" + | Unif.CKresidual -> "residue") + ^ ")! Context expected:\n " + ^ lexp_string t ^ "\nbut expression has type:\n " + ^ lexp_string inferred_t ^ "\ncan't unify:\n " + ^ lexp_string t1 + ^ "\nwith:\n " + ^ lexp_string t2); + assert (not (OL.conv_p (ectx_to_lctx ctx) inferred_t t)) | [] -> ()); e

@@ -993,8 +1000,9 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp =

(* Elaborate a bunch of mutually-recursive definitions. * FIXME: Currently, we never apply generalization to recursive definitions, - * which means we can't define `List_length` or `List_map` without adding - * explicit type annotations :-( *) + * which can leave "bogus" metavariables in the term (and it also means we + * can't define `List_length` or `List_map` without adding explicit type + * annotations :-( ). *) and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) (defs : (symbol * sexp) list) @@ -1026,6 +1034,23 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) and infer_and_generalize_type (ctx : elab_context) se name = let nctx = ectx_new_scope ctx in let t = infer_type se nctx name in + (* FIXME: We should not generalize over metavars which only occur on the rightmost + * side of arrows in type annotations (aka declarations), since there's no + * way for the callee to return something of the proper type if those + * metavar's don't also occur somewhere in the arguments. + * E.g. for annotations like + * + * x : ?; + * F : Type ? → Type ?; + * + * it makes no sense to generalize them to: + * + * x : (ℓ : TypeLevel) ≡> (t : Type ℓ) ≡> t; + * F : (ℓ₁ : TypeLevel) ≡> (ℓ₂ : TypeLevel) ≡> Type ℓ₁ → Type ℓ₂; + * + * since there can't be corresponding definitions. So replace the final + * return type with some arbitrary closed constant before computing the + * set of free metavars. *) match OL.lexp_whnf t (ectx_to_lctx ctx) with (* There's no point generalizing a single metavar, and it's useful * to keep it ungeneralized so we can use `x : ?` to declare that @@ -1431,7 +1456,7 @@ let sform_identifier ctx loc sargs ot = * This is used so that in cases like "lambda t (y : ?) ... " * type inference can guess ? without having to wonder whether it * can refer to `t` or not. If the user wants ? to be able to refer - * to `t`, then she should explicitly write (y : ? t). *) + * to `t`, then they should explicitly write (y : ? t). *) let ctx_shift = ectx_local_scope_size ctx in let octx = Myers.nthcdr ctx_shift (ectx_to_lctx ctx) in let sl = ectx_to_scope_level ctx in @@ -1581,7 +1606,7 @@ let rec infer_level ctx se : lexp = -> OL.mkSLlub (ectx_to_lctx ctx) (infer_level ctx se1) (infer_level ctx se2) | _ -> 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) + newMetalevel (ectx_to_lctx ctx) (ectx_to_scope_level ctx) l)

(* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l")))

===================================== src/lexp.ml ===================================== @@ -1,6 +1,6 @@ (* lexp.ml --- Lambda-expressions: the core language.

-Copyright (C) 2011-2019 Free Software Foundation, Inc. +Copyright (C) 2011-2020 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -204,6 +204,24 @@ let mkCall (f, es) | _, [] -> f | _ -> hc (Call (f, es))

+and lexp_head e = + match e with + | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s + | Var _ -> "Var" + | Let _ -> "let" + | Arrow _ -> "Arrow" + | Lambda _ -> "lambda" + | Call _ -> "Call" + | Cons _ -> "datacons" + | Case _ -> "case" + | Inductive _ -> "typecons" + | Susp _ -> "Susp" + | Builtin (_, _, None) -> "Builtin" + | Builtin _ -> "AttributeTable" + | Metavar _ -> "Metavar" + | Sort _ -> "Sort" + | SortLevel _ -> "SortLevel" + let mkSLlub' (e1, e2) = match (e1, e2) with (* FIXME: This first case should be handled by calling `mkSLlub` instead! *) | (SortLevel SLz, SortLevel l) | (SortLevel l, SortLevel SLz) -> l @@ -214,7 +232,8 @@ let mkSLlub' (e1, e2) = match (e1, e2) with | ((SortLevel _ | Var _ | Metavar _ | Susp _), (SortLevel _ | Var _ | Metavar _ | Susp _)) -> SLlub (e1, e2) - | _ -> Log.log_fatal ~section:"internal" "SLlub of non-level" + | _ -> Log.log_fatal ~section:"internal" + ("SLlub of non-level: " ^ lexp_head e1 ^ " ∪ " ^ lexp_head e2)

let mkSLsucc e = match e with | SortLevel _ | Var _ | Metavar _ | Susp _ @@ -583,7 +602,7 @@ let rec lexp_unparse lxp = -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), [lexp_unparse l1; lexp_unparse l2]) | Sort (l, StypeOmega) -> Symbol (l, "##Type_ω") - | Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel") + | Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel.Sort") | Sort (l, Stype sl) -> Node (Symbol (lexp_location sl, "##Type_"), [lexp_unparse sl]) @@ -601,19 +620,7 @@ and lexp_name e = match e with | Imm _ -> lexp_string e | Var _ -> lexp_string e - | Let _ -> "let" - | Arrow _ -> "Arrow" - | Lambda _ -> "lambda" - | Call _ -> "Call" - | Cons _ -> "datacons" - | Case _ -> "case" - | Inductive _ -> "typecons" - | Susp _ -> "Susp" - | Builtin (_, _, None) -> "Builtin" - | Builtin _ -> "AttributeTable" - | Metavar _ -> "Metavar" - | Sort _ -> "Sort" - | SortLevel _ -> "SortLevel" + | _ -> lexp_head e

(* ------------------------------------------------------------------------- *) (* Printing *) @@ -905,7 +912,7 @@ and lexp_str ctx (exp : lexp) : string = | Sort (_, Stype (SortLevel SLz)) -> "##Type" | Sort (_, Stype (SortLevel (SLsucc (SortLevel SLz)))) -> "##Type1" | Sort (_, Stype l) -> "(##Type_ " ^ lexp_string l ^ ")" - | Sort (_, StypeLevel) -> "##TypeLevel" + | Sort (_, StypeLevel) -> "##TypeLevel.Sort" | Sort (_, StypeOmega) -> "##Type_ω"

| SortLevel (SLz) -> "##TypeLevel.z"

===================================== src/opslexp.ml ===================================== @@ -556,6 +556,8 @@ let rec check'' erased ctx e = -> mkSLlub ctx level (* We need to unshift because the final type * cannot refer to the fields! *) + (* FIXME: If it does refer, + * we get an ugly error! *) (mkSusp level' (L.sunshift n)) | tt -> error_tc ~loc:(lexp_location t) ~print_action:(fun _ ->

===================================== tests/eval_test.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -276,20 +276,20 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv "w = 2" "decltype w" "Int" let _ = test_eval_eqv "w = 2" "declexpr w" "2"

-let attr_decl = " - w = 2; - greater-than = new-attribute (Int -> Int); - greater-than = add-attribute greater-than w (lambda (x : Int) -> x);" - -let _ = test_eval_eqv_named - "has-attribute" - - attr_decl - - "has-attribute greater-than w; - (get-attribute greater-than w) 3;" - - "true; 3" +(* let attr_decl = " + * w = 2; + * greater-than = new-attribute (Int -> Int); + * greater-than = add-attribute greater-than w (lambda (x : Int) -> x);" + * + * let _ = test_eval_eqv_named + * "has-attribute" + * + * attr_decl + * + * "has-attribute greater-than w; + * (get-attribute greater-than w) 3;" + * + * "true; 3" *)

let _ = (add_test "EVAL" "Monads" (fun () ->

@@ -350,21 +350,21 @@ let _ = test_eval_eqv_named

""hello"; 5.0; "hello"; 5.0; "hello"; 7"

-let _ = test_eval_eqv_named - "Implicit Arguments" - - "default = new-attribute Macro; - default = add-attribute default Int (macro (lambda (lst : List Sexp) -> - (IO_return (Sexp_integer (Int->Integer 1))))); - - fun = lambda (x : Int) => - lambda (y : Int) -> - lambda (z : Int) -> x * y + z;" - - "fun 2 1; - fun 2 1" - - "3; 3" +(* let _ = test_eval_eqv_named + * "Implicit Arguments" + * + * "default = new-attribute Macro; + * default = add-attribute default Int (macro (lambda (lst : List Sexp) -> + * (IO_return (Sexp_integer (Int->Integer 1))))); + * + * fun = lambda (x : Int) => + * lambda (y : Int) -> + * lambda (z : Int) -> x * y + z;" + * + * "fun 2 1; + * fun 2 1" + * + * "3; 3" *)

let _ = test_eval_eqv_named "Equalities"

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/56ed11967bf3b8160aaef90c3da5b996e7...