wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

basic haskell operator syntax

Browse source
This commit is contained in:
William Ball 2024-12-10 23:36:34 -08:00
parent 534809bef9
commit e6f9d71c57
7 changed files with 90 additions and 88 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

60
examples/algebra.pg
View file

@ -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`.
variable (M : ★) (op : binop M) (e : M);
-- We'll use `*` as an infix shorthand for `op`
def * (a b : M) := op a b;
-- Let `M` be a set with binary operation `*` and element `e`.
variable (M : ★) (* : binop M) (e : M);
infixl 50 *;
-- a set `M` with binary operation `op` and element `e` is a monoid
def monoid : ★ := (semigroup M op) ∧ (id M op e);
-- a set `M` with binary operation `(*)` and element `e` is a monoid
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 :=
and_elim_l (id_l M op e) (id_r M op e)
(and_elim_r (semigroup M op) (id M op e) Hmonoid);
def id_lm : id_l M (*) e :=
and_elim_l (id_l M (*) e) (id_r M (*) e)
(and_elim_r (semigroup M (*)) (id M (*) e) Hmonoid);
def id_rm : id_r M op e :=
and_elim_r (id_l M op e) (id_r M op e)
(and_elim_r (semigroup M op) (id M op e) Hmonoid);
def id_rm : id_r M (*) e :=
and_elim_r (id_l M (*) e) (id_r M (*) e)
(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 assoc_g : assoc G op := assoc_m G op 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_rg : id_r G op e := id_rm G op e (and_elim_l (monoid G op 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 left_inverse (a b : G) := inv_l G op e a b;
def right_inverse (a b : G) := inv_r G op 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_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 monoid_g : monoid G (*) e := and_elim_l (monoid G (*) e) has_inverses Hgroup;
def assoc_g : assoc G (*) := assoc_m G (*) e monoid_g;
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 (*) e := id_rm G (*) e (and_elim_l (monoid G (*) 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 (*) 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 (*) 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 (*) 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)))));

4
examples/category.pg
View file

@ -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)

2
examples/classical.pg
View file

@ -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));

12
examples/computation.pg
View file

@ -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
def nat : ★ := forall (A : ★), (A -> A) -> A -> A;
-- `A → A` and repeating it `n` times
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,

64
examples/peano.pg
View file

@ -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))
-> forall (n : nat), P n;
axiom nat_ind : forall (P : nat → ★), P zero → (forall (n : nat), P n → P (suc 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
-- exists a unique function f : nat -> A satisfying
-- For every type A, element z : A, and function fS : nat → A → A, there
-- 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
-- R x y iff for every relation Q : nat -> A -> ★ satisfying
-- 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
-- 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
variable (A : ★) (z : A) (fS : nat -> A -> A);
-- First, fix an A, z : A, and 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 -> ★) :=
forall (n : nat) (y : A), Q n y -> Q (suc n) (fS n y);
def cond2 (Q : nat → A → ★) :=
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),
R x y1 -> R x y2 -> eq B y1 y2;
def fl_in (A B : ★) (R : A → B → ★) (x : A) := forall (y1 y2 : B),
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;

24
lib/Eval.hs
View file

@ -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

12
lib/Parser.hs
View file

@ -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