basic haskell operator syntax

examples/algebra.pg

@@ -23,7 +23,7 @@ section BasicDefinitions
     -- a binary operation is a function `A → A → A`
     def binop := A → A → A;
 
-    -- fix some binary operation `op`
+    -- fix some binary operation `*`
     variable (* : binop);
     infixl 20 *;
 
@@ -64,34 +64,31 @@ def semigroup (S : ★) (op : binop S) : ★ := assoc S op;
 
 section Monoid
 
-    -- Let `M` be a set with binary operation `op` and element `e`.
+    -- Let `M` be a set with binary operation `*` and element `e`.
-    variable (M : ★) (op : binop M) (e : M);
+    variable (M : ★) (* : binop M) (e : M);
-
-    -- We'll use `*` as an infix shorthand for `op`
-    def * (a b : M) := op a b;
     infixl 50 *;
 
-    -- a set `M` with binary operation `op` and element `e` is a monoid 
+    -- a set `M` with binary operation `(*)` and element `e` is a monoid 
-    def monoid : ★ := (semigroup M op) ∧ (id M op e);
+    def monoid : ★ := (semigroup M (*)) ∧ (id M (*) e);
 
     -- Suppose `(M, *, e)` is a monoid
     hypothesis (Hmonoid : monoid);
 
     -- some "getters" for `monoid` so we don't have to do a bunch of very verbose
     -- and-eliminations every time we want to use something
-    def id_lm : id_l M op e :=
+    def id_lm : id_l M (*) e :=
-        and_elim_l (id_l M op e) (id_r M op e)
+        and_elim_l (id_l M (*) e) (id_r M (*) e)
-            (and_elim_r (semigroup M op) (id M op e) Hmonoid);
+            (and_elim_r (semigroup M (*)) (id M (*) e) Hmonoid);
 
-    def id_rm : id_r M op e :=
+    def id_rm : id_r M (*) e :=
-        and_elim_r (id_l M op e) (id_r M op e)
+        and_elim_r (id_l M (*) e) (id_r M (*) e)
-            (and_elim_r (semigroup M op) (id M op e) Hmonoid);
+            (and_elim_r (semigroup M (*)) (id M (*) e) Hmonoid);
 
-    def assoc_m : assoc M op := and_elim_l (semigroup M op) (id M op e) Hmonoid;
+    def assoc_m : assoc M (*) := and_elim_l (semigroup M (*)) (id M (*) e) Hmonoid;
 
     -- now we can prove that, for any monoid, if `a` is a left identity, then it
     -- must be "the" identity
-    def monoid_id_l_implies_identity (a : M) (H : id_l M op a) : eq M a e :=
+    def monoid_id_l_implies_identity (a : M) (H : id_l M (*) a) : eq M a e :=
             -- WTS a = a * e = e
             -- we can use `eq_trans` to glue proofs of `a = a * e` and `a * e = e` together
             eq_trans M a (a * e) e
@@ -105,7 +102,7 @@ section Monoid
                 (H e);
 
     -- the analogous result for right identities
-    def monoid_id_r_implies_identity (a : M) (H : id_r M op a) : eq M a e :=
+    def monoid_id_r_implies_identity (a : M) (H : id_r M (*) a) : eq M a e :=
             -- this time, we'll show `a = e * a = e`
             eq_trans M a (e * a) e
 
@@ -121,28 +118,27 @@ end Monoid
 
 section Group
 
-    variable (G : ★) (op : binop G) (e : G) (i : unop G);
+    variable (G : ★) (* : binop G) (e : G) (i : unop G);
 
-    def * (a b : G) := op a b;
     infixl 50 *;
 
     -- groups are just monoids with inverses
-    def has_inverses : ★ := forall (a : G), inv G op e a (i a);
+    def has_inverses : ★ := forall (a : G), inv G (*) e a (i a);
 
-    def group : ★ := (monoid G op e) ∧ has_inverses;
+    def group : ★ := (monoid G (*) e) ∧ has_inverses;
 
     hypothesis (Hgroup : group);
 
     -- more "getters"
-    def monoid_g : monoid G op e := and_elim_l (monoid G op e) has_inverses Hgroup;
+    def monoid_g : monoid G (*) e := and_elim_l (monoid G (*) e) has_inverses Hgroup;
-    def assoc_g : assoc G op := assoc_m G op e monoid_g;
+    def assoc_g : assoc G (*) := assoc_m G (*) e monoid_g;
-    def id_lg : id_l G op e := id_lm G op e (and_elim_l (monoid G op e) has_inverses Hgroup);
+    def id_lg : id_l G (*) e := id_lm G (*) e (and_elim_l (monoid G (*) e) has_inverses Hgroup);
-    def id_rg : id_r G op e := id_rm G op e (and_elim_l (monoid G op e) has_inverses Hgroup);
+    def id_rg : id_r G (*) e := id_rm G (*) e (and_elim_l (monoid G (*) e) has_inverses Hgroup);
-    def inv_g : forall (a : G), inv G op e a (i a) := and_elim_r (monoid G op e) has_inverses Hgroup;
+    def inv_g : forall (a : G), inv G (*) e a (i a) := and_elim_r (monoid G (*) e) has_inverses Hgroup;
-    def left_inverse (a b : G)  := inv_l G op e a b;
+    def left_inverse (a b : G)  := inv_l G (*) e a b;
-    def right_inverse (a b : G) := inv_r G op e a b;
+    def right_inverse (a b : G) := inv_r G (*) e a b;
-    def inv_lg (a : G) : left_inverse a (i a)  := and_elim_l (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g a);
+    def inv_lg (a : G) : left_inverse a (i a)  := and_elim_l (inv_l G (*) e a (i a)) (inv_r G (*) e a (i a)) (inv_g a);
-    def inv_rg (a : G) : right_inverse a (i a) := and_elim_r (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g a);
+    def inv_rg (a : G) : right_inverse a (i a) := and_elim_r (inv_l G (*) e a (i a)) (inv_r G (*) e a (i a)) (inv_g a);
 
     -- An interesting theorem: left inverses are unique, i.e. if b * a = e, then b = a^-1
     def left_inv_unique (a b : G) (h : left_inverse a b) : eq G b (i a) :=
@@ -157,7 +153,7 @@ section Group
         -- b * e = a^-1
         (eq_trans G (b * e) (b * (a * i a)) (i a)
             --b * e = b * (a * a^-1)
-            (eq_cong G G e (a * i a) (op b)
+            (eq_cong G G e (a * i a) ((*) b)
                 -- e = a * a^-1
                 (eq_sym G (a * i a) e (inv_rg a)))
             -- b * (a * a^-1) = a^-1
@@ -196,7 +192,7 @@ section Group
                 -- a^-1 * (a * b) = a^-1
                 (eq_trans G (i a * (a * b)) (i a * e) (i a)
                     -- a^-1 * (a * b) = a^-1 * e
-                    (eq_cong G G (a * b) e (op (i a)) h)
+                    (eq_cong G G (a * b) e ((*) (i a)) h)
 
                     -- a^-1 * e = a^-1
                     (id_rg (i a)))));

examples/category.pg

@@ -3,13 +3,13 @@
 section Category
     variable
         (Obj  : ★)
-        (~>   : Obj -> Obj -> ★);
+        (~>   : Obj → Obj → ★);
 
     infixr 10 ~>;
 
     variable
         (id   : forall (A     : Obj), A ~> A)
-        (comp : forall (A B C : Obj), A ~> B -> B ~> C -> A ~> C);
+        (comp : forall (A B C : Obj), A ~> B → B ~> C → A ~> C);
 
     hypothesis
         (id_l  : forall (A B     : Obj) (f : A ~> B), eq (A ~> B) (comp A A B (id A) f) f)

examples/classical.pg

@@ -11,7 +11,7 @@ def dne (P : ★) (nnp : not (not P)) : P :=
         (fun (np : not P) => nnp np P);
 
 -- ((P => Q) => P) => P
-def peirce (P Q : ★) (h : (P -> Q) -> P) : P :=
+def peirce (P Q : ★) (h : (P → Q) → P) : P :=
     or_elim P (not P) P (em P)
         (fun (p : P) => p)
         (fun (np : not P) => h (fun (p : P) => np p Q));

examples/computation.pg

@@ -5,21 +5,21 @@
 -- computation with them
 
 -- the natural number `n` is encoded as the function taking any function
--- `A -> A` and repeating it `n` times
+-- `A → A` and repeating it `n` times
-def nat : ★ := forall (A : ★), (A -> A) -> A -> A;
+def nat : ★ := forall (A : ★), (A → A) → A → A;
 
 -- zero is the constant function
-def zero : nat := fun (A : ★) (f : A -> A) (x : A) => x;
+def zero : nat := fun (A : ★) (f : A → A) (x : A) => x;
 
 -- `suc n` composes one more `f` than `n`
-def suc : nat -> nat := fun (n : nat) (A : ★) (f : A -> A) (x : A) => f ((n A f) x);
+def suc : nat → nat := fun (n : nat) (A : ★) (f : A → A) (x : A) => f ((n A f) x);
 
 -- addition can be encoded as usual
-def + : nat -> nat -> nat := fun (n m : nat) (A : ★) (f : A -> A) (x : A) => (m A f) (n A f x);
+def + : nat → nat → nat := fun (n m : nat) (A : ★) (f : A → A) (x : A) => (m A f) (n A f x);
 infixl 20 +;
 
 -- likewise for multiplication
-def * : nat -> nat -> nat := fun (n m : nat) (A : ★) (f : A -> A) (x : A) => (m A (n A f)) x;
+def * : nat → nat → nat := fun (n m : nat) (A : ★) (f : A → A) (x : A) => (m A (n A f)) x;
 infixl 30 *;
 
 -- unforunately, it is impossible to prove induction on Church numerals,

examples/peano.pg

@@ -49,15 +49,15 @@ axiom zero : nat;
 axiom suc (n : nat) : nat;
 
 -- axiom 7: If S n = S m, then n = m.
-axiom suc_inj : forall (n m : nat), eq nat (suc n) (suc m) -> eq nat n m;
+axiom suc_inj : forall (n m : nat), eq nat (suc n) (suc m) → eq nat n m;
 
 -- axiom 8: No successor of any natural number is zero.
 axiom suc_nonzero : forall (n : nat), not (eq nat (suc n) zero);
 
 -- axiom 9: Induction! For any proposition P on natural numbers, if P(0) holds,
 -- and if for every natural number n, P(n) ⇒ P(S n), then P holds for all n.
-axiom nat_ind : forall (P : nat -> ★), P zero -> (forall (n : nat), P n -> P (suc n))
+axiom nat_ind : forall (P : nat → ★), P zero → (forall (n : nat), P n → P (suc n))
-    -> forall (n : nat), P n;
+    → forall (n : nat), P n;
 
 -- }}}
 
@@ -130,8 +130,8 @@ def suc_or_zero : forall (n : nat), szc n :=
 -- So, we will take the time to prove the following theorem.
 --
 -- Theorem (recursive definitions):
--- For every type A, element z : A, and function fS : nat -> A -> A, there
+-- For every type A, element z : A, and function fS : nat → A → A, there
--- exists a unique function f : nat -> A satisfying
+-- exists a unique function f : nat → A satisfying
 -- 1)                       f 0 = z
 -- 2) forall n : nat, f (suc n) = fS n (f n)
 --
@@ -146,10 +146,10 @@ def suc_or_zero : forall (n : nat), szc n :=
 -- more used to perga. As such, I will go into a lot less detail on each of
 -- these proofs than in the later sections.
 --
--- Here's our game plan. We will define a relation R : nat -> A -> ★ such that
+-- Here's our game plan. We will define a relation R : nat → A → ★ such that
--- R x y iff for every relation Q : nat -> A -> ★ satisfying
+-- R x y iff for every relation Q : nat → A → ★ satisfying
 -- 1) Q 0 z and
--- 2) forall (x : nat) (y : A), Q x y -> Q (suc x) (fS x y),
+-- 2) forall (x : nat) (y : A), Q x y → Q (suc x) (fS x y),
 -- Q x y.
 -- In more mathy lingo, we take R to be the intersection of every relation
 -- satisfying 1 and 2. From there we will, with much effort, prove that R is
@@ -157,31 +157,31 @@ def suc_or_zero : forall (n : nat), szc n :=
 
 section RecursiveDefs
 
--- First, fix an A, z : A, and fS : nat -> A -> A
+-- First, fix an A, z : A, and fS : nat → A → A
-variable (A : ★) (z : A) (fS : nat -> A -> A);
+variable (A : ★) (z : A) (fS : nat → A → A);
 
 -- {{{ Defining R
 -- Here is condition 1 formally expressed in perga.
-def cond1 (Q : nat -> A -> ★) := Q zero z;
+def cond1 (Q : nat → A → ★) := Q zero z;
 
 -- Likewise for condition 2.
-def cond2 (Q : nat -> A -> ★) :=
+def cond2 (Q : nat → A → ★) :=
-    forall (n : nat) (y : A), Q n y -> Q (suc n) (fS n y);
+    forall (n : nat) (y : A), Q n y → Q (suc n) (fS n y);
 
 -- From here we can define R.
 def rec_rel (x : nat) (y : A) :=
-    forall (Q : nat -> A -> ★), cond1 Q -> cond2 Q -> Q x y;
+    forall (Q : nat → A → ★), cond1 Q → cond2 Q → Q x y;
 -- }}}
 
 -- {{{ R is total
-def total (A B : ★) (R : A -> B -> ★) := forall (a : A), exists B (R a);
+def total (A B : ★) (R : A → B → ★) := forall (a : A), exists B (R a);
 
 def rec_rel_cond1 : cond1 rec_rel :=
-    fun (Q : nat -> A -> ★) (h1 : cond1 Q) (h2 : cond2 Q) => h1;
+    fun (Q : nat → A → ★) (h1 : cond1 Q) (h2 : cond2 Q) => h1;
 
 def rec_rel_cond2 : cond2 rec_rel :=
     fun (n : nat) (y : A) (h : rec_rel n y)
-        (Q : nat -> A -> ★) (h1 : cond1 Q) (h2 : cond2 Q) =>
+        (Q : nat → A → ★) (h1 : cond1 Q) (h2 : cond2 Q) =>
         h2 n y (h Q h1 h2);
 
 def rec_rel_total : total nat A rec_rel :=
@@ -215,7 +215,7 @@ def rec_rel_alt (x : nat) (y : A) := alt_cond1 x y ∨ alt_cond2 x y;
 -- {{{ R = R2
 
 -- {{{ R2 ⊆ R
-def R2_sub_R_case1 (x : nat) (y : A) : alt_cond1 x y -> rec_rel x y :=
+def R2_sub_R_case1 (x : nat) (y : A) : alt_cond1 x y → rec_rel x y :=
     fun (case1 : alt_cond1 x y) =>
         let (x0 := and_elim_l (x = zero) (eq A y z) case1)
             (yz := and_elim_r (x = zero) (eq A y z) case1)
@@ -224,7 +224,7 @@ def R2_sub_R_case1 (x : nat) (y : A) : alt_cond1 x y -> rec_rel x y :=
             (eq_sym nat x zero x0) (fun (n : nat) => rec_rel n y) a1
         end;
 
-def R2_sub_R_case2 (x : nat) (y : A) : alt_cond2 x y -> rec_rel x y :=
+def R2_sub_R_case2 (x : nat) (y : A) : alt_cond2 x y → rec_rel x y :=
     fun (case2 : alt_cond2 x y) =>
         let (h1 := cond_x2 x y)
             (h2 := cond_y2 x y)
@@ -246,7 +246,7 @@ def R2_sub_R_case2 (x : nat) (y : A) : alt_cond2 x y -> rec_rel x y :=
             end)
         end;
 
-def R2_sub_R (x : nat) (y : A) : rec_rel_alt x y -> rec_rel x y :=
+def R2_sub_R (x : nat) (y : A) : rec_rel_alt x y → rec_rel x y :=
     fun (h : rec_rel_alt x y) =>
         or_elim (alt_cond1 x y) (alt_cond2 x y) (rec_rel x y) h
         (R2_sub_R_case1 x y)
@@ -278,7 +278,7 @@ def R2_cond2 : cond2 rec_rel_alt :=
     end;
 
 
-def R_sub_R2 (x : nat) (y : A) : rec_rel x y -> rec_rel_alt x y :=
+def R_sub_R2 (x : nat) (y : A) : rec_rel x y → rec_rel_alt x y :=
     fun (h : rec_rel x y) => h rec_rel_alt R2_cond1 R2_cond2;
 -- }}}
 
@@ -286,12 +286,12 @@ def R_sub_R2 (x : nat) (y : A) : rec_rel x y -> rec_rel_alt x y :=
 
 -- {{{ R2 (hence R) is functional
 
-def fl_in (A B : ★) (R : A -> B -> ★) (x : A) := forall (y1 y2 : B),
+def fl_in (A B : ★) (R : A → B → ★) (x : A) := forall (y1 y2 : B),
-    R x y1 -> R x y2 -> eq B y1 y2;
+    R x y1 → R x y2 → eq B y1 y2;
 
-def fl (A B : ★) (R : A -> B -> ★) := forall (x : A), fl_in A B R x;
+def fl (A B : ★) (R : A → B → ★) := forall (x : A), fl_in A B R x;
 
-def R2_zero (y : A) : rec_rel_alt zero y -> eq A y z :=
+def R2_zero (y : A) : rec_rel_alt zero y → eq A y z :=
     let (cx2 := cond_x2 zero y)
         (cy2 := cond_y2 zero y)
     in fun (h : rec_rel_alt zero y) =>
@@ -305,7 +305,7 @@ def R2_zero (y : A) : rec_rel_alt zero y -> eq A y z :=
                 (eq A y z)))
     end;
 
-def R2_suc (x2 : nat) (y : A) : rec_rel_alt (suc x2) y -> exists A (cond_y2 (suc x2) y x2) :=
+def R2_suc (x2 : nat) (y : A) : rec_rel_alt (suc x2) y → exists A (cond_y2 (suc x2) y x2) :=
     let (x    := suc x2)
         (cx2  := cond_x2 x y)
         (cy2  := cond_y2 x y)
@@ -386,21 +386,21 @@ def rec_def (x : nat) : A :=
 -- existential, it still satisfies the property it definitionally is supposed
 -- to satisfy. This annoying problem would be subverted with proper Σ-types,
 -- provided they had η-equality.
-axiom definite_description (A : ★) (P : A -> ★) (h : exists A P) :
+axiom definite_description (A : ★) (P : A → ★) (h : exists A P) :
     P (exists_elim A A P h (fun (x : A) (_ : P x) => x));
 
 -- Now we can use this axiom to prove that R n (rec_def n).
 def rec_def_sat (x : nat) : rec_rel x (rec_def x) :=
     definite_description A (rec_rel x) (rec_rel_total x);
 
-def eq1 (f : nat -> A) := eq A (f zero) z;
+def eq1 (f : nat → A) := eq A (f zero) z;
 
-def eq2 (f : nat -> A) := forall (n : nat), eq A (f (suc n)) (fS n (f n));
+def eq2 (f : nat → A) := forall (n : nat), eq A (f (suc n)) (fS n (f n));
 
 -- f zero = z
 def rec_def_sat_zero : eq1 rec_def := R_functional zero (rec_def zero) z (rec_def_sat zero) rec_rel_cond1;
 
--- f n = y -> f (suc n) = fS n y
+-- f n = y → f (suc n) = fS n y
 def rec_def_sat_suc : eq2 rec_def := fun (n : nat) =>
     R_functional (suc n) (rec_def (suc n)) (fS n (rec_def n)) (rec_def_sat (suc n)) (rec_rel_cond2 n (rec_def n) (rec_def_sat n));
 
@@ -408,7 +408,7 @@ def rec_def_sat_suc : eq2 rec_def := fun (n : nat) =>
 
 -- {{{ The function satisfying these equations is unique
 
-def rec_def_unique (f g : nat -> A) (h1f : eq1 f) (h2f : eq2 f) (h1g : eq1 g) (h2g : eq2 g)
+def rec_def_unique (f g : nat → A) (h1f : eq1 f) (h2f : eq2 f) (h1g : eq1 g) (h2g : eq2 g)
     : forall (n : nat), eq A (f n) (g n) :=
         nat_ind (fun (n : nat) => eq A (f n) (g n))
         -- base case: f 0 = g 0
@@ -442,7 +442,7 @@ end RecursiveDefs
 def psuc (_ r : nat) := suc r;
 
 -- And here's plus!
-def plus (n : nat) : nat -> nat := rec_def nat n psuc;
+def plus (n : nat) : nat → nat := rec_def nat n psuc;
 
 -- And here's an infix version of it
 def + (n m : nat) : nat := plus n m;

lib/Eval.hs

@@ -52,18 +52,6 @@ envLookupVal n = asks ((_val <$>) . M.lookup n) >>= maybe (throwError $ UnboundV
 envLookupTy :: Text -> ReaderT Env Result Expr
 envLookupTy n = asks ((_ty <$>) . M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure
 
--- reduce until β reducts or let simplifications are impossible in head position
-whnf :: Expr -> ReaderT Env Result Expr
-whnf (App (Abs _ _ _ v) n) = whnf $ subst 0 n v
-whnf (App m n) = do
-    m' <- whnf m
-    if m == m'
-        then pure $ App m n
-        else whnf $ App m' n
-whnf (Free n) = envLookupVal n >>= whnf
-whnf (Let _ _ v b) = whnf $ subst 0 v b
-whnf e = pure e
-
 reduce :: Expr -> ReaderT Env Result Expr
 reduce (App (Abs _ _ _ v) n) = pure $ subst 0 n v
 reduce (App m n) = App <$> reduce m <*> reduce n
@@ -80,6 +68,18 @@ normalize e = do
         then pure e
         else normalize e'
 
+-- reduce until β reducts or let simplifications are impossible in head position
+whnf :: Expr -> ReaderT Env Result Expr
+whnf (App (Abs _ _ _ v) n) = whnf $ subst 0 n v
+whnf (App m n) = do
+    m' <- whnf m
+    if m == m'
+        then pure $ App m n
+        else whnf $ App m' n
+whnf (Free n) = envLookupVal n >>= whnf
+whnf (Let _ _ v b) = whnf $ subst 0 v b
+whnf e = pure e
+
 betaEquiv :: Expr -> Expr -> ReaderT Env Result Bool
 betaEquiv e1 e2
     | e1 == e2 = pure True

lib/Parser.hs

@@ -10,7 +10,7 @@ import qualified Data.Text as T
 import Errors (Error (..))
 import IR
 import Preprocessor
-import Text.Megaparsec (MonadParsec (..), ParsecT, ShowErrorComponent (..), between, choice, errorBundlePretty, label, runParserT, try)
+import Text.Megaparsec (MonadParsec (..), ParsecT, ShowErrorComponent (..), choice, errorBundlePretty, label, runParserT, try, between)
 import Text.Megaparsec.Char
 import qualified Text.Megaparsec.Char.Lexer as L
 
@@ -39,6 +39,9 @@ skipSpace =
 lexeme :: Parser a -> Parser a
 lexeme = L.lexeme skipSpace
 
+parens :: Parser a -> Parser a
+parens = between (char '(') (char ')')
+
 symbol :: Text -> Parser ()
 symbol = void . L.symbol skipSpace
 
@@ -64,7 +67,7 @@ pVar :: Parser IRExpr
 pVar = label "variable" $ lexeme $ Var <$> pIdentifier
 
 pParamGroup :: Parser Text -> Parser [Param]
-pParamGroup ident = lexeme $ label "parameter group" $ between (char '(') (char ')') $ do
+pParamGroup ident = lexeme $ label "parameter group" $ parens $ do
     idents <- some ident
     symbol ":"
     ty <- pIRExpr
@@ -157,8 +160,11 @@ pSquare = lexeme $ (symbol "□" <|> symbol "[]") >> option (Level 0) (Level <$>
 pSort :: Parser IRExpr
 pSort = lexeme $ pStar <|> pSquare
 
+pOpSection :: Parser IRExpr
+pOpSection = lexeme $ parens $ Var <$> pSymbol
+
 pTerm :: Parser IRExpr
-pTerm = lexeme $ label "term" $ choice [pSort, pVar, between (char '(') (char ')') pIRExpr]
+pTerm = lexeme $ label "term" $ choice [pSort, pVar, try pOpSection, parens pIRExpr]
 
 pInfix :: Parser IRExpr
 pInfix = parseWithPrec 0