Wombat and Mathematics

I was disappointed at the somewhat downbeat tone of Mike Shulman in https://golem.ph.utexas.edu/category/2015/06/whats_so_hott_about_formalizat.html#c049290. I had thought HoTT/UF was going to solve all our problems.

Trying to follow along with some of these discussions I see things that seem similar to issues that I try to address in the design of the Wombat programming language.

In the discussion of the merit of type theory versus set theory we see a comment suggesting that in the set theory world we have to worry about whether 1∈2. That’s because the natural numbers are modelled in set theory as: 0 by ∅ (empty set); 1 by {∅} (the set with only the empty set as a member), 2 by {∅,{∅}}, and so on. Yes the natural numbers and their properties can be modelled in set theory this way, but the properties of natural numbers are different from the properties of these sets. This is similar to the way Wombat types are built up in steps from primitive types. A type and its properties are implemented using some other type and that type’s properties, but there is no automatic carryover of properties. This is in contrast to the longstanding tradition in programming languages of identifying types with their implementations. It seems from the comment that mathematics has the same problem.

Another current issue in Mathematics is the meaning of equality. A comprehensive discussion with links is given in http://ncatlab.org/nlab/show/principle+of+equivalence, but also look at John Baez’s first cut of that page http://ncatlab.org/nlab/revision/principle+of+equivalence/1. Wombat allows each type to have its own idea of equality (not necessarily with excluded middle). The problem, very similar to the mathematical one, is to ensure that if x=y then f(x)=f(y) for any function f. For example one of the permitted implementations of rational numbers is as two integers in unreduced form. We need to ensure that functions don’t peek at the representation and return a different result for 6/4 compared to 3/2. In Wombat a Type has properties and axioms. For each implementation of that type the properties are implemented in terms of the underlying type, and the axioms are proved using the axioms of the underlying type. Also when there are multiple implementations, then the later implementations have to proveably give equivalent results to the initial (reference) implementation. Other functions can only access a value through the properties of its Type, and this prevents them from doing the evil thing and peeking at the implementation.

A related question is whether two things can be equal if they are not the same type. Wombat handles this by having a hierarchy (order lattice) of Types. Every value belongs to a hierarchy of types, and values can be compared anywhere in the intersection of the two hierarchies. If the intersection includes the Empty type then they aren’t equal, though this isn’t the way the issue would normally be decided.