the kind of programming
Apr. 7th, 2019 10:25 pmReminds me what we did in Forth, with Leo, present here:
This is a test case. Rather, 25 test cases.
We scan through
and then, in each row, apply this representable to objects
But toposes are not essential here. I just decided to be lazy, and write code as tables, as Leo suggested eons ago, probably in 1989. It's not even my idea.
Implementation:
applyTo | "a" | "b" | "c" | "d" | "e" | at("a") | "a" | "ab" | "" | "" | "" | at("b") | "" | "b" | "" | "" | "" | at("c") | "" | "cb" | "c" | "cd" | "" | at("d") | "" | "" | "" | "d" | "" | at("e") | "" | "" | "" | "ed" | "e"
This is a test case. Rather, 25 test cases.
We scan through
at("a")
to at("e")
, where at(x)
is a representable diagram (presheaf, functor, whatever) for object x
:val at = (obj: topos.site.Obj) => topos.representable(obj)
and then, in each row, apply this representable to objects
"a",..., "e"
, and check that the result is a set (hom(x, y)
) consisting of the values in the cells of the table. The values in the table are split by comma and converted to sets - because we deal with Grothendieck toposes.But toposes are not essential here. I just decided to be lazy, and write code as tables, as Leo suggested eons ago, probably in 1989. It's not even my idea.
Implementation:
val at = (obj: topos.site.Obj) => topos.representable(obj) case class table(data: List[String] = Nil) { def |(x: String): table = table(x::data) def |(d: Diagrams.Diagram) = check(d, data, data) } case class check(d: Diagram, data: List[String], fullList: List[String]) { def |(x: String): check = { d(data.head) === x.split(",").toSet check(d, data.tail, fullList) } def |(d: Diagram): check = check(d, fullList, fullList) } val applyTo = new table