5 | module Data.W

  7 | import Data.Maybe

  9 | %default total

 11 | namespace Finitary

 13 |   data Fin : Type where

 14 |     AVoid : Fin

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

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

 18 |   namespace Fin

 20 |     public export

 21 |     fromString : String -> Fin

 22 |     fromString = AUnit

 24 |   namespace Examples

 26 |     fbb : Fin

 27 |     fbb = "foo" || "bar" || "baz"

 29 |   record NamedUnit (nm : String) where

 30 |     constructor MkNamedUnit

 32 |   Elem : Fin -> Type

 33 |   Elem AVoid = Void

 34 |   Elem (AUnit nm) = NamedUnit nm

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

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

 38 |   lookup AVoid s = Nothing

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

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

 42 |   -- using a record to help the unifier

 43 |   record Shape (d : Fin) where

 44 |     constructor MkShape

 45 |     runShape : Elem d

 47 |   namespace Shape

 49 |     export

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

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

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

 54 |   namespace Examples

 56 |     bar : Shape Examples.fbb

 57 |     bar = "bar"

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

 60 |     constructor MkOne

 61 |     runOne : s

 63 |   Arr : Fin -> Type -> Type

 64 |   Arr AVoid r = ()

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

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

 68 |   export infixr 0 ~>

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

 70 |     constructor MkArr

 71 |     runArr : Arr d r

 73 |   export infix 5 .=

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

 75 |   nm .= v = MkOne v

 77 |   namespace Examples

 79 |     isBar : Examples.fbb ~> Bool

 80 |     isBar = MkArr

 81 |           ( "foo" .= False

 82 |           , "bar" .= True

 83 |           , "baz" .= False

 84 |           )

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

 87 |   lamArr AVoid f = ()

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

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

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

 92 |   lam {d} = MkArr . lamArr d

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

 95 |   appArr AVoid f t = absurd t

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

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

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

100 |   export infixl 0 $$

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

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

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

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

106 |   beta = go d where

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

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

110 |     go AVoid f x = absurd x

111 |     go (AUnit nm) f MkNamedUnit = Refl

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

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

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

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

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

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

120 |     go AVoid () = Refl

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

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

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

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

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

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

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

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

131 |          lamArr d f === lamArr d g

132 |     go AVoid eq = Refl

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

134 |     go (d || e) eq =

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

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

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

139 |   PiArr AVoid b = ()

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

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

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

144 |     constructor MkPi

145 |     runPi : PiArr d (runArr b)

147 |   namespace Dependent

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

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

151 |     lamArr AVoid f = ()

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

153 |     lamArr (d || e) f =

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

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

157 |     export

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

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

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

162 |     public export

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

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

165 |     appArr AVoid f x = absurd x

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

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

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

170 |     export

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

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

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

175 |     export

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

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

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

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

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

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

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

184 |       go AVoid f x = absurd x

185 |       go (AUnit nm) f MkNamedUnit = Refl

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

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

189 |     export

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

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

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

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

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

196 |       go AVoid () = Refl

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

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

200 |     export

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

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

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

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

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

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

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

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

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

211 |       go AVoid eq = Refl

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

213 |       go (d || e) eq =

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

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

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

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

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

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

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

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

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

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

227 |                  pred (MkW s ts)) ->

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

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

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

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

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

234 |     ih AVoid ts = ()

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

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

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

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

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

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

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

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

246 |   namespace Examples

248 |     public export

249 |     NAT : Type

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

251 |         ( "zero" .= AVoid

252 |         , "succ" .= "x"

253 |         )

254 |     zero : NAT

255 |     zero = mkW "zero" ()

257 |     succ : NAT -> NAT

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

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

261 |              pred Examples.zero ->

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

263 |              (n : NAT) -> pred n

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

266 |       where

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

269 |         -- because of a lack of eta

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

272 |         pZero (MkArr ()) ih = pZ

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

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

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

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

279 |     NATindZ = Refl

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

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

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

284 |     NATindS = Refl

286 | namespace PartitionedSets

288 |   record PSet where

289 |     constructor MkPSet

290 |     parts : Fin

291 |     elems : parts ~> Type

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

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

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

297 |   ElemArr AVoid elt = Void

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

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

301 |   Elem : PSet -> Type

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

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

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

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

308 |     go AVoid e x ex = x

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

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

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

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

314 |   Arr AVoid e r = ()

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

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

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

319 |     constructor MkArr

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

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

323 |   PiArr AVoid e r = ()

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

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

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

328 |     constructor MkPi

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

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

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

333 |   lamArr AVoid f b = ()

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

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

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

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

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

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

342 |   appArr AVoid e b x = absurd x

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

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

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

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

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

350 |   namespace Dependent

352 |     public export

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

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

355 |              PiArr d e k

356 |     lamArr AVoid e k b = ()

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

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

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

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

362 |     public export

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

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

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

367 |     public export

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

369 |              PiArr d e k ->

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

371 |     appArr AVoid e k b x = absurd x

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

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

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

376 |     public export

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

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

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

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

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

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

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

386 |         W sh pos

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

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

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

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

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

393 |                  pred (MkW s ts)) ->

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

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

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

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

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

400 |       ih AVoid e ts = ()

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

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

404 |   namespace Examples

406 |     -- proceed with the following assumption

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

409 |       ORD : Type

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

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

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

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

414 |           )

416 |       zero : ORD

417 |       zero = mkW "zero" ()

419 |       succ : ORD -> ORD

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

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

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

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

426 |                pred Examples.zero ->

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

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

429 |                (n : ORD) -> pred n

430 |       ORDind pred pZ pS pL

431 |         = elim pred

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

434 |         where

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

437 |           -- because of a lack of eta

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

440 |           pZero (MkArr ()) ih = pZ

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

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

444 |                   pred (MkW "succ" o)

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

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

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

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

450 |                  pred (MkW "lim" o)

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

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

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

456 |       ORDindZ = Refl

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

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

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

461 |       ORDindS = Refl

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

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

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

466 |       ORDindL = Refl