diff --git a/README.md b/README.md index 6757976..b9f135f 100644 --- a/README.md +++ b/README.md @@ -32,6 +32,28 @@ Line comments are `--` like in Haskell, and block comments are `(* *)` like ML ( 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. Entering “:n ” will fully normalize (including unfolding definitions) an expression. +Here’s an example session defining Church numerals and doing some computations with them to show the capabilities of the repl. + + > nat : * := forall (A : *), (A → A) → A → A; + > zero : nat := fun (A : *) (f : A -> A) (x : A) ⇒ x; + > :t zero + nat + > suc : nat → nat := fun (n : nat) (A : *) (f : A → A) (x : A) ⇒ f (n A f x); + > one : nat := suc zero; + > add (n m : nat) : nat := fun (A : *) (f : A → A) (x : A) ⇒ n A f (m A f x); + > :e + add : nat -> nat -> nat + nat : * + one : nat + suc : nat -> nat + zero : nat + > two : nat := suc one; + > :n add one one + λ (A : *) (f : A -> A) (x : A) . f (f x) + > :n two + λ (A : *) (f : A -> A) (x : A) . f (f x) + > :q + You can also give `perga` a filename as an argument, in which case it will typecheck every definition in the file. Upon finishing, which should be nearly instantaneous, it will print out all the definitions it parsed along with their types (like you had typed “:e” in the repl) so you can verify that it worked. @@ -87,7 +109,7 @@ Obviously not fully decidable, but I might be able to implement some basic unifi ### TODO Implicits -Much, much more useful than [inference](#org6d7253e), 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. Getting rid of stuff like [lines 213-215 of the example file](./examples/example.pg) would be amazing. +Much, much more useful than [inference](#org84d2ba6), 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. Getting rid of stuff like [lines 213-215 of the example file](./examples/example.pg) would be amazing. ### TODO Module System @@ -97,7 +119,7 @@ A proper module system would be wonderful. To me, ML style modules with structur ### TODO Universes? -Not really all that necessary, especially without [inductive definitions](#org89fc2b3), but could be fun. +Not really all that necessary, especially without [inductive definitions](#orgfd1e388), but could be fun. ### TODO Inductive Definitions @@ -164,7 +186,7 @@ I’m imagining the parser could be chosen based on the file extension or so ### TODO treesitter parser and/or emacs mode -Really not necessary, especially while the syntax is in a bit of flux, but would eventually be nice. The syntax is simple enough that a treesitter grammar shouldn’t be too hard to write. An emacs mode would especially be nice if I ever get end up implementing an [alternate syntax](#orgf8270fd), to better handle indentation, automatically adjust line numbers, etc. +Really not necessary, especially while the syntax is in a bit of flux, but would eventually be nice. The syntax is simple enough that a treesitter grammar shouldn’t be too hard to write. An emacs mode would especially be nice if I ever get end up implementing an [alternate syntax](#org058ce83), to better handle indentation, automatically adjust line numbers, etc. ### TODO TUI diff --git a/README.org b/README.org index a5b7f6a..3e7aaee 100644 --- a/README.org +++ b/README.org @@ -31,6 +31,29 @@ Line comments are =--= like in Haskell, and block comments are =(* *)= like ML ( * 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. Entering ":n " will fully normalize (including unfolding definitions) an expression. +Here's an example session defining Church numerals and doing some computations with them to show the capabilities of the repl. +#+begin_src + > nat : * := forall (A : *), (A → A) → A → A; + > zero : nat := fun (A : *) (f : A -> A) (x : A) ⇒ x; + > :t zero + nat + > suc : nat → nat := fun (n : nat) (A : *) (f : A → A) (x : A) ⇒ f (n A f x); + > one : nat := suc zero; + > add (n m : nat) : nat := fun (A : *) (f : A → A) (x : A) ⇒ n A f (m A f x); + > :e + add : nat -> nat -> nat + nat : * + one : nat + suc : nat -> nat + zero : nat + > two : nat := suc one; + > :n add one one + λ (A : *) (f : A -> A) (x : A) . f (f x) + > :n two + λ (A : *) (f : A -> A) (x : A) . f (f x) + > :q +#+end_src + You can also give =perga= a filename as an argument, in which case it will typecheck every definition in the file. Upon finishing, which should be nearly instantaneous, it will print out all the definitions it parsed along with their types (like you had typed ":e" in the repl) so you can verify that it worked. * Simple Example