Three Dollar Quill

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.