From 959f425afa065b9844ec5960817b6605cb1c7f54 Mon Sep 17 00:00:00 2001 From: William Ball Date: Sun, 1 Dec 2024 18:16:45 -0800 Subject: [PATCH] updated README with changes --- README.org | 33 ++++++++++++++++++--------------- 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/README.org b/README.org index 8ccc9ac..03e8750 100644 --- a/README.org +++ b/README.org @@ -18,11 +18,11 @@ To be perfectly clear, =λ= abstractions can be written with either "λ" or "fun =Let= expressions have syntax shown below. #+begin_src - let ( ( := ) )+ in end + let ( ( (: )? := ) )+ in end #+end_src Below is a more concrete example. #+begin_src - let (a := (and_elim_l A (and B C) h)) + let (a : A := (and_elim_l A (and B C) h)) (bc := (and_elim_r A (and B C) h)) (b := (and_elim_l B C bc)) (c := (and_elim_r B C bc)) @@ -38,19 +38,20 @@ You can also directly bind functions. Here's an example. #+end_src The syntax for binding functions is just like with definitions. -Definitions have abstract syntax as shown below. +Definitions and axioms have abstract syntax as shown below. #+begin_src - ( : )* : ? := | axiom; + def ( : )* : ? := ; + axiom ( : )* : ; #+end_src -(The distinction between == and == is for emphasis; they are the exact same syntactic category.) Here's a couple definitions of the =const= function from above showing the options with the syntax, and a more complex example declaring functional extensionality as an axiom (assuming equality has been previously defined having type =eq : Π (A : *) → A → A → *=). Duplicate definitions are not normally allowed and will result in an error. +(The distinction between == and == is purely for emphasis; they are the exact same syntactic category.) Here's a couple definitions of the =const= function from above showing the options with the syntax, and a more complex example declaring functional extensionality as an axiom (assuming equality has been previously defined having type =eq : Π (A : *) → A → A → *=). Duplicate definitions are not normally allowed and will result in an error. #+begin_src - const := λ (α : *) ⇒ λ (β : *) ⇒ λ (x : α) => λ (y : β) => x; - const : ∀ (α β : *), α → β → α := fun (α β : *) (x : α) (y : β) ⇒ x; - const (α β : *) (x : α) (y : β) : α := x; + def const := λ (α : *) ⇒ λ (β : *) ⇒ λ (x : α) => λ (y : β) => x; + def const : ∀ (α β : *), α → β → α := fun (α β : *) (x : α) (y : β) ⇒ x; + def const (α β : *) (x : α) (y : β) : α := x; - funext (A B : *) (f g : A → B) : (∀ (x : A), eq B (f x) (g x)) → eq (A → B) f g := axiom; + axiom funext (A B : *) (f g : A → B) : (∀ (x : A), eq B (f x) (g x)) → eq (A → B) f g; #+end_src -Type ascriptions are optional. If included, =perga= will check to make sure your definition matches the ascription, and, if so, will remember the way your wrote the type when printing inferred types, which is particularly handy when using abbreviations for complex types. =perga= has no problem inferring the types of top-level definitions, as they are completely determined by the term, but I recommend including ascriptions most of the time, as they serve as a nice piece of documentation, help guide the implementation process, and make sure you are implementing the type you think you are. +Type ascriptions are optional in both definitions and =let= bindings. If included, =perga= will check to make sure your definition matches the ascription, and, if so, will remember the way your wrote the type when printing inferred types, which is particularly handy when using abbreviations for complex types. =perga= has no problem inferring the types of top-level definitions, as they are completely determined by the term, but I recommend including ascriptions most of the time, as they serve as a nice piece of documentation, help guide the implementation process, and make sure you are implementing the type you think you are. If the RHS of a definition is =axiom=, then =perga= will assume that the identifier is an inhabitant of the type ascribed to it (as such when using axioms, a type ascription is required). This allows you to use axioms. @@ -59,7 +60,7 @@ Line comments are =--= like in Haskell, and block comments are =[* *]= somewhat There isn't a proper module system (yet), but you can include other files in a dumb, C preprocessor way by using =@include = (NOTE: this unfortunately messes up line numbers in error messages). Filepaths are relative to the current file. Additionally, =@include= automatically keeps track of what has been included, so duplicate inclusions are skipped, meaning no include guards are necessary. * Usage -Running =perga= without any arguments drops you into a basic repl. From here, you can type in definitions which =perga= will typecheck. Previous definitions are accessible in future definitions. The usual readline keybindings are available, including navigating history, which is saved between sessions (in =~/.cache/perga/history=). In the repl, you can enter ":q", press C-c, or press C-d to quit. Entering ":e" shows everything that has been defined along with their types. Entering ":t " prints the type of a particular identifier, while ":v " prints its value. Entering ":n " will fully normalize (including unfolding definitions) an expression, while ":w " will reduce it to weak head normal form. Finally ":l " loads a file. +Running =perga= without any arguments drops you into a basic repl. From here, you can type in definitions which =perga= will typecheck. Previous definitions are accessible in future definitions. The usual readline keybindings are available, including navigating history, which is saved between sessions (in =~/.cache/perga/history=). In the repl, you can enter ":q", press C-c, or press C-d to quit. Entering ":e" shows everything that has been defined along with their types. If you want to see the value of an identifier defined in the environment, you can enter ":v ". Entering ":t " prints the type of an expression. Entering ":n " will fully normalize (including unfolding definitions) an expression, while ":w " will reduce it to weak head normal form. Finally ":l " loads a file. Here's an example session showing the capabilities of the repl. #+begin_src text @@ -160,7 +161,7 @@ This indicates that, when evaluating =Hxy Hx=, it was expecting something of typ ** Substantive *** TODO Sections -Coq-style sections would be very handy, and probably /relatively/ easy to implement (compared to everything else on this todo list). Upon parsing a definition inside a section, will somehow need to look ahead to see what variables are used to see how I need to modify =binders=, or just make every definition require every section variable as an argument. +Coq-style sections would be very handy, and probably /relatively/ easy to implement (compared to everything else on this todo list), especially now that we have an [[Multiple levels of AST][intermediate representation]]. *** TODO Inference Not decidable, but I might be able to implement some basic unification algorithm, or switch to bidirectional type checking. This isn't super necessary though, I find leaving off the types of arguments to generally be a bad idea, but in some cases it can be handy, especially not at the top level. @@ -169,7 +170,7 @@ Not decidable, but I might be able to implement some basic unification algorithm Much, much more useful than [[Inference][inference]], implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none. *** TODO Module System -A proper module system would be wonderful. To me, ML style modules with structures, signatures, and functors seems like the right way to handle algebraic structures for a relatively simple language, rather than records (or, worse, a bunch of =and='s like I currently have; especially painful without [[Implicits][implicits]]) or type classes (probably much harder, but could be nicer), but any way of managing scope, importing files, etc. is a necessity. The [[https://www.cambridge.org/core/services/aop-cambridge-core/content/view/B573FA00832D55D4878863DE1725D90B/S0956796814000264a.pdf/f-ing-modules.pdf][F-ing modules]] paper is probably a good reference. +A proper module system would be wonderful. To me, ML style modules with structures, signatures, and functors seems like the right way to handle algebraic structures for a relatively simple language, rather than records (or, worse, a bunch of =and='s like I currently have; especially painful without [[Implicits][implicits]]) or type classes (probably much harder, but could be nicer), but any way of managing scope, importing files, etc. is a necessity. The [[https://www.cambridge.org/core/services/aop-cambridge-core/content/view/B573FA00832D55D4878863DE1725D90B/S0956796814000264a.pdf/f-ing-modules.pdf][F-ing modules]] paper is probably a good reference. Now that I have an [[Multiple levels of AST][intermediate representation]], following in /F-ing modules/'s footsteps and implementing modules purely through elaboration should be possible. *** DONE Universes? Not super necessary, but occasionally extremely useful. Could be fun, idk. @@ -178,6 +179,8 @@ I was looking into bidirectional typing and came across a description of univers Also, everything ends up impredicative (no =* : *=, but quantifying over =*i= still leaves you in =*i=), and my implementation of impredicativity feels a little sketchy. There might be paradoxes lurking. It would be easy to switch it over to being predicative, but, without inductive types or at least more built-in types, logical connectives can only be defined impredicatively, so that will have to wait until we have inductive definitions. +I may follow in Coq's footsteps and switch universe hierarchies to something like =* : □ : □₁ : □₂ : □₃ : ...=, where all the =□ᵢ= are predicative and =*= is impredicative (analogous to =Prop= and =Type i=). For now at least, we definitely need at least the lowest sort to be impredicative to allow for impredicative definitions of connectives. + *** TODO Universe polymorphism I have [[Universes?][universes]], but without universe polymorphism, they're basically useless, or at least I am unable to find a practical use for them. (When would you want to quantify over e.g. kinds specifically?) @@ -204,8 +207,8 @@ Probably a smart idea. *** TODO More incremental parsing/typechecking Right now, if there's a failure, everything just stops immediately. More incremental parsing/typechecking could pave the way for more interactivity, e.g. development with holes, an LSP server, etc., not to mention better error messages. -*** TODO Multiple levels of AST -Right now, the parsing and typechecking kind of happens all at once on a single syntax representation. As I add fancier and fancier elaboration, it might be a good idea to have multiple syntax representations. So we'd have one level of syntax representing what is actually in the file (modulo some easy elaboration like with function definitions), and through a series of transformations transform it into something like the current =Expr= type with all the information needed for typechecking and all the complex language features removed. +*** DONE Multiple levels of AST +Added a couple types representing an intermediate representation, as well as a module responsible for elaboration (basically a function from these intermediate types to =Expr=). This /drastically/ simplified the parser, now that it is not responsible for converting to de Bruijn indices, handling the environment, and type checking all in addition to parsing. However, now that type checking is out of the parser, we lost location information for errors, making [[Improve error message][better error messages]] much more important now. I have some ideas for getting location information (and more accurate location information, instead of always pointing to the end of the most relevant definition), which should drastically improve the error messages. *** TODO Improve type checking algorithm I'm proud that I just kinda made up a working type checking algorithm, but it is clearly quite flawed. Even assuming no need to check beta equivalence, I'm pretty sure that this algorithm is approximately exponential in the length of a term, which is pretty terrible. It hasn't been a huge problem, but type checking just the term =R2_sub_R= in [[./examples/peano.pg]] takes about 1.5 seconds. Performance could easily be drastically improved with some memoization, but upgrading to an off-the-shelf bidirectional type checking algorithm seems like a good idea in general. Another problem with my current type checking algorithm is that it is very inflexible (e.g. adding optional return type ascriptions in functions, or type ascriptions in =let= bindings is currently impossible, while trivial to add with bidirectional type checking). I also have no idea how to add [[Inference][type inference]] or [[Implicits][implicits]] with how things are currently structured. A more flexible type checking algorithm, likely together with [[Multiple levels of AST][multiple levels of AST]], makes it seem more possible.