Skip to content

Commit

Permalink
Fix Hurkens' paradox to type check all the way to M; improve error me…
Browse files Browse the repository at this point in the history
…ssages somewhat.
  • Loading branch information
ionathanch committed Aug 9, 2023
1 parent b64a243 commit d0d3e12
Show file tree
Hide file tree
Showing 4 changed files with 25 additions and 33 deletions.
13 changes: 6 additions & 7 deletions pi/Hurkens.pi
Original file line number Diff line number Diff line change
Expand Up @@ -17,23 +17,22 @@ tau = \t. \x. \f. \p. t (\s. p (f (s x f)))
sigma : U -> P (P U)
sigma = \s. s U tau

Delta : P U
Delta = \y. neg ((p : P U) -> sigma y p -> p (tau (sigma y)))
Delta : Type -> P U
Delta = \b. \y. ((p : P U) -> sigma y p -> p (tau (sigma y))) -> b

Omega : U
Omega = tau (\p. (x : U) -> sigma x p -> p (\y. x y))

M : (x : U) -> sigma x Delta -> Delta x
M = \x. \two. \three. three Delta two (\p. three (\y. p (tau (sigma y))))

-- can't type check
M : (x : U) -> sigma x (Delta Void) -> (Delta Void) x
M = \x. \two. \three. three (Delta Void) two (\p. three (\y. p (tau (sigma y))))

{-
R : (p : P U) -> ((x : U) -> sigma x p -> p x) -> p Omega
R = \zero. \one. one Omega (\x. one (tau (sigma x)))

L : neg ((p : P U) -> ((x : U) -> sigma x p -> p x) -> p Omega)
L = \zero. zero Delta M (\p. zero (\y. p (tau (sigma y))))
L = \zero. zero (Delta Void) M (\p. zero (\y. p (tau (sigma y))))

false : Void
false = L R
-}
40 changes: 16 additions & 24 deletions pi/HurkensEx.pi
Original file line number Diff line number Diff line change
Expand Up @@ -3,23 +3,19 @@ module HurkensEx where

data Void : Type where {}

neg : Type -> Type @ 0
neg = \X. X -> Void

P : Type -> Type @ 0
P = \S. S -> Type

U : Type @ 1
U = (x : Type @ 0) -> (((P^0) ((P^0) x)) -> x) -> (P^0) ((P^0) x)
U = (x : Type @ 0) -> (P^0 (P^0 x) -> x) -> P^0 (P^0 x)

tau : ((P^0) ((P^0) (U^0))) -> (U^0) @ 1
tau : P^0 (P^0 U^0) -> U^0 @ 1
tau = \t. \x. \f. \p. t (\s. p (f (s x f)))

sigma : U -> (P^0) ((P^0) (U^0)) @ 2
sigma = \s. s (U^0) (tau^0)
sigma : U^1 -> P^0 (P^0 U^0) @ 2
sigma = \s. s U^0 tau^0

{-

s : U^1
s : (x:*1) -> (P1 (P1 x) -> x) -> P1 (P1 x)

Expand All @@ -31,28 +27,24 @@ NOTE:
P1 (P1 U0) = P0 (P0 U0)
but *only* after expanding terms
so we should keep track of which definitions are freely displaceable

-}

Delta : Type -> P^0 U^1 @ 2
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))

Delta : (P^0) U^1 @ 2
Delta = \y. neg ((p : (P^0) (U^0) @ 1) -> (sigma^0) y p -> p ((tau^0) ((sigma^0) 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))))

-- warning: parser is not good enough for U^1 @ 2, need to have parens around displaced term

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 -> Delta^1 x @ 4
M = \x. \two. \three. three Delta^0 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))))

{- -- can't type check
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 : neg ((p : (P^0) (U^0)) -> ((x : (U^0)) -> (sigma^0) x p -> p x) -> p (Omega^0))
L = \zero. zero Delta M (\p. zero (\y. p ((tau^0) ((sigma^0) y))))
false : Void
false : Void^0
false = L R
-}
3 changes: 2 additions & 1 deletion src/Equal.hs
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,8 @@ equate' d t1 t2 = do
(_, tyB1, _, tyB2) <- Unbound.unbind2Plus bnd1 bnd2
unless (r1 == r2) $
tyErr n2 n1
cs1 <- equateMaybeLevel l1 l2
cs1 <- Env.extendErr (equateMaybeLevel l1 l2) $
disp [DS "when equating", DD n1, DS "and", DD n2]
cs2 <- equate' Shallow tyA1 tyA2
cs3 <- equate' Shallow tyB1 tyB2
return (cs1 <> cs2 <> cs3)
Expand Down
2 changes: 1 addition & 1 deletion src/TypeCheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -334,7 +334,7 @@ tcTerm PrintMe (Just ty) mk = do
cs <- Env.dumpConstraints
let dcs = displayConstraints (Env.simplify cs)
Env.warn $ [DS "Unmet obligation.\nContext:", DD gamma,
DS "\nGoal:", DD ty,
DS "\nGoal:", DD ty, DS " @ ", DD mk,
DS "\nConstraints:"] ++ dcs
ty' <- tcType ty mk
return (ty', PrintMe)
Expand Down

0 comments on commit d0d3e12

Please sign in to comment.