Stefan pushed to branch master at Stefan / Typer
Commits: 84313d0d by Stefan Monnier at 2017-02-10T23:48:01-05:00 Rename vdef to vname
- - - - -
8 changed files:
- − DESIGN - src/REPL.ml - src/debruijn.ml - src/elexp.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/util.ml
Changes:
===================================== DESIGN deleted ===================================== --- a/DESIGN +++ /dev/null @@ -1,1823 +0,0 @@ --*- org -*- - -New: -- extend the stt table to give precedence for "inner op chars" to use within - identifiers (i.e. the "." for module naming). -- "Confusion is power: blurring the line between Bool and Type". - Maybe have "if" use a "Decidable" type class, or maybe automatically - turn "e : t : Bool" into "e : t = true : Type"? - -* Categories of arguments -We want different categories of arguments. I'm thinking here of the -following categories, which are not necessarily mutually-exclusive: - -** Implicit -in the sense that when calling the function, the actual argument will be -automatically inferred from context (at compile-time, by the elaboration -phase). This is typically what happens in Haskell for type arguments as -well as for type-class dictionaries. - -** Partial -in the sense of this being an argument to a partial function. IOW, the -function may fail to terminate, or it may have other side-effects. -The short-term plan is to use Haskell-style monads for that, but we could -imagine extending the "core" notion of function to accommodate a notion of -partial function (especially one which only adds non-termination but not -other kinds of side-effects). - -** Erasable -in the sense that the argument is only needed at compile-time. -There are different slightly different notions of "erasability", which I'll -classify in 2 sub-categories: - -- Type arguments - These are arguments which are only used in type-annotations. IOW after - erasing all type annotations, those arguments are either unreferenced, or - will be become unreferenced after we get rid of all the other - unreferenced arguments. - - One interesting aspect of these is that, according to Werner's IJCAR06, we - can erase those arguments *before* checking convertibility, thus - strengthening the logic by equating more terms. - - Also, there's a chance that we can allow such type arguments to be - impredicative without breaking consistency and without having to introduce - notions like "strong elimination of large inductive types". - -- Hollow arguments - These are arguments whose actual value is not used during evaluation. - This corresponds to Coq's Prop (i.e. erasable because of proof-irrelevance). - Here's an example: - - let p : Int = 56 - let x = lambda (P: Int = String) ≡> - let p' : String = cast P p - string-ref p' 0 - - Here "P" is a hollow argument in that "cast" will be compiled to a no-op so - it won't use it. Yet we can't just throw away this "P" before checking - convertibility, since if we do that, we end up with - - let p = 56 - let x = lambda () ≡> - let p' = p - string-ref p' 0 - - and if we try to normalize this term, we end up doing "string-ref 56 0" :-( - - There are also various ways to define "hollow". E.g. - - Values of this type carry no information. - E.g. this is the case for the equality type: there's only one - constructor and it carries no information, so arguments of this type are - always hollow. - - The argument is never "really used". - E.g. whenever we do case-analysis on it, there's only one possible - branch, and the values we extract are themselves hollow. - -"Hollow" corresponds more or less to the constraints imposed on Coq's Prop -so that extraction can erase it. - -All "type" arguments are also "hollow" arguments. - -One possible choice for Typer is to only use "type" arguments, so that -arguments which are "hollow" but not "type" need to be declared as "normal" -or "implicit". This has 2 downsides: -- Efficiency - We can hope that the optimizer will still end up eliminating those - arguments, but there will necessarily be cases where it will fail to do so. -- Value restriction - Since the language is pure, erasable arguments do not need to obey the - value restriction (note that adding call/cc would break this). - Arguably the same holds for all implicit arguments, but in practice we - want to have a value restriction on implicit-but-non-hollow arguments - because we do not want to have costly operations to happen implicitly, IOW - an "implicit call" should be operationally cheap. - OTOH, we may decide to impose the value restriction on both implicit - and erasable arguments anyway, just to be on the safe side, and because in - practice it very rarely gets in the way. - -* Syntax - -arw ::= '≡>' | '=>' | '->' -colon ::= ':::' | '::' | ':' -exp ::= '(' id ':' exp ')' arw exp | exp arw exp #Function Types - | 'let' decls 'in' exp - | exp actual_arg* #Funcall - | exp ':' exp #Type annotation - | 'lambda' simple_arg* arw exp - | 'case' exp ('|' pattern '->' exp)* - | 'inductive' id formal_arg* ('|' id ind_arg*)* #Kinda like a μ -pattern ::= id pat_arg* -decls ::= ε | decl ';' decls -decl ::= id ':' exp - | id formal_arg* '=' exp -simple_arg ::= id | '('id ':' exp')' -formal_arg ::= id | '(' id colon exp ')' -ind_arg ::= exp | '(' id colon exp ')' -pat_arg ::= id | '(' id ':=' pattern ')' -actual_arg ::= exp | '(' id ':=' exp ')' - -An identifier which starts with a question mark is one meant to be -generalized as an implicit/erasable argument. E.g. - - identity : ?a -> ?a - identity (x : ?a) = x - -should be generalized to - - identity : (a : _) ≡> a -> a - identity (a ::: _) (x : a) = x - -* Compilation efficiency -** Laziness and sharing -Use hash-consing of all terms during elaboration, so as to maximize sharing -and reuse previous computations. -** Handle large inductive types -Don't expand "default branches" in "case" statements too eagerly. -Use binary trees for case statements. - -Typical example could be for something like - - case (a,b) - | (Foo,Foo) => ... - | (Bar,Bar) => ... - ... - -where the type of a (and b) has 100 branches: we shouldn't generate a tree -with 10K branches! - -* TODO -** Mention Minamide&Garrigue's "on the runtime complexity of type-directed unboxing" for "threesomes, with and without blame" by Jeremy Siek and Philip Wadler -** blame calculus, threesomes for coercions-that-dont-accumulate -** Pass implicit args even if there's no subsequent explicit arg. -E.g. "f" might need to be applied to some implicit arg. -E.g. "f x" might need extra implicit args *after* x. -** Represent {n:Int | P(n)} with P(n) erasable -type IntSubset P = mkIS : (n:Int) -> (P n) ≡> IntSubset P -[ This is an example where there's a trailing implicit arg. ] -** Unify Nat, Fin n, Mem x xs -type Singleton x = mkSingleton : (x : t) -> Singleton x -type (∃x ≡> T') = Pack : (x:_) ≡> T' -> (∃x ≡> T') - -Summary below is encouraging, but hides the remaining difficulty: -each constructor (and each branch of the Cases) has a different number (and -type) of erasable arguments. -The Swiss Coercion did solve such problems, so we should be able to -use a similar approach. - -type Coerce T₁ T₂ - = App : Coerce ((x : T₁) ≡> T₂ x) (T₂ X) - | - -*** For Nat -type Nat = Zero | Succ Nat -type Nat' = ∃n ≡> Singleton (nat→int n) -Zero' = Pack {n=Zero} (mkSingleton 0) -Succ' = λ (Pack {n} (mkSingleton i)) -> Pack {n=Succ n} (mkSingleton (i + 1)) -CaseNat' n f₀ f₁ - = λ (Pack {n} i) -> if i = 0 then f₀ () else f₁ (Pack ? (i - 1)) -Proof : (n : Nat) -> (n' : Singleton (nat→int n)) - -> CaseNat n f₀ f₁ = CaseNat' n' f₀ f₁ -*** For Fin n -type Fin n = FZero : Fin (S n) | FSucc : Fin n -> Fin (S n) -type Fin' l = ∃n : Fin l ≡> Singleton (fin→int n) -Zero' = Pack {n=FZero} (mkSingleton 0) -Succ' = λ (Pack {n} (mkSingleton i)) -> Pack {n=FSucc n} (mkSingleton (i + 1)) -CaseFin' n f₀ f₁ - = λ (Pack {n} i) -> if i = 0 then f₀ () else f₁ (Pack ? (i - 1)) -Proof : (n : Fin l) -> (n' : Singleton (fin→int n)) - -> CaseFin n f₀ f₁ = CaseFin' n' f₀ f₁ -*** For Member x xs -type Mem x xs = MZero : Mem x (x::xs) | MSucc : Mem x xs -> Mem x (y::xs) -type Mem' l = ∃n : Mem x xs ≡> Singleton (mem→int n) -Zero' = Pack {n=MZero} 0 -Succ' = λ (Pack {n} i) -> Pack {n=MSucc n} (i + 1) -CaseMem' n f₀ f₁ - = λ (Pack {n} i) -> if i = 0 then f₀ () else f₁ (Pack ? (i - 1)) -Proof : (n : Mem x xs) -> (n' : Singleton (mem→int n)) - -> CaseMem n f₀ f₁ = CaseMem' n' f₀ f₁ - -** "applicative notation" (see Idris) -** named patterns (so I can say "foo = A|B" and then use `foo' in case). -Maybe I can simply perform macro-expansion on patterns. -** Allow limited overloading -E.g. allow the use of the same name to refer to a type and the module in -which it's defined. -Or same name for a type and its sole constructor. -* Core syntax -FIXME: need a syntax for implicit/erasable lambda and call, probably the -same can be used for both, as in "lambda {x:t} body" and "f{y}". -- we don't need to distinguish implicit from erasable in function calls. -- we don't really need to distinguish them in lambda either, - because we can simply make them erasable whenever possible. -- we may need to make an erasable argument non-erase (i.e. just implicit) - since the resulting type is different. So we do need a separate syntax - for "implicit and not erasable" arguments in lambda. - But it can be cumbersome since it should be needed rather rarely. -- we could use "lambda farg => exp" -- if we want "lambda a1 a2 a3 -> exp", then it'd be natural to extend it to - something like "lambda {a1} a2 {a3} -> exp". -- we don't need implicit args in lambda since we can just rely on free vars - being turned into implicit args. - - exp ::= var | "_" | integer | float | string | block - | "let" decl "in" exp - | aarg arw exp - | "lambda" farg arw exp - | exp exp - | "macro_" exp # `exp' is a function of 3 arguments. - | "inductive_" exp_type exp* - | "cons_" var_tname i - | "case_" exp branch* ["_" "=>" exp] - -_ stands for a metavariable to be inferred via unification. - - branch ::= i var* "=>" exp - farg ::= var | "(" var ":" exp ")" - aarg ::= exp | "(" var ":" exp ")" - decl ::= ε - | var ":" exp - | var "=" exp - | decl ";" decl - arw ::= "->" | "=>" | "≡>" - -=> is used for functions whose argument is implicit (i.e. will be - automatically provided either via unification or by a macro). -≡> is used for functions whose argument is not only implicit but - also erasable (will not be needed at run-time). -Maybe we'll need another arrow for non-pure functions. - -** Syntax for function types, arguments, and type declarations. - -*** a -> b, a => b, a ≡> b -*** Data type declarations - -data Foo - | Foo1 T1 T2 T3 - -We need T1, T2, and/or T3 to be sometimes implicit/erasable - -It'd be nice to use the same syntax as for function calls. - -If it's the same syntax as for function calls, then a non-dependent T1 -would want to look like (fieldname : T1), since in function calls, "e" is -equivalent to (e : τ) rather than to (x : e). - -Imposing a fieldname is not a bad idea, tho it's a bit verbose, OTOH it's -not indispensable, since the two syntaxes can be "similar but not equal". - -It's tempting to accept - - | Foo2 T1 => T2 T3 - -for implicit args, à la Haskell, but if an implicit arg's type needs to -refer to a non-implicit arg, that doesn't work, so maybe we can accept this -syntax, but we also need another. - -Maybe another option is to allow - - | Foo2 T1 ≡> T2 => (x : T3) T4 - -where T1 and T2 can refer to x. I.e. auto-order the implicit arguments based -on dependencies. After all, the "generalize" part of HM will need to perform -the exact same auto-ordering, so it's no extra work, really. -This would naturally extend to: - - | Foo2 T1 => T5 ≡> (x : T2) T3 - -Then the fully-explicit syntax could look like - - | Foo2 (x1 : T1) (x2 :: T2) (x3 ::: T3) - -where : is for normal args, :: for implicit and ::: for erasable. - -Another approach is to drop Haskell-like syntax and go for: - - | Foo3 {x : T1; y : T2; z : T3} - -And then use : for normal args, :: for implicit and ::: for erasable - -Equality constraints for data types are implicit, and we'd like some special -syntax for it, like: - - | Foo5 T1 T2 T3 where x = y - -But maybe - - | Foo5 (x = y) => T1 T2 T3 - -would work as well. - -*** Explicit implicit args - -Coq uses something like - - f (x := e1) e2 e3 - -We could make the implicit-vs-erasable choice explicit with ::=. -We don't necessarily need to know at the call site which is erasable and -which is implicit, so we could accept a single syntax for all cases (could -even include normal args, so as to allow out-of-order parameter passing). - -It'd be nice to allow passing implicit parameters without referring to -their name (especially for those where the name is auto-generated). -Of course - - f (_ := e1) e2 e3 - -is an option, but it kinda sucks. Some System F presentations use - - f [τ₁] e2 - -so we could use this as well, but then that clashes with other uses of [...] -for arguments, which is a rather big deal, I think. - -Hopefully this will not be needed often enough to warrant a special syntax. - -** Maybe we need erasable non-implicit args (e.g. type args for module instantiations)? - -** let and recursive defs -*** type annotations may need to refer to earlier defs -(e.g. first define nat, then use it) -*** if we use an SCC analysis, we need all defs before we can start -This is clearly needed especially because of "free vars are implicit args". -*** First attempt: -- read decls in sequence. -- for each decl, if it's an infix declaration, process it immediately. -- for unknown decl, macro-expand it. -- once all decls have been read, collect the set of vars defined. -- perform SCC analysis. -- elaborate SCC groups in sequence. - -Can't work: SCC analysis requires FreeVars, which is only available after -elaboration (since macro-expansion can't be done before elaboration). - -*** Second attempt: -- read and process decls in sequence. -- var decls elaborate and then add to the environment. -- elaboration may partly fail because of forward references. -- elaboration returns a set of free vars found (which may either be free - vars or forward references). -- as soon as all (formerly) free vars have been encountered, the resulting - SCC can be completed (e.g. generalized maybe). -- as soon as we reach the end of decls, we can distinguish free vars from - forward references, and hence complete the corresponding SCCs. - -* Implicit args -** Two varieties: implicit and erasable -** let-polymorphim -When `gen' adds implicit args, all the ones that can be erasable are -marked erasable. -** free type vars -Free vars occurring in type declarations are taken to be erasable arguments. -I.e. implicit args need to be written explicitly. -** inferring implicit actual args -By default, unification is used. -But some types can be associated with specialized decision procedures (macros). -** optional args -Implicit args subsume optional args. -We just need to associate the `Option' type with a macro that always returns -`None' if the args is not provided and `Some a' when `a' is provided. -We can even provide a non-None default value. Just define -type Default (T : Type) (b : T) = - | Actual :: T -> Default T b -and associate `Default' with a macro that returns `b' if no arg is provided. -** Implicit existentials -Just like we can pass a "∀α.α→α" where a "Int→Int" is expected, maybe we -should be able to directly use an ∃α.τ as if it were τ and have the "open" -happen implicitly. - -* case statement -Typing of case statements is a tricky issue: -- we want it to be "as simple as possible" (i.e. try and avoid the - kind of complexity of Coq's "match <e> as <v> in <pat> return <t> with <bs>") -- but we don't want this simplicity to make some things impossible. - -** design ideas: -*** All constructors in an "inductive" definition return the same type. - More specifically, instead of - - Inductive VList a : nat -> Type - | VNil : VList a 0 - | VCons : a -> VList a n -> VList a (S n) - - We have to use something like - - Inductive VList a n - | VNil (n = 0) - | VCons (n = S n1) a (VList a n1) - - The upside being that we don't need Coq's "in <pat>". - -*** Instead of "as <v>" we can provide equality proof in each branch - I.e. each branch would get an implicit extra argument of type - "<e> = <something>". - This gets us rid of Coq's "as <v>". - -*** Since we don't have "as" and "in" any more, we can drop "return" - Since "return" can't refer to special local variables any longer, we can - move it out, so we don't actually need it since we can use a normal type - annotation like "(case <e> <bs>): <t>" instead. - -*** More precise typing of default branch -Usually, in the default branch, we don't get any extra "refining" type -information, because it's a branch that covers several different cases. -But it'd be good to get rid of this limitation. E.g. - - case x - | VCons x xs => ...something... - | _ => ...else... - -here in the ...else... branch we actually know that "x = VNil". So Typer -should provide here an implicit proof that "x = VNil". -More generally, the default branch should get an implicit proof of something -like "<e> = <caseA> ∨ <e> = <caseB> ∨ ...". - -* IF -`if' should accept more than booleans. E.g. it should accept Agda's -"decidable", which is nothing more than a boolean annotated with -erasable proofs (and the erasable proofs should implicitly be available in the -respective branches). - -To be more Lispy (tho not Schemey) maybe it should also accept most other -datatypes where one of the elements can be meaningfully treated as the -"false"/"null" value (e.g. the empty list, the "none" of the option type, -...). - -* Equality - -** Heterogenous equality - -*** One suggestion from Agda list ("telescopic equlity"): - - [_]_≅_ : ∀ {X : Set} {x y} → (Z : X → Set) → Z x → Z y → Set - [_]_≅_ {x = x} {y} Z a b = (x , a) ≡ (y , b) - -*** Definition in Agda - - data _≅_ {i} {A : Set i} (x : A) : {B : Set i} → B → Set i where - refl : x ≅ x - -** K axiom - -[ See article by Jesper Cockx et al. -http://dl.acm.org/citation.cfm?id=2628139&CFID=459245005&CFTOKEN=469... ] - -K : (P : a ≡ a -> Type) -> (p : P refl) -> (e : a ≡ a) -> P e - -Example of use: - -If we have - - coerce : A ≡ B -> A -> B - -then the proof - - coerce-id: (e : Bool ≡ Bool) -> coerce e true ≡ true - coerce-id refl = refl - -requires the K axiom. - -Why can't we prove K? - - Inductive eq (A : Type) (a : A) : A -> Type := - | refl : eq A a a - . - - Definition K (A : Type) - (a : A) - (P : (eq A a a) -> Type) - (p : P (refl A a)) - (e : eq A a a) - : P e := - match e as e0 return P e0 with - | refl => p - end. - -Coq tells us that the "e0" has type "eq A a a0" rather than "eq A a a"! - -* Erasure - -Conversion checks equality after erasure. - -[lambda (var : exp1) exp2] => [exp2] or lambda (var) [exp2] -[exp1 exp2] => [exp1] or [exp1] [exp2] -[var1 vari* => exp] => var1 (not erasable vari)* => [exp] - -congruence everywhere else, e.g.: -[Π(v:exp1)exp2] => Π(v:[exp1])[exp2] - -** equality: - - eq : inductive _ : Type -> Type -> Type | refl : eq a a - eq : inductive _ : (t:Type) => t -> t -> Type | refl : eq a a - -** For erasure to work well, we need some value polymorphism restriction. - -Actually, it's needed because of implicit arguments as well (a use that's -syntactically a plain symbol should not perform computation, even if pure). - -So the rule should be the usual one: an implicit or erasable lambda's body -should be a constructor (lambdas are constructors). - -** Cast/coercion -We should be able to add a "swiss coercion" along the lines of: - - Γ ⊢ v : τ₁ Γ ⊢ P: τ₁ ⊆ τ₂ - ———————————————————————————— - Γ ⊢ cast P v : τ₂ - -with - - type τ₁ ≡ τ₂ = - | eqid : T ≡ T - | eqpm : T₁ ⊆ T₂ -> T₂ ⊆ T₁ -> T₁ ≡ T₂ - | eqcong: Regular F -> (T₁ ≡ T₂) -> (F T₁ ≡ F T₂) - type τ₁ ⊆ τ₂ = - | eid : T₁ ≡ T₂ -> T₁ ⊆ T₂ - | eapp : ((x : T₁) ≡> T₂ x) ⊆ T₂ T₃ - | eabs : ((x : T₁) -> T₂ ⊆ T₃ x) -> T₂ ⊆ ((x : T₁) ≡> T₃ x) - | econg+: Positive F -> (T₁ ⊆ T₂) -> (F T₁ ⊆ F T₂) - | econg-: Negative F -> (T₁ ⊆ T₂) -> (F T₂ ⊆ F T₁) - -Maybe a good τ₁ ⊆ τ₂ constructor would be something like: - - | eimply (F : (x : τ₁) -> τ₂) (_ : (x : τ₁) -> x = F x) - -Where the "=" equality uses erasure, hence covering "eapp" and "eabs", and -probably also econg. - -*** What about recursion/induction? - -** Challenge: from a (potentially costly) ∃b. b > n && P b, write - a (total) function - - search n P (P? : decidable P) (terminates ::: ∃b. b > n && P b) - -> ∃b. b > n && P b - - which just iterates through all integers starting at n. Most likely - "terminates" will only be "runtime erasable" and not - "typecheck-erasable". - -* Useful macros -** Syntax extensions -*** case, with non-trivial patterns -*** re2c -*** Yacc maybe? -*** would "generalized variables" work well for Typer? -** Automatic proof generators -*** Omega -*** Contradiction (e.g. if we have "1=2" in the context) -** Automatic program generators -*** coerce: automatically find the coercion from one type to another -*** type-class: build goal from available dictionaries -*** Herbie: take a numeric expression and rewrite it so as to avoid -overflows/underflows (https://github.com/mikeizbicki/HerbiePlugin) -*** Automatically find the sequence of calls to turn a <Foo> into a <Bar> -More general case of coercions, where the Foo could be, say, a string, -and Bar be a socket descriptor, so it would figure out that it needs to -create a socket, then open a connection to the host described by the string. -Not sure how useful that could be, but I remember reading a paper some years -ago about such a tool for Java. -* Inudction-induction or induction-recursion - -** email - -Hi Jason, - -afaik there is no easy way to do this. I discussed this recently with -Frederik Forsberg, whose PhD thesis is a good source of information about -induction-induction. See section 5.3. - -You can approximate inductive-inductive definition using a similar technique -as for induction-recursion but you don t get the right eliminator. E.g. If -you define a family A : Set, B : A -> Set you expect that the elimination -operators have the form - -elim-A : (X : Set)(Y : X -> Set) -> -> A -> X -elim-B : (X : Set)(Y : X -> Set) -> -> (a : A) -> B a -> Y (elim-A X Y a) - -the problem here is the dependency of the 2nd operator on the first. - -However, unlike the problem with univalence and extensionality this one is -relatively easy to fix as Agda shows. Inductive-inductive definitions -have a straightforward operational semantics and also it is no problem to -derive eliminators and recursors for them. So why are they not included -in Coq? - -Thorsten - -** JFP'09 of Ralph Matthes (and maybe Venanzio Capretta) - -* Generalized variables -Lisp-style generalized variables could look like a pair of a getter+setter -function in the IO/ST monad. -So the "x <- general-var" would call the getter and "general-var := e" -would call the setter. -And I'd guess that "generalized-var" would be a type-class. - -* Translation to/from Java(script) -We'd want to turn classes and interfaces into Typer type-classes and -vice-versa. There's some serious impedance mismatch, tho, so it's not -obvious how such a matching would work. Also if the type-classes are -macro-only then it may be difficult for the compiler to make use of them. - -* Univalence -** Univalence via Agda's primTrustMe again^2 - -Alan Jeffrey ajeffrey-zWi12Q5vYqaakBO8gow8eQ@public.gmane.org -Subject: Univalence via Agda's primTrustMe again^2 -Newsgroups: gmane.comp.lang.agda -To: Agda mailing list agda-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org, Homotopy Type Theory - HomotopyTypeTheory-/JYPxA39Uh5TLH3MbocFFw@public.gmane.org -Date: Tue, 17 Feb 2015 12:02:57 -0600 (1 day, 21 hours, 3 minutes ago) - -*** Explanation - -Hi everyone, - -Here is a very tidied up version of how Agda's primTrustMe can be used to -define a model in which univalence holds... - -The idea is to define equivalence and identity types by induction of -universe level. At level n, (A ≃ B) is the usual definition of half-adjoint -equivalence, which uses ≡ at level n. At level 0, (a ≡ b) is just skeletal -propositional equality. At level n+1, (a ≡ b) is defined to be ∀ F → (F a ≃ -F b). - -We can postulate J, with its beta reduction rule (using Agda's primTrustMe -to define postulates with beta-reductions). - -Part of univalence is postulating that ≃ is a congruence, that is there -is a term cong F : (A ≃ B) → (F A ≃ F B). Somewhat annoyingly, this has two -obvious beta-reductions: - - (cong F refl) --> refl - (cong id p) --> p - -Agda doesn't allow such nondeterminism, so in the Agda development -I introduced two congruence rules, cong and cong′. From cong, we can define -ua (and ditto ua′) as: - - ua : (A ≃ B) -> (A ≡ B) - ua p F = cong F p - -These have inverses, with type: - - ua⁻¹ : (A ≡ B) -> (A ≃ B) - -The inverse of ua is the usual extension of the identity function using -J. The invrse of ua′ is: - - ua′⁻¹ p = p id - -and we can check that ua′⁻¹ (ua′ e) beta reduces to e. To get univalence, we -postulate that ua and ua′ are equivalent, that ua⁻¹ and ua′⁻¹ are -equivalent, and a beta-reduction saying that everything collapses on -reflexivity: - - ua≡ua′ : ∀ e → (ua n e ≡ ua′ n e) - ua⁻¹≡ua′⁻¹-cong : (p ≡ q) → (ua⁻¹ n p ≡ ua′⁻¹ n q) - (ua⁻¹≡ua′⁻¹-cong (ua≡ua′ (ua⁻¹ refl))) --> refl - -From these, we get univalence. - -All comments welcome... - -Alan. - -*** Code - -open import Level using (Level ; zero ; suc ; _ _ ) - -module UnivalenceViaPrimTrustMe3 where - --- Identity and composition of functions - -id : { } {A : Set } A A -id x = x - -_ _ : { m n} {A : Set } {B : Set m} {C : Set n} (B C) (A B) (A C) -(f g) x = f(g x) - --- Skeletal propositional equality - -data _ _ { } {A : Set } (a : A) : A Set where - -refl : (a a) - -{-# BUILTIN EQUALITY _ _ #-} -{-# BUILTIN REFL -refl #-} - - -cong : { m} {A : Set } {B : Set m} (f : A B) {x y : A} (x y) (f x f y) - -cong f -refl = -refl - --- Postulates which beta-reduce - -private - - -- (trustMe a b) has type (a b) for any a and b, handle with care! - - primitive primTrustMe : { } {A : Set } {a b : A} (a b) - - trustMe : { } {A : Set } (a b : A) (a b) - trustMe a b = primTrustMe - - POSTULATE[_ _] : { m} {A : Set } {B : A Set m} a B a ( a B a) - POSTULATE[ a b ] a with trustMe a a - POSTULATE[ a b ] .a | -refl = b - --- Natural numbers - -data : Set where - O : - _+1 : - --- Induction over universe levels - -level : Level -level O = zero -level (n +1) = suc (level n) - -Type : n Set (level (n +1)) -Type n = Set (level n) - --- Equivalence and identity types defined as contextual equivalence --- (a b) at level 0 whenever (a b) --- (a b) at level n+1 whenever for every F, (F a F b) at level n --- (A B) at level n is half-adjoint equivalence, using at level n --- Note that this definition is by inudction on universe level - -Type_ _ _ _ : n (A : Type n) (a b : A) Type n - -cong : n {A B : Type n} (f : A B) {x y : A} (Type n A x y) (Type n B f x f y) -record Type_ _ _ n (A B : Type n) : Type (n +1) - -(Type O A a b) = (a b) -(Type (n +1) A a b) = (F : A Type n) (Type n F a F b) - - -cong O f p = -cong f p - -cong (n +1) f p = F p (F f) - -record Type_ _ _ n (A B : Type n) where - constructor _,_,_,_,_ - field f : A B - field f ¹ : B A - field : a Type n A f ¹(f a) a - field : b Type n B f(f ¹ b) b - field : a Type n (Type n B f (f ¹ (f a)) f a) ( -cong n f ( a)) ( (f a)) - --- Reflexivity - - -refl : n {A} {a} (Type n A a a) - -refl- : n {A} {a} (Type n (Type n A a a) ( -cong n ( x x) ( -refl n)) ( -refl n)) - -refl : n {A} (Type n A A) - - -refl O = -refl - -refl (n +1) = F -refl n - - -refl- O = -refl - -refl- (n +1) = F -refl n - - -refl n = ( x x) , ( x x) , ( x -refl n) , ( x -refl n) , ( x -refl- n) - --- Postulate J - -J : n {A} (C : a b (Type n A a b) Type n) ( a C a a ( -refl n)) a b p C a b p -J n C c a = POSTULATE[ a POSTULATE[ -refl n c a ] ] - --- Symmetry and transitivity of follow from J - - -sym : n {A a b} (Type n A a b) (Type n A b a) - -sym n {A} {a} {b} = J n ( a b p Type n A b a) ( a -refl n) a b - - -trans : n {A a b c} (Type n A a b) (Type n A b c) (Type n A a c) - -trans n {A} {a} {b} {c} = J n ( a b p Type n A b c Type n A a c) ( a id) a b - --- Two possible definitions of being a conguruence... --- both of them have the type -cong n F : (Type n A B) (Type n F A F B) --- but they have different beta-reductions: --- -cong n F ( -refl n) beta-reduces to ( -refl n) --- -cong n id p beta-reduces to p - - -cong : n (F : Type n Type n) {A B} (Type n A B) (Type n F A F B) - -cong n F {A} {B} = f B where - - f : B (Type n A B) (Type n F A F B) - f = POSTULATE[ A POSTULATE[ -refl n -refl n ] ] - - -cong : n {A B} (F : Type n Type n) (Type n A B) (Type n F A F B) - -cong n = POSTULATE[ id id ] - --- From these two definitions of -cong, we get two definitions of ua - -ua : n {A B} (Type n A B) (Type (n +1) Type n A B) -ua n e F = -cong n F e - -ua : n {A B} (Type n A B) (Type (n +1) Type n A B) -ua n e F = -cong n F e - --- Each of these has an inverse. --- Note that (ua ¹ n (ua n p)) beta-reduces to p - -ua ¹ : n {A B} (Type (n +1) Type n A B) (Type n A B) -ua ¹ n {A} {B} = J (n +1) ( A B p (Type n A B)) ( A -refl n) A B - -ua ¹ : n {A B} (Type (n +1) Type n A B) (Type n A B) -ua ¹ n p = p id - --- We postulate that ua and ua are the same - -postulate ua ua : n {A B} e (Type (n +1) (Type (n +1) Type n A B) ua n e ua n e) - --- We also postulate that ua and ua ¹ are the same --- moreover, (ua ¹ ua ¹-cong n (ua ua n ( -refl n)) beta reduces to -refl (n +1) - -ua ¹ ua ¹-cong : n {A B p q} (Type (n +1) _ p q) (Type (n +1) (Type n A B) ua ¹ n p ua ¹ n q) -ua ¹ ua ¹-cong n {A} {B} {p} {q} = r B p q where - - r : B p q (Type (n +1) _ p q) (Type (n +1) (Type n A B) ua ¹ n p ua ¹ n q) - r = POSTULATE[ A POSTULATE[ -refl (n +1) POSTULATE[ ua n ( -refl n) POSTULATE[ ua ua n ( -refl n) -refl (n +1) ] ] ] ] - -ua ¹ ua ¹ : n {A B} p (Type (n +1) (Type n A B) ua ¹ n p ua ¹ n p) -ua ¹ ua ¹ n p = ua ¹ ua ¹-cong n ( -refl (n +1)) - --- From this, we can show that ua and ua ¹ form an equivalence - -ua- : n {A B} (p : Type (n +1) Type n A B) - (Type (n +1) (Type (n +1) Type n A B) (ua n (ua ¹ n p)) p) -ua- n {A} {B} p = J (n +1) ( A B p Type n +1 _ ua n (ua ¹ n p) p) ( A -refl (n +1)) A B p - -ua- : n {A B} (e : Type n A B) - (Type (n +1) (Type n A B) (ua ¹ n (ua n e)) e) -ua- n e = ua ¹ ua ¹-cong n (ua ua n e) - -ua- : n {A B} (p : Type (n +1) Type n A B) - (Type (n +1) _ ( -cong (n +1) (ua ¹ n) (ua- n p)) (ua- n (ua ¹ n p))) -ua- n {A} {B} p = J (n +1) ( A B p Type (n +1) _ ( -cong (n +1) (ua ¹ n) (ua- n p)) (ua- n (ua ¹ n p))) ( A -refl (n +1)) A B p - --- Thus, we have univalence - -univalence : n {A B} (Type (n +1) (Type (n +1) Type n A B) (Type n A B)) -univalence n = ua ¹ n , ua n , ua- n , ua- n , ua- n - - - -* Modules - -Modules should be able to hold definitions which are universe-polymorphic, -which means that the module language can't be the CIC-like core calculus but -has to be a new lambda calculus layered on top, just like the ML -module language. - -Furthermore, module signatures are not really types, but records -holding types. Maybe they can be macro-expanded to something like types: - - F = functor (M1 : SIG) => M2 - -could turn into - - F = λ Mt (M1 : Mt) (Mp : ModuleObeys Mt SIG) => M2 - -But then M2 will have trouble when extracting elements from M1, since -they'll have an unknown abstract type, which can only be turned into -something of a useful type by casting using the proofs in Mp. - -* Type providers (F# and Idris) -* Low-level Typer -** control over low-level representation -*** Use `int' for Nat/Fin n/x ∈ xs -*** Use 0 | 1+<val> for Maybe -This requires knowing that <val> is always smaller than 2^32-2. -*** Use 1 tag-bit for A+B -This requires knowing the useful-bit-size of values (e.g. 30bit for pointers). - -** Region allocation -Can macros be used to implement region-inference? -How 'bout for non-nested region lifetimes, as in typed-regions? - -* Top-level IO -** Should the top-level be a list of definitions or commands? -I think a list of definitions is cleaner. - -But if we want to allow top-level "IORef" values, then we have to provide -some way to run some IO during evaluation of a list of definitions. - -* eta -** eta reduction and case analysis -when unifying "e" with "case e₁ ..." we could use the following eta rule: -e = case e₁ of T₁ x₁₁ .. x₁ₙ -> assume e₁ = T₁ x₁₁ .. x₁ₙ in e - | T₂ x₂₁ .. x₂ₙ -> assume e₁ = T₂ x₂₁ .. x₂ₙ in e - ... - -Actually, during type-inference, we should always "assume" those equalities -when entering a `case' branch, so the issue is how to avoid inf-looping and -how to then rewrite the result into "core PTS code" using explicit equality -proofs and casts. - -** eta of records - -Agda has made its record eta-equivalent. If we do the same for our inductives: - - Inductive R = T x1 x2 - -then - - case (x : R) - | T x1 x2 => F x1 x2 - -turns into - - F (π₁ x) (π₂ x) - -Aka - - F (case x | T x1 _ => x1) (case x | T _ x2 => x2) - -** Generalization to non-records: - -I guess a generalization could look like: - - case x - | T₁ xs => F (G₁ xs) - | T₂ ys => F (G₂ ys) - .. - -=> - - F (case x - | T₁ xs => G₁ xs - | T₂ ys => G₂ ys - ..) - -* Positivity checking -When X is passed to a function, Agda checks how the function uses it to -determine if it's (strictly) positive. -** comp.lang.agda: Strict positivity and indices -** [Coq-Club] Strictly positive inductive types: non-strictly seems safe -as long as the type is not large. -See http://dx.doi.org/10.1007/3-540-52335-9_47. - -** We can stop the positivity checker when it bumps into IO - -This should allow HOAS-style encodings like - - data exp - | Cst Nat - | App exp exp - | Lam (IO (exp -> exp)) - -* Strong elimination of large types -*** From "Recursive Families of Inductive Types" by Capretta -Strong elimination is the elimination rule for inductive types in which the -elimination predicate is allowed to be big, that is, we can have an -elimination predicate "x: I ⊢ (P x): □". If <foo> is impredicative, strong -elimination result in inconsistency (see Coquand's "An Analysis of Girard's -Paradox"). Nevertheless, it can still be admitted if the inductive type -I is defined without the use of impredicativity, that is, as already -mentioned, if there is a type in □ isomorphic to it. - -* Polymorphic recursion inference -GADTs, nested datatypes, indexed inductive families, all make polymorphic -recursion much more common, so it's more important to try and infer it. -One way to try and attack the problem: -1- Infer the type of a recursive function, ignoring the recursive calls - (i.e. delaying them, giving them a fresh return type), -2- generalize, -3- type the recursive calls (now that we know how many implicit params to add). -Of course, this introduces another problem: the generalization depends on -the set of "free fresh vars", which itself can be affected by the typing of -the recursive calls. -** Type Inference with Polymorphic Recursion, Fritz Henglein, toplas 93. - -* Mumble -** Dependent types imply that type-inference needs to call the normalizer. -** macros means that we need to call the evaluator during sexp->lexp parsing. -** typed macros means that macro-expansion is done during type-inference. -** Together this means that sexp->lexp does macro+eval+infer! -** since macro expansion needs type-information, macros can't implement -`macroexpand' easily, so macros that require walking the code tree -(e.g. that need to know the set of freevars in one of its arguments) are -"impossible" unless Typer provides extra support for them. -* Syntax -** Provide syntax for backquote&unquote -Since "," is to be used as separator, maybe (,e) and (`e) could be used? -** Macros -*** Papers -**** ABI Compatibility Through a Customizable Language, Kevin Atkinson and Matthew Flatt and Gary Lindstrom. -*** Additionally to "typecheck" which takes a sexp and returns the sexp -representation of its type, we may need to be able to do that within -some deeper context (i.e. adding some bindings around it). I guess -(fun _ -> ..) sexp wrappers can do the trick. -*** We need to contract (notation) macros for pretty printing. -We might be able to auto-generate the contraction function from the macro -definition for simple macros. For other cases, user-provided contraction -code might do the trick. Another approach might be to try and preserve the -unexpanded form of a macro as some property of the expanded code. -** Implicit args and free vars -Free vars can be used as implicit args, as in: -identity : a -> a - -Let definitions are usually presumed to be non-recursive. There are two -ways to get recursive definitions: add a type-declaration of a variable -as a "forward declaration" before its use, or just reference the -variable without any forward declaration in the case the variable is not -present in the previous environment (in which case it's presumed to -be a forward reference). - -This "free vars might be forward references" only works for definitions and -not for type declarations. This restriction is needed to make sure that -forward declarations work reliably. - - -* Name-equivalence -** Generative types -We want to be able to say that "data A = Ca: Int → A" and "data B = Cb: -Int → B" are different, so A and B have the same structure but are -not equal. Maybe we can do that with a "fresh" operation, so that -"fresh (Ind (Set; Int → α))" does just that. -** non-generative types -We don't want all inductive definitions to be generative, OTOH, because we -want to be able to generate Inductive definitions for tuples "on the fly" -without having to hash-cons them. -OTOH, maybe we can just have a predefined "list of tuple types", so there's -no need to hash-cons. If that's the only case where non-generativity is -needed, that might be sufficient. Haskell and SML seem happy with -generative-only datatypes. -** Opaque definitions -Maybe the same "fresh" can be used for opaque definitions. -** Partially generative/opaque -Maybe we could provide a rule such that "a : fresh τ ⇒ a : τ" and -vice-versa, while still treating two "fresh τ" as being different. -E.g. used for "type BufferPos = fresh Int" so BufferPos can be used anywhere -an Int is needed (and vice-versa), but you can't pass a BufferPos -to a BufferLength without an explicit conversion. - -* Termination checking - -** Termination checking with CBV may be slightly different. - -*** - -From: Pierre Boutillier pierre.boutillier@pps.univ-paris-diderot.fr -Subject: Re: [Coq-Club] Termination -To: coq-club@inria.fr -Date: Fri, 15 Jun 2012 10:10:41 +0200 (4 hours, 28 minutes, 45 seconds ago) - -[1. text/plain] - -On 15/06/2012 08:29, Gert Smolka wrote: -> One of our students discovered that Coq 8.3 accepts -> -> Fixpoint foo (x : nat) : nat := (fun _ => O) (foo x). -> -> although foo diverges under cbv. -> -> Is this considered a bug or a feature? -> (foo terminates under call by name) -> -> Gert -This is definitely not a feature ! This is not really a bug either because -if strong normalization is broken, weak is not. As a result, -consistency remains. - -In any case, it's a known but not that popular fact. (Each time I show that -to someone, he can't believe its eyes, then he trys for half a day to -get a closed proof of false thanks to that. None has succeed yet). - -It is also one of the purpose of my proposal for a new implementation of -guard condition that I formally describe and badly try to explain the -motivations here : -http://hal.archives-ouvertes.fr/docs/00/65/17/80/PDF/boutillier.pdf - -The main purpose is to exhibit how an abstract machine that computes -subterm_values instead of lambda terms could at the same time ensure strong -normalization and allow to interleave "fix" and "injection" tactics (which -means in CIC term accepting - -fix f x := match x with |C y => fun f' => f' y end f. - -) - -The patch that implements this is in the proof reading queue of the kernel -guardian for a month... - -Pierre. - -*** - -From: Robbert Krebbers mailinglists@robbertkrebbers.nl -Subject: Re: [Coq-Club] Termination -To: Gert Smolka smolka@ps.uni-saarland.de -CC: coq-club@inria.fr -Date: Fri, 15 Jun 2012 10:11:39 +0200 (4 hours, 37 minutes, 52 seconds ago) - -[1. text/plain] - -Hello, - -this is a known problem of the termination checker. - -What happens is that Coq reduces the body of the fixpoint, and then checks -whether all recursive calls are guarded. In your example, after reduction, -the body no longer contains any recursive calls (and in particular the -non-terminating call), so Coq accepts your definition. - -See also: - -- http://foundations.cs.ru.nl/chitchat/slides/chit-barras.pdf - A talk by Bruno Barras on the implementation of the guard condition. Slide -22 shows about the same example as below. - -- http://cs.ioc.ee/~tarmo/papers/mscs04.pdf - Page 2 (last paragraph) - 4 explain the problems of the guard condition. - -- http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=1843 - -Robbert - -* Side-effects -** Check "Extensible Effects" by Kiselyov and Sabry -** We can safely provide a "runIO" of type "IO () → ()" -*** Try to provide HashCons, Memoize, Lazy libraries. -*** How 'bout pointer-equality? -** Non-termination and exceptions -*** We want the language to "feel imperative" to the extent that you don't -need monads for exceptions and infinite recursion. -*** We can't just disallow normalization of partial functions. -This is because if they're used in proofs, we may erase the proof before -running it, so the partial"ness" is not detected when needed. Think of -passing a dummy proof to "array_ref" that can only be evaluated at run-time -when the actual index is known, but by that time the proof is gone, because -we assumed it is total! -*** But we do want to allow partial functions in type expressions. -*** I.e. we want to un-erase the partial functions. -So we can only call code that depends on a particular computation once -that computation has been shown to terminate (without error). - -E.g. - - ask_oracle : (α:Type) ⇁ α - - foo = array_get (P:=ask_oracle (n<m)) n v - -would not fail to type-check but would behave like - - p <- ask_oracle (n<m); - array_get (P:=p) n v - -*** More generally, we want to lift all applications of partial functions -to a top-level monad! - -** Monadic notation? - -We'd like to be able to write "a->b->c(!d)" rather than -"t₁ <- a->b; t₂ <- t₁->c; t₃ <- !d; t₂ t₃". - -A similar notational convenience could be used for relations where a natural -syntax could be "a * b = c" and we'd then want to be able to write "a * b * -c = d" to mean "∃x. R a b x ⋀ R x c d". -If we treat it "a * b" as a thing with a monadic type, we'd get "a * b = c" => -"bind (a * b) (λt. t = c)" and "a * b * c = d" as "bind (a * b) (λt₁. bind -(t₁ * c) (λt₂. t₂ = d))" where the "bind" could be defined as - - bind (x * y) f = ∃t. R x y t ⋀ y t - -So we'd want to do something like "A-normalize" or "CPS convert" locally. - -*** Type-directed control-inversion? - -IO could declare an associated macro, so that any expression of type "IO τ" -is passed to that macro along with its surrounding "continuation". So - - in "e₁ e₁", if "e₂" has type "IO τ", we'd call that macro with "e₂" as - argument as well as with a function λx."e₁ x". - -For IO the macro would return "bind e1 e2", whereas for "a * b" it would use -"∃x. a * b " - - -* Partial functions - -Here's an example of a use of partial functions: - - type Exp (e : Env) - | Var i (t : lookup i e) - -where "lookup" might fail. Without partial functions, we have to use -a relational style, as in: - - type Exp (e : Env) - | Var i (_: lookup i e t) t - -In the present case, we could make "lookup" return False, but if we change -it to: - - type Exp (e : Env) (τ : EType) - | SetVar i (v : Exp Env (lookup i e)) - -Suddenly, this doesn't work any more. We would then have to do something -like, have `lookup` return an `Option` and then do: - - type Exp (e : Env) (τ : EType) - | SetVar i (v : (case lookup i e - | Some t => Exp Env t - | None -> False)) - -It would be neat to have some way to "automate" this. - -* Erasable constructors - -Some constructors should be erased! Example: - - type Exp τ := - [..blabla..] - | Esubsumption {_ : τ' < τ} (e : Exp τ') - -Maybe the code wants to do something useful with Esubsumption, in which case -it shouldn't be erased, but if the code only introduced Esubsumption so as -to lift objects of type "Exp τ'" to type "Exp τ", then Esubsumption is not -really desired, and we'd rather have a "cast" to turn "Exp τ'" into "Exp τ" -without having to add branches for Esubsumption. - -IOW, we want to be able to construct "Esubsumption" as a Swiss Coercion -with a rule like: - - (e : Exp τ') -> (_ : τ' < τ) -> ∃e' : Exp τ. e = e' - -which generalizes to - - (e : F τ') -> (_ : P τ' τ) -> ∃e' : F τ. e = e' - -Of course, we have the problem that this "=" predicate is heterogeneous. - -* Implicit and irrelevant args - -Werner's IJCAR06 seems to say that we can make the "eq_cast" rule take an -erasable proof "a = b": rather than check that the proof is "refl" (which -can't be" done once the arg is erased), the reduction rule of eq_cast can -check that "a ≡ b". This way, the reduction rule can commute with the -erasure rule, so that subject reduction and strong normalization -is preserved. - -Problem is: now "a" and "b" can't be erasable arguments any more, so we've -just moved the problem! - -But really, they're working in a different context where erasability is part -of the type of the object, rather than its use. Still, we need to solve the -following problem: "case <eqproof> | refl => <blabla>" uses <eqproof>, so -<eqproof> can't be erased :-( -Of course, we can provide a special "cast_eq <eqproof> <blabla>" where the -<eqproof> arg is marked as erasable, but: is it sound? - -Here's a sample problem: - - let p : Int = 56 - let x = lambda (P: Int = String) ≡> - let p' : String = cast P p - string-ref p' 0 - -after erasure we'd get: - - let p = 56 - let x = let p' = p - string-ref p' 0 - -now `x' will be dead because we can't provide the proof "Int = String", but -the code will be executed anyway. We can delay/avoid the execution by -imposing a value restriction, such that the above becomes: - - let p = 56 - let x = lambda _ -> - let p' = p - string-ref p' 0 - -This way CBV won't execute the dangerous code. -BUT: normalization will still execute it, so we still have a problem! - -** The core language need to have "irrelevant/erasable" arguments -so that type-equality can be defined modulo erasure -** It would be nice to push implicit arguments outside of the core language -and have them be implemented by a "define" macro. -E.g. "define f {a} b c = toto" could be expanded into: - - def f' a b c = toto; defmacro f = v <- newmetavar; return `(f' ,v) - -but this is problematic in several ways: -- if we want to provide ML-style implicit formal type arguments which are - automatically inserted by the type inference. -- how can we provide a syntax that lets the programmer supply explicitly - implicit arguments? -- what about implicit args that do not come first: - "define f a {b} c = toto" - => - "def f' a b c = toto; defmacro f a = v <- newmetavar; return `(f' ,a ,v)" - but would this work well? -** Can't conflate implicit and irrelevant? -Type-class arguments(dictionaries) need to be implicit but aren't erasable. -** Inference of irrelevant args -If implicit formal args can be inferred (by "free var generalization"), then -we need/want some way to automatically infer which of those args are -irrelevant. -We can do that based on the arg's use: if it only shows up in irrelevant -places, then it's marked irrelevant. Or we can do that based on the arg's -type, with some types marked as "irrelevant if implicit". -** Having both irrelevant and implicit args -*** Should we make implicitness visible in the type? -*** declare all irrelevant args to be implicit => one less case -*** Should irrelevance be a property of the type? -**** We don't want to do it flat out -because Nat may sometimes be irrelevant and sometimes not. -**** We can mark types as "irrelevant when implicit", -so that we can control whether they're irrelevant by making them -implicit/explicit. -**** This would generally imply that all proof args should be implicit. -**** It doesn't offer any way to explicitly make a specific arg irrelevant. -**** Implicit args only used in irrelevant args need to become irrelevant. -E.g. an irrelevant (e.g. proof) arg may cause a new implicit arg (e.g. an -Int) to be added because it appears in the proof type, in which case this -Int arg needs to be irrelevant even if Int is not "irrelevant if implicit". -**** So, can we still infer irrelevance from the type? -In the previous example, in order to know that the Int arg is irrelevant, -we may need an explicit annotation on the type of the function. -We can't assume a convention like "irrelevant args come first", I think, -since often (irrelevant) proof args will have to depend on -relevant args. Maybe we can arrange to have all implicit (relevant) -args come after the (implicit) irrelevant args? -**** There's a tension between making most types "irrelevant when implicit" -since it's often a good idea, and only doing it when it's really known to be -needed since it otherwise forces too many args to be explicit (which can be -cumbersome). The rule that makes implicit args irrelevant -when they're only used in irrelevant args might relieve the tension. - -* Unification -** How to unify ((λx . Cons _ []) 1) = Cons foo [] ? -** How 'bout (λx.B) = A y => B = A y x => A = λy.λx.B -** A(args) = t => A'[args/formals] = t -** Papers -*** occurrence checks: [Reed, LFMTP 2009; Abel & Pientka, TLCA 2011] -*** pruning: [Pientka, PhD, Sec. 3.1.2; Abel & Pientka, TLCA 2011] -*** http://www.cs.cmu.edu/~fp/papers/jicslp96.pdf - -* Universes -** Universe polymorphism -Agda seems to do: -- Add Level as a new special type (with 0 and S constructors and without elim). -- Define: "Set : Πl:Level.Set(S l)". -- Give Πl:Level.e a "non-Set" type to disallow "deep" polymorphism. - -** PTS versions - -*** universes with baked in ~subsumption - -Level = Nat -S = { Type l | l ∈ Level } -A = { (Type l₁ : Type l₂) | l₁ < l₂ } -R = { (Type l₁, Type l₂, Type l₃) | l₃ ≥ max(l₁, l₂) } - -*** universes with subsumption rule - -Level = Nat -S = { Type l | l ∈ Level } -A = { (Type l : Type (S l)) | l ∈ Level } -R = { (Type l, Type l, Type l) | l ∈ Level } - -+ subsumption rule! - -*** universe polymorphism, with explicit lifts - -S = { TypeL, Typeω } ∪ { Type l | l : Level } -A = { Level : TypeL, - 0 : Level, S : Level → Level, - Type : Πl:Level. Type (S l), - max : Level → Level → Level, - lift1 : Πl₁,l₂:Level. Type l₁ → Type (max l₁ l₂), - lift2 : Πl₁,l₂:Level,t: Type l₁. t → (lift1 l₁ l₂ t) - } -R = { (TypeL, Type l, Typeω), (TypeL, Typeω, Typeω), (Type l, Typeω, Typeω), } - ∪ { (Type l₁, Type l₂, Type (max l₁ l₂)) } - -Those lift1 and lift2 could surely get really ugly (tho they'd be folded -into `cast'). Better would be to tweak the App rule, adding maybe an -"App&Lift", where the application takes an extra arg describing the lift. - -OTOH an HM-style inference would make "everything" polymorphic, so maybe -lift1/2 wouldn't be needed very often. - -** Predicativity - -Πx:τ₁.τ₂ : Type (max l₁ l₂) - where τ₁ : Type l₁ - τ₂ : Type l₂ - -type t : Πx:τ₁.Type l - | C1 : Πx:τ₁₁.τ₂ - | Cn : Πx:τₙ₁.τ₂ - -Additional constraint: l ≥ (S (max l1₁ lₙ)) - where τ₁₁ : Type l₁ - τₙ₁ : Type lₙ - -tho this constraint is only needed for those τᵢ₁ which are really carried by -the constructor (not parameters of t). - -** Inductive types and equality constraints - -We can either allow inductive types of the form - - type Vec1 a n = Null1 : Vec1 a 0 | Cons1 : a -> Vec1 a n -> Vec1 a (S n) -or - type Vec2 a n = Null2 (n = 0) | Cons2 a (Vec2 a n') (n = S n') - -To some extent we can even automatically convert from one to the other. -So we could restrict the internal representation to only accept the second -form, and then provide special-support for equality, which we pretty much -need to do anyway. - -Does it come with a cost? That depends on the universe-level of the -equality type. - -We can encode equality in CoC: - - eq x y = ∀f. f x -> f y - eq_refl : ∀x. eq x x - eq_refl x f P = P - -*** E.g. if (x = y) is in Type 0: - -type (=) (t:Type l) (a:t) : t -> Type 0 - refl: a = a - -Vec1 : Type l -> Nat -> Type l : Type l+1 -Vec2 : Type l -> Nat -> Type l : Type l+1 -Null1 : ∀a:Type l. Vec a 0 : Type l+1 -(=) : ∀t:Type l. t -> t -> Type 0 : Type l+1 -Nat : Type 0 -n = 0 : Type 0 -Null2 : ∀a:Type l. ∀n:Nat. ∀P:(n = 0). Vec a n : Type l+1 - -In general, a constructor of the form: - - C : <args> -> T <indices> - -can be replaced by - - C : <args> {index₀ = x₀} ... {indexₙ = xₙ} -> T <xs> - -this should not affect typing very much since - - (index = x) : Type₀ - -so the level of T is not affected. - -*** E.g. if (x = y) is in Type l: - -type (=) (t:Type l) (a:t) : t -> Type l - refl: a = a - -Vec1 : Type l -> Nat -> Type l : Type l+1 -Vec2 : Type l -> Nat -> Type l : Type l+1 -Null1 : ∀a:Type l. Vec a 0 : Type l+1 -(=) : ∀t:Type l. t -> t -> Type l : Type l+1 -Nat : Type 0 -n = 0 : Type 0 -Null2 : ∀a:Type l. ∀n:Nat. ∀P:(n = 0). Vec a n : Type l+1 - -In general, a constructor of the form: - - C : <args> -> T <indices> - -can be replaced by - - C : <args> {index₀ = x₀} ... {indexₙ = xₙ} -> T <xs> - -And we have - - indexᵢ : Aᵢ : Type i => (indexᵢ = x) : Type i - -so the level of T can be affected! - -** Impredicativity of erasable arguments - -Could it be that erasable parameters could be handled impredicatively? - -I'd guess not, since someone would have done it by now!! - -Coq's Prop is "erasable and impredicative" but that means Πx:τ₁.τ₂ can be -impredicative if τ₂:Prop, i.e. if the result is erasable, so that only works -if something will always be used in an erasable position. I guess we could -add "erase-only" types and then allow them to be impredicative. - -OTOH, in "Carnap's remarks on impredicative definitions and the genericity -theorem", they make a case for the fact that impredicativity might indeed -make sense for "erasable" terms. - -Also, by marking "large" elements of inductive definitions as erasable, we'd -get something similar to preventing strong elimination for them. - -E.g. in cast-ultimate.v I had to use axioms like - - EQ_ex : Exists K1 TF1 = Exists K2 TF2 -> (∀F. F K1 TF1 = F K2 TF2) - -whose soundness is actually not known. -With impredicative erasable args we do not need an axiom de define: - - EQ_ex : Exists(K:≡K1) TF1 = Exists(K:≡K2) TF2 - -> (∀F. F(K:≡K1) TF1 = F(K:≡K2) TF2) - -Notice how F only takes an erasable version of K1 and K2, thus -imposing a constraint on the axiom which might indeed be sufficient to make -it sound. Hopefully it's also still sufficient for the cast-ultimate.v proof -to go through! - -** Universe level of equality - -In current Coq, homogenous equality is: - - type (=) (t:Type l) (a:t) : t -> Type 0 - refl: a = a - -But supposedly, this is not compatible with the univalence axiom, so it is -out of fashion. -[ https://github.com/vladimirias/Foundations/blob/master/Coq_patches/README ] - -To be compatible we need: - - type (=) (t:Type l) (a:t) : t -> Type l - refl: a = a - -which implies (instatiating t as "Type l") a type equality of the form - - type (t=) (t:Type l) : Type l -> Type (l + 1) - refl: t = t - -But apparently, the univalence theorem itself implies that type equality -lives one level lower: - - type (t=) (t:Type l) : Type l -> Type l - refl: t = t - -What does it mean for equality of type constructors, like: - - type (t=) (t:Type l -> Type l) : (Type l -> Type l) -> Type ¿? - refl: t = t - -The same univalence axiom seems to require heterogeneous equality to be - - type (~=) (t1:Type l) (a1:t1) : (t2:Type l) -> t2 -> Type (l+1) - refl: a1 ~= a1 - -But apparently we can bring it down to "Type l" in the following way: - - (~=) : (t1:Type l) -> (t2:Type l) -> t1 -> t2 -> Type l - (~=) t1 t2 a1 a2 = ((Q : t1 = t2) -> coerce Q a1 = a2) - -Which I guess is comparable to: - - type (~=) (t1:Type l) (a1:t1) (t2:Type l) (Q:t1 = t2) : t2 -> Type l - refl: a1 ~= (coerce Q a1) - -*** "Natural" level via encoding - -Let's check the "natural" level of the "eq" encoding: - - eq = λ(l:Level) ≡> λ(T:Type l) ≡> λ(x:T) (y:T) -> - (l':Level) ≡> (T':Type l') ≡> (f:T -> T') -> f x -> f y - eq x y : Typeω - -Ouch! But if we consider that the level of inductive definitions is -normally unaffected by the level at which they're eliminated (contrary to -what happens for the kind of impredicative encoding used here) we could -treat it more like - - eq = λ(l:Level) ≡> λ(T:Type l) ≡> λ(x:T) (y:T) -> - (T':Type 0) ≡> (f:T -> T') -> f x -> f y - eq x y : Type l - -Which gives us the dreaded "Type (l+1)" if T is "Type l". -But if x and y are types, we should be able to cut the middle man: - - eq' = λ(l : Level) ≡> λ(x : Type l) (y : Type l) -> - (T':Type 0) ≡> (f : Type l -> T') -> f x -> f y - eq' x y : Type l - -but that doesn't seem to help. - -** Inference - -We'd want inference of universes to go somewhere between Coq's approach and -HM's approach: Coq doesn't use polymorphism, which sometimes leads to -unnecessary restrictions, but HM inference introduces too much polymorphism. - -So we want to only add polymorphism when useful, by cleverly considering -whether subsumption would do the trick anyway. - -- If the unconstrained level types a return value, then - set it as low as possible without polymorphism. -- If it types an argument, OTOH it should be "as high as possible", which is - where we need polymorphism. -- If several levels are needed, merge them into their max: instead of - - type Pair1 : ∀l₁,l₂. Type l₁ → Type l₂ → Type (max l₁ l₂) - mkpair1: ∀l₁:Level,t₁:Type l₁. t₁ → ∀l₂:Level,t₂:Type l₂. t₂ → Pair1 t₁ t₂ - - use - - type Pair2 : ∀l. Type l → Type l -> Type l - mkpair2: ∀l,t₁:Type l,t₂:Type l. t₁ -> t₂ -> Pair2 t₁ t₂ - - this does force us to know l₂ before passing any argument but, - modulo a bit of η-expansion, it's just as good: - - mkpair1 = λl₁,t₁,x₁,l₂. mkpair2 (max l₁ l₂) t₁ x₁ - -* Classical logic -** Paper: Classical Mathematics for a Constructive World, Russell O'Connor -Defines classical as: - - A ∨ B = ¬(A × B) - ∃x . P x = ¬(Πx . P x) - -Defines "stable types": - - stable A = ¬¬A => A - -And notes that for any function that returns a stable type, any "classical" -argument can be assumed to be constructive. E.g.: - - A + B - ⋮ - A ∨ B C stable C - ——————————————————————— - C - -He then defines notations and principles for how to use such classical -definitions in a constructive logic without too much pain. - -Look ma! No axioms! - -Or almost: with these classical definitions we cannot prove the classical -axiom of choice as a theorem, so if you need it, you have to add it as an axiom. - -* Co-induction - -Coinductive data is basically defined by observation, so what is often -written as something like - - codata Stream α - | Nil - | Cons α (Stream α) - -really means something like: - - type StreamAccessor - | Car | Cdr - Stream α = - (a : StreamAccessor) - -> case a - | Car => Maybe α - | Cdr => Maybe (Stream α) - -And with length, that could turn into: - - type StreamAccessor n - | Empty? | Car (n > 0) | Cdr (n > 0) - Stream α n = - (a : StreamAccessor n) - -> case a - | Empty? => Maybe (n > 0) - | Car _ => α - | Cdr _ => Stream α (n - 1) - -In either case, the definition of `Stream` is recursive and doesn't follow -the supported forms of recursion in CIC (i.e. inductive types and inductive -functions) so it requires ad-hoc support. - -It would help to have something akin to the "impredicative encoding" of -inductive types to get an intuitive idea of what should be safe and what -might be dangerous. - -Let's try for `Stream α`: - - Stream α = - (β : Type) -> (a : StreamAccessor) - -> (case a - | Car => Maybe α -> β - | Cdr => Maybe β -> β) - -> β - -So we'd define - - numbers' n β a = case a - | Car => λ f -> f (just n) - | Cdr => λ f -> f (just ¿?¿) %% (numbers' (n + 1)) - numbers = numbers' 0 - -* Papers -** Macros and tactics -*** Rtac -[1] Dissertation: -https://gmalecha.github.io/publication/2015/02/01/extensible-proof-engineeri... -[2] ESOP'16: -https://gmalecha.github.io/publication/2016/01/01/extensible-and-efficient-a... -[3] ITP'14: -https://gmalecha.github.io/publication/2014/07/14/compositional-computationa... -*** ssreflect -*** Mtac -** Other -*** BigBang: Designing a statically typed scripting language -*** Dependently typed Racket -*** Dependently typed Haskell -"My dissertation (github.com/goldfirere/thesis) is about adding dependent -types to GHC. I believe I've solved the first problem, basically by copying -Adam Gundry's approach (http://adam.gundry.co.uk/pub/thesis/). Still working -on that practical problem, though. Expect some changes in time for 7.12 -though. (See https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1 -for some discussion here.)" - -*** On Irrelevance and Algorithmic Equality in Predicative Type Theory, -Andreas Abel & Gabriel Scherer, FOSSACS 2011. -*** "A few constructions on constructors" -*** How to Make Ad Hoc Proof Automation Less Ad Hoc, Beta Ziliani -*** http://homotopytypetheory.org/book/ -*** CMU's 2013 Fall: 15-819 Advanced Topics in Programming Languages -http://scs.hosted.panopto.com/Panopto/Pages/Sessions/List.aspx#folderID=%220... -*** Propositions as Sessions, Philip Wadler -*** A few constructions on constructors, by Conor et al. -*** Constructive selection principle (Markov's principle) -http://www.encyclopediaofmath.org/index.php/Constructive_selection_principle -https://en.wikipedia.org/wiki/Markov%27s_principle -*** size-change termination, Lee, Jones and Ben-Amram, doi:10.1145/360204.360210 -*** A Predicative Analysis of Structural Recursion, Andreas Abel and Thorsten Altenkirch, http://www.cs.nott.ac.uk/~txa/publ/jfp02.pdf -*** A New Look at Generalized Rewriting in Type Theory, Matthieu Sozeau -*** http://moca.inria.fr/ On the implementation of construction functions for non-free concrete -data types. F. Blanqui, T. Hardin and P. Weis. ESOP'07. -*** The Nemerle language -*** "A Theory of Typed Hygienic Macros" de David Herman -http://www.ccs.neu.edu/home/dherman/research/papers/dissertation.pdf -*** http://www.mpi-sws.org/~beta/mtac/ -*** Non-strictly positive and elimination -"Inductively defined types", by Thierry Coquand and -Christine Paulin, COLOG'88, LNCS 417 -*** Dependently Typed Programming based on Automated Theorem Proving, Alasdair Armstrong, Simon Foster, and Georg Struth. -http://arxiv.org/pdf/1112.3833v1 - -*** Strong Normalization for Coq (CiC). -http://www.cs.rice.edu/~emw4/uniform-lr.pdf -*** Irrelevant/erasable args - -*** The Implicit Calculus of Constructions as a Programming Language with Dependent Types, Bruno Barras and Bruno Bernardo, fossacs08. - -In this paper, we show how Miquel's Implicit Calculus of Constructions -(ICC) can be used as a programming language featuring dependent types. -Since this system has an undecidable type-checking, we introduce a more -verbose variant, called ICC which fixes this issue. Datatypes and program -specifications are enriched with logical assertions (such as preconditions, -postconditions, invariants) and programs are decorated with proofs of -those assertions. The point of using ICC rather than the Calculus of -Constructions (the core formalism of the Coq proof assistant) is that all of -the static information (types and proof objects) is transparent, in the -sense that it does not affect the computational behavior. This is -concretized by a built-in extraction procedure that removes this static in- -formation. We also illustrate the main features of ICC on classical examples -of dependently typed programs. - -*** Erasure and polymorphism in pure type systems, Nathan Mishra-Linger and Tim Sheard - -*** On the strength of proof-irrelevant type theories, Benjamin Werner, IJCAR06. - -We present a type theory with some proof-irrelevance built into the -conversion rule. We argue that this feature is particularly useful when -type theory is used as the logical formalism underlying a theorem prover. We -also show a close relation with the subset types of the theory of PVS. -Finally we show that in these theories, because of the additional -extentionality, the axiom of choice implies the decidability of equality, -that is, almost classical logic. - -*** Parametricity and variants of Girard's J operator, Robert Harper and John C. Mitchell, Journal Information Processing Letters archive, Volume 70 Issue 1, April 01, 1999 -The Girard-Reynolds polymorphic λ-calculus is generally regarded -as a calculus of parametric polymorphism in which all well-formed terms are -strongly normalizing with respect to β-reductions. Girard demonstrated that -the addition of a simple "non-parametric" operation, J, to the calculus -allows the definition of a non-normalizing term. Since the type of J is not -inhabited by any closed term, one might suspect that this may play a role in -defining a non-normalizing term using it. We demonstrate that this is not -the case by giving a simple variant, J', of J whose type is otherwise -inhabited and which causes normalization to fail. It appears that -impredicativity is essential to the argument; predicative variants of the -polymorphic λ-calculus admit non-parametric operations without -sacrificing normalization. - -*** Idris (Edwin Brady) -*** http://albatross-lang.sourceforge.net -*** Idris's Effects http://eb.host.cs.st-andrews.ac.uk/drafts/dep-eff.pdf -*** Read -*** (Co)Iteration for higher-order nested datatypes, Andreas Abel and Ralph Matthes, [Abel03] -*** Inductive Families Need Not Store Their Indices, Edwin Brady, Conor McBride and James McKinna. -http://www.cs.st-andrews.ac.uk/~eb/writings/types2003.pdf -*** A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi, Andrew Gacek and Gopalan Nadathur -*** How OCaml type checker works, http://okmij.org/ftp/ML/generalization.html -* Related languages -** Idris -** F-star (https://www.fstar-lang.org) -** Less closely related -*** Dependently typed Racket -*** Dependently typed Haskell
===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -1,6 +1,6 @@ (* REPL.ml --- Read Eval Print Loop (REPL)
-Copyright (C) 2016 Pierre Delaunay +Copyright (C) 2016-2017 Free Software Foundation, Inc.
Author: Pierre Delaunay pierre.delaunay@hec.ca
@@ -99,7 +99,7 @@ let rec read_input i =
(* Interactive mode is not usual typer It makes things easier to test out code *) -type ldecl = vdef * lexp * ltype +type ldecl = vname * lexp * ltype type lexpr = lexp
(* Grouping declaration together will enable us to support mutually recursive
===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2017 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -93,7 +93,7 @@ let type_float = mkBuiltin ((dloc, "Float"), type0, None) let type_string = mkBuiltin ((dloc, "String"), type0, None)
(* easier to debug with type annotations *) -type env_elem = (db_offset * vdef option * varbind * ltype) +type env_elem = (db_offset * vname option * varbind * ltype) type lexp_context = env_elem M.myers
type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *) @@ -145,26 +145,26 @@ let lexp_ctx_cons (ctx : lexp_context) offset d v t = || previous_offset = 1 + offset))); M.cons (offset, d, v, t) ctx
-let lctx_extend (ctx : lexp_context) (def: vdef option) (v: varbind) (t: lexp) = +let lctx_extend (ctx : lexp_context) (def: vname option) (v: varbind) (t: lexp) = lexp_ctx_cons ctx 0 def v t
-let env_extend_rec r (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = +let env_extend_rec r (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = let (loc, name) = def in let ((n, map), env) = ctx in let nmap = SMap.add name n map in ((n + 1, nmap), lexp_ctx_cons env r (Some def) v t)
-let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = env_extend_rec 0 ctx def v t +let env_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec 0 ctx def v t
-let ectx_extend (ectx: elab_context) (def: vdef option) (v: varbind) (t: lexp) +let ectx_extend (ectx: elab_context) (def: vname option) (v: varbind) (t: lexp) : elab_context = match def with | None -> let ((n, map), lctx) = ectx in ((n + 1, map), lexp_ctx_cons lctx 0 None v t) | Some def -> env_extend ectx def v t
-let lctx_extend_rec (ctx : lexp_context) (defs: (vdef * lexp * ltype) list) = +let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = let (ctx, _) = List.fold_left (fun (ctx, recursion_offset) (def, e, t) -> @@ -173,7 +173,7 @@ let lctx_extend_rec (ctx : lexp_context) (defs: (vdef * lexp * ltype) list) = (ctx, List.length defs) defs in ctx
-let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) = +let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = let ((n, senv), lctx) = ctx in let senv', _ = List.fold_left (fun (senv, i) ((_, vname), _, _) ->
===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2017 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -36,7 +36,7 @@ open Pexp (* Aexplicit *)
module U = Util
-type vdef = U.vdef +type vname = U.vname type vref = U.vref type label = symbol
@@ -45,16 +45,16 @@ module SMap = U.SMap type elexp = | Imm of sexp
- | Builtin of vdef + | Builtin of vname | Var of vref
- | Let of U.location * (vdef * elexp) list * elexp - | Lambda of vdef * elexp + | Let of U.location * (vname * elexp) list * elexp + | Lambda of vname * elexp | Call of elexp * elexp list | Cons of symbol | Case of U.location * elexp - * (U.location * (vdef option) list * elexp) SMap.t - * (vdef option * elexp) option + * (U.location * (vname option) list * elexp) SMap.t + * (vname option * elexp) option (* Type place-holder just in case *) | Type (* Inductive takes a slot in the env that is why it need to be here *)
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2017 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -400,7 +400,7 @@ and build_arg_list args ctx i = (* Add args inside context *) List.fold_left (fun c v -> add_rte_variable None v c) ctx arg_val
-and _eval_decls (decls: (vdef * elexp) list) +and _eval_decls (decls: (vname * elexp) list) (ctx: runtime_env) i: runtime_env =
let n = (List.length decls) - 1 in @@ -610,7 +610,7 @@ let debug_eval lxp ctx =
let eval_decls decls ctx = _eval_decls decls ctx ([], [])
-let eval_decls_toplevel (decls: (vdef * elexp) list list) ctx = +let eval_decls_toplevel (decls: (vname * elexp) list list) ctx = (* Add toplevel decls function *) List.fold_left (fun ctx decls -> eval_decls decls ctx) ctx decls
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -1,6 +1,6 @@ (* lexp.ml --- Lambda-expressions: the core language.
-Copyright (C) 2011-2016 Free Software Foundation, Inc. +Copyright (C) 2011-2017 Free Software Foundation, Inc.
Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -34,7 +34,7 @@ open Grammar (* open Unify *) module S = Subst
-type vdef = U.vdef +type vname = U.vname type vref = U.vref
type label = symbol @@ -63,25 +63,25 @@ type ltype = lexp | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level | Sort of U.location * sort - | Builtin of vdef * ltype * lexp AttributeMap.t option + | Builtin of vname * ltype * lexp AttributeMap.t option | Var of vref | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) - | Let of U.location * (vdef * lexp * ltype) list * lexp - | Arrow of arg_kind * vdef option * ltype * U.location * lexp - | Lambda of arg_kind * vdef * ltype * lexp + | Let of U.location * (vname * lexp * ltype) list * lexp + | Arrow of arg_kind * vname option * ltype * U.location * lexp + | Lambda of arg_kind * vname * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) | Inductive of U.location * label - * ((arg_kind * vdef * ltype) list) (* formal Args *) - * ((arg_kind * vdef option * ltype) list) SMap.t + * ((arg_kind * vname * ltype) list) (* formal Args *) + * ((arg_kind * vname option * ltype) list) SMap.t | Cons of lexp * symbol (* = Type info * ctor_name *) | Case of U.location * lexp * ltype (* The type of the return value of all branches *) - * (U.location * (arg_kind * vdef option) list * lexp) SMap.t - * (vdef option * lexp) option (* Default. *) + * (U.location * (arg_kind * vname option) list * lexp) SMap.t + * (vname option * lexp) option (* Default. *) (* The `subst` only applies to the lexp associated * with the metavar's index (i.e. its "value"), not to the ltype. *) - | Metavar of int * subst * vdef * ltype + | Metavar of int * subst * vname * ltype (* (* For logical metavars, there's no substitution. *) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -125,14 +125,9 @@ module VMap = Map.Make (struct type t = int let compare = compare end) type meta_subst = lexp VMap.t type constraints = (lexp * lexp) list
-(* What people do to statisfy Ocaml type inference ...*) -let empty_meta_subst = - let lxp = Var((U.dummy_location, "dummy"), -1) in - let v = VMap.empty in - let c = VMap.add 1 lxp v in VMap.remove 1 c +let empty_meta_subst : meta_subst = VMap.empty
-let empty_constraint = - let lxp = Var((U.dummy_location, "dummy"), -1) in List.tl [(lxp, lxp)] +let empty_constraint : constraints = []
let impossible = Imm Sexp.Epsilon
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2017 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -168,7 +168,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = " because"; lexp_string ltype' ^ " != " ^ lexp_string ltype])
-let ctx_extend (ctx: elab_context) (var : vdef option) def ltype = +let ctx_extend (ctx: elab_context) (var : vname option) def ltype = elab_check_proper_type ctx ltype var; ectx_extend ctx var def ltype
@@ -805,7 +805,7 @@ and infer_call ctx (func, ltp) (sargs: sexp list) = and lexp_parse_inductive ctors ctx =
let make_args (args:(arg_kind * pvar option * pexp) list) ctx - : (arg_kind * vdef option * ltype) list = + : (arg_kind * vname option * ltype) list = let rec loop args acc ctx = match args with | [] -> (List.rev acc) @@ -910,8 +910,8 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) =
and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) - (defs : (vdef * pexp * ltype) list) - : (vdef * lexp * ltype) list * elab_context = + (defs : (vname * pexp * ltype) list) + : (vname * lexp * ltype) list * elab_context = let (declmap, nctx) = List.fold_right (fun ((_, vname) as v, pexp, ltp) (map, nctx) -> @@ -936,8 +936,8 @@ and lexp_decls_1 (ectx : elab_context) (* External ctx. *) (nctx : elab_context) (* New context. *) (pending_decls : (location * ltype) SMap.t) (* Pending type decls. *) - (pending_defs : (vdef * pexp * ltype) list) (* Pending definitions. *) - : (vdef * lexp * ltype) list * pdecl list * elab_context = + (pending_defs : (vname * pexp * ltype) list) (* Pending definitions. *) + : (vname * lexp * ltype) list * pdecl list * elab_context =
match pdecls with | [] -> (if not (SMap.is_empty pending_decls) then @@ -1004,7 +1004,7 @@ and lexp_decls_1 else fatal l "Context changed in already changed context")
-and lexp_p_decls pdecls ctx: ((vdef * lexp * ltype) list list * elab_context) = +and lexp_p_decls pdecls ctx: ((vname * lexp * ltype) list list * elab_context) = if pdecls = [] then [], ctx else let decls, pdecls, nctx = lexp_decls_1 pdecls ctx ctx SMap.empty [] in let declss, nnctx = lexp_p_decls pdecls nctx in
===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -1,6 +1,6 @@ (* util.ml --- Misc definitions for Typer. -*- coding: utf-8 -*-
-Copyright (C) 2011-2013, 2016 Free Software Foundation, Inc. +Copyright (C) 2011-2017 Free Software Foundation, Inc.
Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -35,11 +35,11 @@ let dummy_location = {file=""; line=0; column=0} (* Occurrence of a variable's symbol: we use DeBruijn index, and for * debugging purposes, we remember the name that was used in the source * code. *) -type vdef = location * string +type vname = location * string type db_index = int (* DeBruijn index. *) type db_offset = int (* DeBruijn index offset. *) type db_revindex = int (* DeBruijn index counting from the root. *) -type vref = vdef * db_index +type vref = vname * db_index
type bottom = | B_o_t_t_o_m_ of bottom
View it on GitLab: https://gitlab.com/monnier/typer/commit/84313d0d723193e441b2177f551d9693b2a3...