As a C++ user (with a background in categories) patiently waiting for
something a lot better, I personally favour two principles:
1. let's go for undecidable type checking. I want the compiler to be able
to do as much work as possible: ideally, everything that can be resolved at
compile
special
testing.
Regarding the integers =0 as a partial order with a=b when a|b (a divides
b) then gcd a b is the lattice meet of a and b, and 0 is the top element.
Defining gcd 0 x = 0 is consistent with this, for any x.
Michael Abbott
