Add builtin Void + absurd bc it was annoying me

README.md

@@ -26,27 +26,30 @@ M ::= <name>           (* module names *)
 i, j, k ::= <natural>  (* levels *)
 
 (* terms *)
-a, b, A, B ::= x                   (*           variable or constant with implicit displacement *)
-             | x ^ i               (* [xⁱ]      constant with explicit displacement *)
-             | Type                (* [⋆]       type universe *)
-             | \x. b               (* [λx. b]   function *)
-             | b a                 (*           application *)
-             | (x : A @ k) -> B    (* [Πx:ᵏA.B] dependent function type with explicit domain level *)
-             | (x : A) -> B        (*                               and with implicit domain level *)
-             | A -> B              (* [A → B]   nondependent function type *)
+a, b, A, B ::= x                   (*             variable or constant with implicit displacement *)
+             | x ^ i               (* [xⁱ]        constant with explicit displacement *)
+             | Type                (* [⋆]         type universe *)
+             | \x. b               (* [λx. b]     function *)
+             | b a                 (*             application *)
+             | (x : A @ k) -> B    (* [Πx:ᵏA.B]   dependent function type with explicit domain level *)
+             | (x : A) -> B        (*                                 and with implicit domain level *)
+             | A -> B              (* [A → B]     nondependent function type *)
+             | Void                (* [⊥]         empty type *)
+             | absurd b            (* [absurd(b)] ex falso quodlibet *)
 (* the following are features not found in StraTT *)
-             | a = b               (*           equality type *)
-             | subst a by b        (*           substitute in the type of a the equality b *)
-             | Refl                (*           reflexivity proof *)
-             | (a : A)             (*           explicit type annotation *)
-             | let x = a in b      (*           let-bound expressions *)
-             | TRUSTME             (*           typed hole *)
-             | PRINTME             (*           typed hole printing context, constraints, and goal *)
+             | a = b               (*             equality type *)
+             | Refl                (*             reflexivity proof *)
+             | subst a by b        (*             substitute in the type of a the equality b *)
+             | contra b            (*             eliminate propositional equality of definitionally inequal terms *)
+             | (a : A)             (*             explicit type annotation *)
+             | let x = a in b      (*             let-bound expressions *)
+             | TRUSTME             (*             typed hole *)
+             | PRINTME             (*             typed hole printing context, constraints, and goal *)
 (* the following are relevant to datatypes *)
-             | D a...              (*           fully applied datatype *)
-             | C a...              (*           fully applied constructor *)
-             | case a of
-                 (C x... => b)...  (*           case expression *)
+             | D a...              (*             fully applied datatype *)
+             | C a...              (*             fully applied constructor *)
+             | case a of           (*             case expression *)
+                 (C x... => b)...
 
 (* signatures *)
 Δ ::= x : A      (* [x : A ≔ a] global definition *)

pi/Equal.pi

@@ -1,4 +1,4 @@
-module Equality where
+module Equal where
 
 -- Defining propositional equality as an indexed datatype
 

pi/Hurkens.pi

@@ -1,7 +1,5 @@
 module Hurkens where
 
-data Void : Type where {}
-
 neg : Type -> Type
 neg = \X. X -> Void
 

pi/HurkensAnnot.pi

@@ -1,7 +1,5 @@
 module HurkensAnnot where
 
-data Void : Type where {}
-
 P : Type -> Type @ 0
 P = \S. S -> Type
 
@@ -31,16 +29,16 @@ Delta = \b. \y. ((p : P^0 U^0 @ 1) -> sigma^0 y p -> p (tau^0 (sigma^0 y))) -> b
 Omega : U^0 @ 3
 Omega = tau^0 (\p. (x : U^1 @ 2) -> sigma^0 x p -> p (\y. x y))
 
-M : (x : U^2 @ 3) -> sigma^1 x (Delta^0 Void^0) -> Delta^1 Void^0 x @ 4
-M = \x. \two. \three. three (Delta^0 Void^0) two (\p. three (\y. p (tau^0 (sigma^0 y))))
+M : (x : U^2 @ 3) -> sigma^1 x (Delta^0 Void) -> Delta^1 Void x @ 4
+M = \x. \two. \three. three (Delta^0 Void) two (\p. three (\y. p (tau^0 (sigma^0 y))))
 
 {-
 R : (p : P^0 U^0) -> ((x : U^0) -> sigma^0 x p -> p x) -> p Omega^0
 R = \zero. \one. one Omega^0 (\x. one (tau^0 (sigma^0 x)))
 
-L : ((p : P^0 U^0) -> ((x : U^0) -> sigma^0 x p -> p x) -> p Omega^0) -> Void^0
-L = \zero. zero (Delta^0 Void^0) M (\p. zero (\y. p (tau^0 (sigma^0 y))))
+L : ((p : P^0 U^0) -> ((x : U^0) -> sigma^0 x p -> p x) -> p Omega^0) -> Void
+L = \zero. zero (Delta^0 Void) M (\p. zero (\y. p (tau^0 (sigma^0 y))))
 
-false : Void^0
+false : Void
 false = L R
 -}

pi/Logic.pi

@@ -80,15 +80,6 @@ or_assoc = \[A] [B] [C] abc.
       Inl b -> Inl (Inr b)
       Inr c -> Inr c
 
--- Falsehood
-------------
-
-data Void : Type where {} -- no constructors
-
--- aka ex_falso_quolibet
-false_elim : [P : Type] -> Void -> P
-false_elim = \[P] v. case v of {}
-
 -- Negation
 -----------
 
@@ -101,7 +92,7 @@ not_false = \x. x
 contradiction_implies_anything : [P : Type] -> [Q : Type] -> And P (neg P) -> Q
 contradiction_implies_anything = \[P] [Q] and.
   case and of
-    Conj p notp -> false_elim [Q] (notp p)
+    Conj p notp -> absurd (notp p)
 
 double_neg : [P : Type] -> P -> neg (neg P)
 double_neg = \[P] p. \x. x p
@@ -115,7 +106,7 @@ not_both_true_and_false = \[P] [Q] andpnp.
     Conj p np -> np p
 
 iff_neg_false : [A : Type] -> iff (neg A) (iff A Void)
-iff_neg_false = \[A]. Conj (\x. Conj x (\y. false_elim [A] y)) (proj1 [A -> Void] [Void -> A])
+iff_neg_false = \[A]. Conj (\x. Conj x (\y. absurd y : Void -> A)) (proj1 [A -> Void] [Void -> A])
 
 em_irrefutable : [A : Type] -> neg (neg (Either A (neg A)))
 em_irrefutable = \[A] f. f (Inr (\a. f (Inl a)))

pi/Ord.pi

@@ -1,7 +1,5 @@
 module Ord where
 
-data Void : Type where {}
-
 -- Ordinals and their order
 
 data Ord : Type where
@@ -17,12 +15,12 @@ lt : Ord -> Ord -> Type
 lt = \o1 o2. Leq (Succ o1) o2
 
 zero : Ord
-zero = Lim [Void] (\v. case v of {})
+zero = Lim [Void] (\b. absurd b : Void -> Ord)
 
 -- Properties of the order
 
 zeroLeq : [o : Ord] -> Leq zero o
-zeroLeq = \[o]. Limiting [Void] (\v. case v of {}) (\v. case v of {})
+zeroLeq = \[o]. Limiting [Void] (\b. absurd b : Void -> Ord) (\b. absurd b : (v : Void) -> Leq (absurd v) o)
 
 reflLeq : (o : Ord) -> Leq o o
 reflLeq = \o. case o of

pi/README.pi

@@ -1,6 +1,6 @@
 module README where
 
--- Conjuction, disjuction, falsehood, negation
+-- Conjuction, disjuction, negation
 import Logic
 
 -- Properties of _=_ (builtin equality type)

pi/Russell.pi

@@ -2,8 +2,6 @@
 
 module Russell where
 
-data Void : Type @ 0 where {}
-
 data Pair (A : Type @ 0) (B : A -> Type) : Type @ 1 where
   pair of (x : A @ 0) (B x) @ 1
 

pi/WFU.pi

@@ -1,7 +1,5 @@
 module WFU where
 
-data Void : Type @ 0 where {}
-
 data U : Type where
   Mk_U of (X : Type) (X -> U)
 

pi/WFUAnnot.pi

@@ -1,7 +1,5 @@
 module WFUAnnot where
 
-data Void : Type @ 0 where {}
-
 data U : Type @ 1 where
   Mk_U of (X : Type @ 0) (X -> U) @ 1
 
@@ -23,10 +21,10 @@ loop : U^1 @ 2
 loop = Mk_U^1 U^0 liftU^0
 
 {-
-not_WF : WF^1 loop^0 -> Void^0 @ 3
+not_WF : WF^1 loop^0 -> Void @ 3
 not_WF = \y. case y of
   Mk_WF [X] [f] x -> not_WF (x loop^0)
 
-false : Void^0
+false : Void
 false = not_WF^0 (always_WF^0 loop^0)
 -}

src/Equal.hs

@@ -99,6 +99,8 @@ equate' d t1 t2 = do
     (TrustMe, TrustMe) ->  return success
     (PrintMe, PrintMe) ->  return success
 
+    (Void, Void) -> return success
+
     (TyUnit, TyUnit)   -> return success
     (LitUnit, LitUnit) -> return success
 
@@ -180,6 +182,9 @@ equate' d t1 t2 = do
             (Contra a1, Contra a2) ->
               equate' Shallow a1 a2
 
+            (Absurd b1, Absurd b2) ->
+              equate' Shallow b1 b2
+
             (Case s1 brs1, Case s2 brs2) ->
               if length brs1 == length brs2 then do
                   cs1 <- equate' Shallow s1 s2
@@ -487,6 +492,8 @@ displace j t = case t of
     Type -> return Type
     PrintMe -> return PrintMe
     TrustMe -> return TrustMe
+    Void -> return Void
+    Absurd b -> Absurd <$> displace j b
     TyUnit -> return TyUnit
     LitUnit -> return LitUnit
     (LitBool b) -> return (LitBool b)

src/Parser.hs

@@ -50,6 +50,9 @@ Optional components in this BNF are marked with < >
 
     | let x = a in b           Let expression
 
+    | Void                     Empty type
+    | absurd b                 ex falso quodlibet
+
     | Unit                     Unit type
     | ()                       Unit value
 
@@ -185,6 +188,7 @@ piforallStyle = Token.LanguageDef
                   ,"ord"
                   ,"Bool", "True", "False"
                   ,"if","then","else"
+                  ,"Void", "absurd"
                   ,"Unit", "()"
                   ]
                , Token.reservedOpNames =
@@ -477,7 +481,6 @@ funapp = do
 
 factor = choice [ try displaceTm <?> "displaced term"
                 , varOrCon   <?> "a variable or nullary data constructor"
-
                 , typen      <?> "Type"
                 , lambda     <?> "a lambda"
                 , try letPairExp  <?> "a let pair"
@@ -487,13 +490,13 @@ factor = choice [ try displaceTm <?> "displaced term"
                 , substExpr  <?> "a subst"
                 , refl       <?> "Refl"
                 , contra     <?> "a contra"
+                , absurd     <?> "ex falso quodlibet"
                 , trustme    <?> "TRUSTME"
                 , printme    <?> "PRINTME"
                 , impProd    <?> "an implicit function type"
                 , bconst     <?> "a constant"
                 , ifExpr     <?> "an if expression"
                 , sigmaTy    <?> "a sigma type"
-
                 , expProdOrAnnotOrParens
                     <?> "an explicit function type or annotated expression"
                 ]
@@ -525,6 +528,7 @@ bconst  :: LParser Term
 bconst = choice [reserved "Bool"  >> displace >>= \j -> return (TCon boolName j []),
                  reserved "False" >> displace >>= \j -> return (DCon falseName j []),
                  reserved "True"  >> displace >>= \j -> return (DCon trueName j []),
+                 reserved "Void"  >> displace >>= \j -> return Void,
                  reserved "Unit"  >> displace >>= \j -> return (TCon tyUnitName j []),
                  reserved "()"    >> displace >>= \j -> return (DCon litUnitName j [])]
 
@@ -698,6 +702,11 @@ contra = do
   witness <- expr
   return $ Contra witness
 
+absurd :: LParser Term
+absurd = do
+  reserved "absurd"
+  witness <- expr
+  return $ Absurd witness
 
 sigmaTy :: LParser Term
 sigmaTy = do

src/PrettyPrint.hs

@@ -390,6 +390,11 @@ instance Display Term where
     return $ PP.text "TRUSTME"
   display PrintMe = do
     return $ PP.text "PRINTME"
+  display Void = return $ PP.text "Void"
+  display (Absurd b) = do
+    p <- ask prec
+    db <- display b
+    return $ parens (levelPi < p) $ PP.text "absurd" <+> db
   display TyUnit = return $ PP.text "Unit"
   display LitUnit = return $ PP.text "()"
   display TyBool = return $ PP.text "Bool"

src/Syntax.hs

@@ -73,6 +73,10 @@ data Term
   | -- | let expression, introduces a new (non-recursive) definition in the ctx
     -- | `let x = a in b`
     Let Term (Unbound.Bind TName Term)
+  | -- | the empty type
+    Void
+  | -- | ex falso quodlibet
+    Absurd Term
   | -- | the type with a single inhabitant, called `Unit`
     TyUnit
   | -- | the inhabitant of `Unit`, written `()`
@@ -511,6 +515,8 @@ isFreelyDisplaceable = go where
   go TrustMe = True
   go PrintMe = True
   go (Let te bnd) = go te && let (_,a) = Unbound.unsafeUnbind bnd in go a
+  go Void = True
+  go (Absurd b) = go b
   go TyUnit = True
   go LitUnit = True
   go TyBool = True

src/TypeCheck.hs

@@ -143,6 +143,13 @@ tcTerm TrustMe (Just ty) mk = do
   ty' <- tcType ty mk
   return (ty', TrustMe)
 
+-- i-void
+tcTerm Void Nothing k = return (Type, Void)
+tcTerm (Absurd b) (Just ty) k = do
+  ty' <- tcType ty k
+  b' <- checkType b Void k
+  return (ty', Absurd b')
+
 -- i-unit
 tcTerm TyUnit Nothing k = return (Type, TyUnit)
 tcTerm LitUnit Nothing k = return (Type, LitUnit)