5 | module Data.W

  7 | import Data.Maybe

  9 | %default total

 11 | namespace Finitary

 13 |   public export

 14 |   data Fin : Type where

 15 |     AVoid : Fin

 16 |     AUnit : (nm : String) -> Fin

 17 |     (||) : (d, e : Fin) -> Fin

 19 |   namespace Fin

 21 |     public export

 22 |     fromString : String -> Fin

 23 |     fromString = AUnit

 25 |   namespace Examples

 27 |     fbb : Fin

 28 |     fbb = "foo" || "bar" || "baz"

 30 |   public export

 31 |   record NamedUnit (nm : String) where

 32 |     constructor MkNamedUnit

 34 |   public export

 35 |   Elem : Fin -> Type

 36 |   Elem AVoid = Void

 37 |   Elem (AUnit nm) = NamedUnit nm

 38 |   Elem (d || e) = Either (Elem d) (Elem e)

 40 |   public export

 41 |   lookup : (d : Fin) -> String -> Maybe (Elem d)

 42 |   lookup AVoid s = Nothing

 43 |   lookup (AUnit nm) s = MkNamedUnit <$ guard (nm == s)

 44 |   lookup (d || e) s = Left <$> lookup d s <|> Right <$> lookup e s

 46 |   -- using a record to help the unifier

 47 |   export

 48 |   record Shape (d : Fin) where

 49 |     constructor MkShape

 50 |     runShape : Elem d

 52 |   namespace Shape

 54 |     public export

 55 |     fromString : {d : Fin} -> (nm : String) ->

 56 |                  IsJust (lookup d nm) => Shape d

 57 |     fromString {d} nm = MkShape (fromJust (lookup d nm))

 59 |   namespace Examples

 61 |     bar : Shape Examples.fbb

 62 |     bar = "bar"

 64 |   public export

 65 |   record One (nm : String) (s : Type) where

 66 |     constructor MkOne

 67 |     runOne : s

 69 |   public export

 70 |   Arr : Fin -> Type -> Type

 71 |   Arr AVoid r = ()

 72 |   Arr (AUnit nm) r = One nm r

 73 |   Arr (d || e) r = (Arr d r, Arr e r)

 75 |   export infixr 0 ~>

 76 |   public export

 77 |   record (~>) (d : Fin) (r : Type) where

 78 |     constructor MkArr

 79 |     runArr : Arr d r

 81 |   export infix 5 .=

 82 |   public export

 83 |   (.=) : (nm : String) -> s -> One nm s

 84 |   nm .= v = MkOne v

 86 |   namespace Examples

 88 |     isBar : Examples.fbb ~> Bool

 89 |     isBar = MkArr

 90 |           ( "foo" .= False

 91 |           , "bar" .= True

 92 |           , "baz" .= False

 93 |           )

 95 |   public export

 96 |   lamArr : (d : Fin) -> (Elem d -> r) -> Arr d r

 97 |   lamArr AVoid f = ()

 98 |   lamArr (AUnit nm) f = MkOne (f MkNamedUnit)

 99 |   lamArr (d || e) f = (lamArr d (f . Left), lamArr e (f . Right))

101 |   lam : {d : Fin} -> (Elem d -> r) -> (d ~> r)

102 |   lam {d} = MkArr . lamArr d

104 |   public export

105 |   appArr : (d : Fin) -> Arr d r -> (Elem d -> r)

106 |   appArr AVoid f t = absurd t

107 |   appArr (AUnit nm) f t = runOne f

108 |   appArr (d || e) f (Left x) = appArr d (fst f) x

109 |   appArr (d || e) f (Right x) = appArr e (snd f) x

111 |   export infixl 0 $$

112 |   public export

113 |   ($$) : {d : Fin} -> (d ~> r) -> (Elem d -> r)

114 |   MkArr f $$ x = appArr d f x

116 |   beta : {d : Fin} -> (f : Elem d -> r) -> (x : Elem d) ->

117 |          (lam {d} f $$ x) === f x

118 |   beta = go d where

120 |     go : (d : Fin) -> (f : Elem d -> r) -> (x : Elem d) ->

121 |          (appArr d (lamArr d f) x) === f x

122 |     go AVoid f x = absurd x

123 |     go (AUnit nm) f MkNamedUnit = Refl

124 |     go (d || e) f (Left x) = go d (f . Left) x

125 |     go (d || e) f (Right x) = go e (f . Right) x

127 |   eta : {d : Fin} -> (f : d ~> r) -> f === lam (\ x => f $$ x)

128 |   eta (MkArr f) = cong MkArr (go d f) where

130 |     go : (d : Fin) -> (f : Arr d r) ->

131 |          f === lamArr d (\ x => appArr {r} d f x)

132 |     go AVoid () = Refl

133 |     go (AUnit nm) (MkOne v) = Refl

134 |     go (d || e) (f, g) = cong2 MkPair (go d f) (go e g)

136 |   ext : {d : Fin} -> (f, g : Elem d -> r) ->

137 |         (eq : (x : Elem d) -> f x === g x) ->

138 |         lam f === lam {d} g

139 |   ext f g eq = cong MkArr (go d eq) where

141 |     go : (d : Fin) -> {f, g : Elem d -> r} ->

142 |          (eq : (x : Elem d) -> f x === g x) ->

143 |          lamArr d f === lamArr d g

144 |     go AVoid eq = Refl

145 |     go (AUnit nm) eq = cong MkOne (eq MkNamedUnit)

146 |     go (d || e) eq =

147 |       cong2 MkPair (go d (\ t => eq (Left t)))

148 |                    (go e (\ t => eq (Right t)))

150 |   public export

151 |   PiArr : (d : Fin) -> (b : Arr d Type) -> Type

152 |   PiArr AVoid b = ()

153 |   PiArr (AUnit nm) b = One nm (runOne b)

154 |   PiArr (d || e) b = (PiArr d (fst b), PiArr e (snd b))

156 |   record Pi (d : Fin) (b : d ~> Type) where

157 |     constructor MkPi

158 |     runPi : PiArr d (runArr b)

160 |   namespace Dependent

162 |     lamArr : (d : Fin) -> {0 b : Arr d Type} ->

163 |              ((x : Elem d) -> appArr d b x) -> PiArr d b

164 |     lamArr AVoid f = ()

165 |     lamArr (AUnit nm) f = MkOne (f MkNamedUnit)

166 |     lamArr (d || e) f =

167 |       ( Dependent.lamArr d (\ x => f (Left x))

168 |       , Dependent.lamArr e (\ x => f (Right x)))

170 |     export

171 |     lam : {d : Fin} -> {0 b : d ~> Type} ->

172 |           ((x : Elem d) -> b $$ x) -> Pi d b

173 |     lam {b = MkArr b} f = MkPi (Dependent.lamArr d f)

175 |     public export

176 |     appArr : (d : Fin) -> {0 b : Arr d Type} ->

177 |              PiArr d b -> ((x : Elem d) -> appArr d b x)

178 |     appArr AVoid f x = absurd x

179 |     appArr (AUnit nm) f x = runOne f

180 |     appArr (d || e) (f, g) (Left x) = Dependent.appArr d f x

181 |     appArr (d || e) (f, g) (Right x) = Dependent.appArr e g x

183 |     export

184 |     ($$) : {d : Fin} -> {0 b : d ~> Type} ->

185 |            Pi d b -> ((x : Elem d) -> b $$ x)

186 |     ($$) {b = MkArr b} (MkPi f) x = Dependent.appArr d f x

188 |     export

189 |     beta : {d : Fin} -> {0 b : d ~> Type} ->

190 |            (f : (x : Elem d) -> b $$ x) ->

191 |            (x : Elem d) -> (lam {b} f $$ x) === f x

192 |     beta {b = MkArr b} f x = go d f x where

194 |       go : (d : Fin) -> {0 b : Arr d Type} ->

195 |            (f : (x : Elem d) -> appArr d b x) ->

196 |            (x : Elem d) -> appArr d {b} (lamArr d {b} f) x === f x

197 |       go AVoid f x = absurd x

198 |       go (AUnit nm) f MkNamedUnit = Refl

199 |       go (d || e) f (Left x) = go d (\ x => f (Left x)) x

200 |       go (d || e) f (Right x) = go e (\ x => f (Right x)) x

202 |     export

203 |     eta : {d : Fin} -> {0 b : d ~> Type} ->

204 |           (f : Pi d b) -> lam {b} (\ x => f $$ x) === f

205 |     eta {b = MkArr b} (MkPi f) = cong MkPi (go d f) where

207 |       go : (d : Fin) -> {0 b : Arr d Type} ->

208 |            (f : PiArr d b) -> (lamArr d {b} $ \ x => appArr d {b} f x) === f

209 |       go AVoid () = Refl

210 |       go (AUnit nm) (MkOne f) = Refl

211 |       go (d || e) (f, g) = cong2 MkPair (go d f) (go e g)

213 |     export

214 |     ext : {d : Fin} -> {0 b : d ~> Type} ->

215 |           (f, g : (x : Elem d) -> b $$ x) ->

216 |           (eq : (x : Elem d) -> f x === g x) ->

217 |           lam {b} f === lam g

218 |     ext {b = MkArr b} f g eq = cong MkPi (go d eq) where

220 |       go : (d : Fin) -> {0 b : Arr d Type} ->

221 |            {f, g : (x : Elem d) -> appArr d b x} ->

222 |            (eq : (x : Elem d) -> f x === g x) ->

223 |            lamArr d {b} f === lamArr d {b} g

224 |       go AVoid eq = Refl

225 |       go (AUnit nm) eq = cong MkOne (eq MkNamedUnit)

226 |       go (d || e) eq =

227 |         cong2 MkPair (go d (\x => eq (Left x)))

228 |                      (go e (\x => eq (Right x)))

230 |   data W : (sh : Type) -> (pos : sh -> Fin) -> Type where

231 |     MkW : (s : sh) -> (pos s ~> W sh pos) -> W sh pos

233 |   mkW : (s : sh) -> Arr (pos s) (W sh pos) -> W sh pos

234 |   mkW s f = MkW s (MkArr f)

236 |   elim : {0 sh : Type} -> {pos : sh -> Fin} ->

237 |          (0 pred : W sh pos -> Type) ->

238 |          (step : (s : sh) -> (ts : pos s ~> W sh pos) ->

239 |                  (Pi (pos s) (lam $ \ p => pred (ts $$ p))) ->

240 |                  pred (MkW s ts)) ->

241 |          (w : W sh pos) -> pred w

242 |   elim pred step (MkW s (MkArr ts))

243 |     = step s (MkArr ts) (MkPi $ ih (pos s) ts) where

245 |     ih : (d : Fin) -> (ts : Arr d (W sh pos)) ->

246 |          PiArr d (lamArr d $ \ p => pred (appArr d ts p))

247 |     ih AVoid ts = ()

248 |     ih (AUnit nm) (MkOne ts) = MkOne (elim pred step ts)

249 |     ih (d || e) (ts, us) = (ih d ts, ih e us)

251 |   public export

252 |   cases : {d : Fin} -> {0 b : Shape d -> Type} ->

253 |           PiArr d (lamArr d (b . MkShape)) -> (x : Shape d) -> b x

254 |   cases f (MkShape x) = go (b . MkShape) f x where

256 |     go : (0 b : Elem d -> Type) ->

257 |          PiArr d (lamArr d b) -> (x : Elem d) -> b x

258 |     go b f x = rewrite sym (Finitary.beta {d} b x) in Dependent.appArr d f x

260 |   namespace Examples

262 |     public export

263 |     NAT : Type

264 |     NAT = W (Shape ("zero" || "succ")) $ cases

265 |         ( "zero" .= AVoid

266 |         , "succ" .= "x"

267 |         )

268 |     zero : NAT

269 |     zero = mkW "zero" ()

271 |     succ : NAT -> NAT

272 |     succ x = mkW "succ" ("x" .= x)

274 |     NATind : (0 pred : NAT -> Type) ->

275 |              pred Examples.zero ->

276 |              ((n : NAT) -> pred n -> pred (succ n)) ->

277 |              (n : NAT) -> pred n

278 |     NATind pred pZ pS = elim pred $ cases ("zero" .= pZero, "succ" .= pSucc)

280 |       where

282 |         -- we're forced to do quite a bit of additional pattern matching

283 |         -- because of a lack of eta

285 |         pZero : (k : AVoid ~> ?) -> ? -> pred (MkW "zero" k)

286 |         pZero (MkArr ()) ih = pZ

288 |         pSucc : (k : "x" ~> ?) -> Pi "x" (lam (\ p => pred (k $$ p))) -> pred (MkW "succ" k)

289 |         pSucc (MkArr (MkOne k)) (MkPi (MkOne ih)) = pS k ih

291 |     NATindZ : {0 pred : NAT -> Type} -> {0 pZ, pS : ?} ->

292 |               NATind pred pZ pS Examples.zero === pZ

293 |     NATindZ = Refl

295 |     NATindS : {0 pred : NAT -> Type} -> {0 pZ : ?} ->

296 |               {pS : (n : NAT) -> pred n -> pred (succ n)} ->

297 |               {0 n : NAT} -> NATind pred pZ pS (succ n) === pS n (NATind pred pZ pS n)

298 |     NATindS = Refl

300 | namespace PartitionedSets

302 |   record PSet where

303 |     constructor MkPSet

304 |     parts : Fin

305 |     elems : parts ~> Type

307 |   public export

308 |   mkPSet : (d : Fin) -> Arr d Type -> PSet

309 |   mkPSet d e = MkPSet d (MkArr e)

311 |   ElemArr : (parts : Fin) -> Arr parts Type -> Type

312 |   ElemArr AVoid elt = Void

313 |   ElemArr (AUnit nm) (MkOne e) = One nm e

314 |   ElemArr (d || e) (f, g) = Either (ElemArr d f) (ElemArr e g)

316 |   Elem : PSet -> Type

317 |   Elem (MkPSet d (MkArr elt)) = ElemArr d elt

319 |   el : {d : Fin} -> {e : d ~> Type} -> (x : Elem d) -> e $$ x -> Elem (MkPSet d e)

320 |   el {e = MkArr e} x ex = go d e x ex where

322 |     go : (d : Fin) -> (e : Arr d Type) -> (x : Elem d) -> appArr d e x -> ElemArr d e

323 |     go AVoid e x ex = x

324 |     go (AUnit nm) (MkOne e) x ex = MkOne ex

325 |     go (d || e) (f, g) (Left x) ex = Left (go d f x ex)

326 |     go (d || e) (f, g) (Right x) ex = Right (go e g x ex)

328 |   Arr : (d : Fin) -> Arr d Type -> Type -> Type

329 |   Arr AVoid e r = ()

330 |   Arr (AUnit nm) (MkOne e) r = One nm (e -> r)

331 |   Arr (d || e) (f , g) r = (Arr d f r, Arr e g r)

333 |   record (~>) (p : PSet) (r : Type) where

334 |     constructor MkArr

335 |     runArr : Arr p.parts p.elems.runArr r

337 |   PiArr : (d : Fin) -> (e : Arr d Type) -> Arr d e Type -> Type

338 |   PiArr AVoid e r = ()

339 |   PiArr (AUnit nm) (MkOne e) (MkOne r) = One nm ((x : e) -> r x)

340 |   PiArr (d || e) (f, g) r = (PiArr d f (fst r), PiArr e g (snd r))

342 |   record Pi (p : PSet) (r : p ~> Type) where

343 |     constructor MkPi

344 |     runPi : PiArr p.parts p.elems.runArr r.runArr

346 |   lamArr : (d : Fin) -> (e : Arr d Type) ->

347 |            (ElemArr d e -> r) -> (Arr d e r)

348 |   lamArr AVoid f b = ()

349 |   lamArr (AUnit nm) (MkOne f) b = MkOne (b . MkOne)

350 |   lamArr (d || e) (f, g) b = (lamArr d f (b . Left), lamArr e g (b . Right))

352 |   lam : {p : PSet} -> (Elem p -> r) -> (p ~> r)

353 |   lam {p = MkPSet d (MkArr e)} f = MkArr (lamArr d e f)

355 |   appArr : (d : Fin) -> (e : Arr d Type) ->

356 |            (Arr d e r) -> (ElemArr d e -> r)

357 |   appArr AVoid e b x = absurd x

358 |   appArr (AUnit nm) (MkOne e) (MkOne b) (MkOne x) = b x

359 |   appArr (d || e) (f, g) (b , c) (Left x) = appArr d f b x

360 |   appArr (d || e) (f, g) (b , c) (Right x) = appArr e g c x

362 |   ($$) : {p : PSet} -> (p ~> r) -> Elem p -> r

363 |   ($$) {p = MkPSet d (MkArr e)} (MkArr b) = appArr d e b

365 |   namespace Dependent

367 |     public export

368 |     lamArr : (d : Fin) -> (e : Arr d Type) -> (k : Arr d e Type) ->

369 |              ((x : ElemArr d e) -> appArr d e k x) ->

370 |              PiArr d e k

371 |     lamArr AVoid e k b = ()

372 |     lamArr (AUnit nm) (MkOne e) (MkOne k) b = MkOne (\ x => b (MkOne x))

373 |     lamArr (d || e) (f, g) (k, l) b

374 |       = ( lamArr d f k (\ x => b (Left x))

375 |         , lamArr e g l (\ x => b (Right x)))

377 |     public export

378 |     lam : {p : PSet} -> {k : p ~> Type} ->

379 |           ((x : Elem p) -> k $$ x) -> Pi p k

380 |     lam {p = MkPSet d (MkArr e)} {k = MkArr k} b = MkPi (lamArr d e k b)

382 |     public export

383 |     appArr : (d : Fin) -> (e : Arr d Type) -> (k : Arr d e Type) ->

384 |              PiArr d e k ->

385 |              ((x : ElemArr d e) -> appArr d e k x)

386 |     appArr AVoid e k b x = absurd x

387 |     appArr (AUnit nm) (MkOne e) (MkOne k) (MkOne b) (MkOne x) = b x

388 |     appArr (d || e) (f, g) (k, l) (b, c) (Left x) = appArr d f k b x

389 |     appArr (d || e) (f, g) (k, l) (b, c) (Right x) = appArr e g l c x

391 |     public export

392 |     ($$) : {p : PSet} -> {k : p ~> Type} ->

393 |            Pi p k -> ((x : Elem p) -> k $$ x)

394 |     ($$) {p = MkPSet d (MkArr e)} {k = MkArr k} (MkPi b) = appArr d e k b

396 |   export

397 |   data W : (sh : Type) -> (pos : sh -> PSet) -> Type where

398 |     MkW : (s : sh) -> (k : pos s ~> W sh pos) -> W sh pos

400 |   mkW : {pos : sh -> PSet} ->

401 |         (s : sh) -> Arr ((pos s).parts) ((pos s) .elems .runArr) (W sh pos) ->

402 |         W sh pos

403 |   mkW s f = MkW s (MkArr f)

405 |   elim : {0 sh : Type} -> {pos : sh -> PSet} ->

406 |          (0 pred : W sh pos -> Type) ->

407 |          (step : (s : sh) -> (ts : pos s ~> W sh pos) ->

408 |                  (Pi (pos s) (lam $ \ p => pred (ts $$ p))) ->

409 |                  pred (MkW s ts)) ->

410 |          (w : W sh pos) -> pred w

411 |   elim pred step (MkW s (MkArr ts)) with (step s) | (pos s)

412 |     _ | steps | MkPSet d (MkArr e) = steps (MkArr ts) (MkPi $ ih d e ts) where

414 |       ih : (d : Fin) -> (e : Arr d Type) -> (ts : Arr d e (W sh pos)) ->

415 |            PiArr d e (lamArr d e $ \ p => pred (appArr d e ts p))

416 |       ih AVoid e ts = ()

417 |       ih (AUnit nm) (MkOne e) (MkOne ts) = MkOne (\ x => elim pred step (ts x))

418 |       ih (d || e) (f, g) (ts, us) = (ih d f ts, ih e g us)

420 |   namespace Examples

422 |     -- proceed with the following assumption

423 |     parameters { auto etaUnit : forall a. (o : () -> a) -> o === (\ _ => o ()) }

425 |       ORD : Type

426 |       ORD = PartitionedSets.W (Shape ("zero" || "succ" || "lim")) $ cases

427 |           ( "zero" .= mkPSet AVoid ()

428 |           , "succ" .= mkPSet "x" ("x" .= ())

429 |           , "lim"  .= mkPSet "f" ("f" .= NAT)

430 |           )

432 |       zero : ORD

433 |       zero = mkW "zero" ()

435 |       succ : ORD -> ORD

436 |       succ o = mkW "succ" ("x" .= \ _ => o)

438 |       lim : (NAT -> ORD) -> ORD

439 |       lim f = mkW "lim" ("f" .= f)

441 |       ORDind : (0 pred : ORD -> Type) ->

442 |                pred Examples.zero ->

443 |                ((n : ORD) -> pred n -> pred (succ n)) ->

444 |                ((f : NAT -> ORD) -> ((n : NAT) -> pred (f n)) -> pred (lim f)) ->

445 |                (n : ORD) -> pred n

446 |       ORDind pred pZ pS pL

447 |         = elim pred

448 |         $ cases ("zero" .= pZero, "succ" .= pSucc, "lim" .= pLim)

450 |         where

452 |           -- we're forced to do quite a bit of additional pattern matching

453 |           -- because of a lack of eta

455 |           pZero : (o : mkPSet AVoid () ~> ORD) -> ? -> pred (MkW "zero" o)

456 |           pZero (MkArr ()) ih = pZ

458 |           pSucc : (o : mkPSet (AUnit "x") ("x" .= ()) ~> ORD) ->

459 |                   Pi (mkPSet (AUnit "x") ("x" .= ())) (lam (\p => pred (o $$ p))) ->

460 |                   pred (MkW "succ" o)

461 |           pSucc (MkArr (MkOne o)) (MkPi (MkOne po)) =

462 |             rewrite etaUnit o in pS (o ()) (po ())

464 |           pLim : (o : mkPSet (AUnit "f") ("f" .= ?A) ~> ORD) ->

465 |                  Pi (mkPSet (AUnit "f") ("f" .= ?B)) (lam (\p => pred (o $$ p))) ->

466 |                  pred (MkW "lim" o)

467 |           pLim (MkArr (MkOne o)) (MkPi (MkOne po)) = pL o po

470 |       ORDindZ : {0 pred : ORD -> Type} -> {0 pZ, pS, pL : ?} ->

471 |                 ORDind pred pZ pS pL Examples.zero === pZ

472 |       ORDindZ = Refl

474 |       ORDindS : {0 pred : ORD -> Type} -> {0 pZ, pL : ?} ->

475 |                 {pS : (n : ORD) -> pred n -> pred (succ n)} ->

476 |                 {0 n : ORD} -> ORDind pred pZ pS pL (succ n) === pS n (ORDind pred pZ pS pL n)

477 |       ORDindS = Refl

479 |       ORDindL : {0 pred : ORD -> Type} -> {0 pZ, pS : ?} ->

480 |                 {pL : (f : NAT -> ORD) -> ((n : NAT) -> pred (f n)) -> pred (lim f)} ->

481 |                 {0 f : NAT -> ORD} -> ORDind pred pZ pS pL (lim f) === pL f (\ n => ORDind pred pZ pS pL (f n))

482 |       ORDindL = Refl