Inductively-Correct Models of Algebraic Theories

Owen Lynch

Wed May 08 2024

This is a follow-up to Program Safety Via Lexical Constraints.

Suppose I have an theory T (algebraic or otherwise). For instance, suppose that T is the theory of groups. I might write this down in GATlab as

@theory ThGroup begin
  default::TYPE
  unit::default
  (a*b)::default ⊣ [a,b]
  inv(a)::default ⊣ [a]

  #... laws
end

I then might implement this for permutations in the following way.

struct Permutation
  values::Vector{Int}
end

struct PermutationGroup <: Model{Tuple{Permutation}}
  n::Int
end

@instance ThGroup{Permutation} [model::PermutationGroup] begin
  unit() = Permutation(1:model.n)
  (f*g) = Permutation(f.values[g.values])
  inv(f) = Permutation(last.(sorted([zip(f.values, 1:model.n)...])))
end

Now, here’s the question. Is this a correct model of the theory of groups? Clearly, there are values of Permutation where the methods that I defined would in fact throw errors. However, on valid values of Permutation, these methods are in fact correct, and satisfy the group laws!

How should we think about this? One approach would be to make a check in Permutation which would only allow construction of valid permutations. However, running this check all of the time would slow the implementation of unit, *, and inv down, for no measurable gain because we know these are correct. The ideal solution would be to expose some method Vector{Int} -> Permutation that throws an error on an invalid Vector{Int}, and hide the constructor method of Permutation. Then the exposed API to Permutation can be perfectly safe, without any performance penalty. It is for this reason that I think that the fact that Julia doesn’t support private constructors is a big mistake; you can make up for the lack of safety in the type system by having safety in how you expose things!

Anyways, I want to think about this situation mathematically. I want to say that the right way to think about models of theories T is that a model of T is an extension T \to T', and a model M of the signature of T', such that the image of the free model of T' in M is a model of T'.

In other words, the submodel of M consisting of all of the constants that can be written down in T' satisfies the laws in T'.

If we only considered the case T = T', then we wouldn’t be able to do much with models, because there might not be interesting constants in T. Having the theory T' allows us to “inductively present” more terms, but perhaps not all of the terms, of M. For instance, M might be "all Vector{Int}. But if our theory extension T' includes a “partial constructor” Vector{Int} -> Option{default} where default is the single sort in the theory of groups, then we get the ability to do interesting things in M.

This sort of thing seems to be essential for working with models of theories in non-dependently typed languages, because very often we have subtle correctness conditions that can’t be expressed in the type system, and the way to retain correctness in this situation is “by construction”; make sure that the affordances presented to the user cannot produce bad values.

struct Permutation
  values::Vector{Int}

  Permutation(v::Vector{Int}) = isperm(v) ? new(v) : error("$v is not a permutation")
  Permutation(n::Int) = n >= 0 ? new(1:n) : error("$n < 0")
  Permutation(π::Permutation, σ::Permutation) = new(compose_perms(π, σ))
end

compose_perms(π::Permutation, σ::Permutation) = 
        [σ.values[π.values[i]] for i in 1:length(π)]

id(n::Int) = Permutation(n)
(*)(π::Permutation, σ::Permutation) = Permutation(π,σ)