[Git][monnier/typer][master] * src/opslexp.ml (impredicative_erase): Disable it
Stefan pushed to branch master at Stefan / Typer Commits: b4bacaf0 by Stefan Monnier at 2020-03-17T14:26:41-04:00 * src/opslexp.ml (impredicative_erase): Disable it (impredicative_universe_poly): Rename from deep_universe_poly. - - - - - 1 changed file: - src/opslexp.ml Changes: ===================================== src/opslexp.ml ===================================== @@ -1,6 +1,6 @@ (* opslexp.ml --- Operations on Lexps -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. @@ -46,11 +46,13 @@ let conv_erase = true (* Makes conv ignore erased terms. *) (* `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. *) +let impredicative_erase = false (* 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. *) +(* The safety of `impredicative_universe_poly` is unknown. + * But I also like the idea. + * Furthermore it is sufficient to be able to encode System-F (tho + * I haven't been able to generalize this result to Fω). *) +let impredicative_universe_poly = true (* Assume arg is TypeLevel.z when erasable. *) (* Lexp context *) @@ -360,7 +362,7 @@ let sort_compose ctx1 ctx2 l ak k1 k2 = 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 + when ak == P.Aerasable && impredicative_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 View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b4bacaf063bc0fbdd54347c6f9e8b90681... -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b4bacaf063bc0fbdd54347c6f9e8b90681... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Stefan