## Coding 2023-07-27

Okay.
So.
I *could* keep on with the Crafting Interpreters stuff I was sketching out yesterday.
I *could* do a lot of things.
Like take another tack for encoding Math Stuff.

So I was reading an article on constructive mathematics, and one point it made was that the kinds of limitations that constructivists place on mathematical reasoning can be related to the kinds of limitations that software has to be written under in order to... do anything. One example I'll develop is, it's not obvious to me how you'd establish that a particular property holds for every member of a set. So let's flip it around. Let's reason about what we can do with a contradiction of a property.

Well, if the set is, handwavily speaking, "simple", then, not too much, really.
But if the set is built up from smaller sets in some manner, then it should be possible to *reduce* the contradiction into one that applies to the smaller set.
If not, then there's something wrong with the reduction or the composition, and we can report that still.

Let's see if I can put this together in a way that makes sense to anyone, and hopefully to me.
Let's have an informal class of types called **elements**.
These elements are used to **witness** contradictions to a property.
Something like:

```
type 'a total = Total of 'a * 'a
type 'a commutative = Commutative of 'a * 'a
(* I tried defining a "binary operation" sig, but I just confused myself. *)
module type Magma = sig
type t
val op: t -> t -> t
end
module type Witness = sig
type t
val is_contradiction: t -> bool
end
module TotalWitness(M : Magma) = struct
type t = M.t total
let is_contradiction (Total (a, b)) =
try
M.op a b |> ignore;
false
with _ -> true
end
module CommutativeWitness(M : Magma) = struct
type t = M.t commutative
let is_contradiction (Commutative (a, b)) = M.op a b <> M.op b a
end
```

I doubt that I got all of this exactly right. Like, the specific operation should probably be encoded in the witness type or module... Let's see if defining composition enlightens things any.

```
module MagmaProduct(M1 : Magma) (M2 : Magma) : Magma = struct
type t = M1.t * M2.t
let op (a1, a2) (b1, b2) = (M1.op a1 b1, M2.op a2 b2)
end
```

All right.
There's a slight problem there with the module type specification turning `t` abstract, but, eh.
I'm getting tired, but I'm going to try to articulate the bigger problems here.
The key thing missing is the code to isolate and express the errors.
That needs to build on the code above, or something like it.

At this point, I have some ideas for totally reworking this, but it's too late right now for it to be a good idea to try to write them up.

...

I tried working on it outside of this entry, and just confused myself. Time to get ready for bed.

Good night.