Inductively-Correct Models of Algebraic Theories

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.

4 Likes

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!

This has been a persistent frustration for me. It’s important to be able to distinguish the case of constructing an instance of a type from external data that could be nonsense from the case where you know that, by construction, the input data is valid because it is downstream of other data known to be valid.

4 Likes

Aren’t inner constructors enough to enforce these?

https://docs.julialang.org/en/v1/manual/constructors/#man-inner-constructor-methods

For example, you could have

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(π,σ)

It has two downsides:

  1. You lose the openness to new methods that Julia’s multiple dispatch creates
  2. You have to put a lot of logic in the definition of the struct.
  3. You only get one function per type signature.

But those seem like reasonable sacrifices for the kind of guarantee that you want for types being properly instantiated. And you can avoid the last one with ::typeof(f) where f is a function.

Like if you wanted to add a special constructor for the reversed permuation on n things you could add an inner constructor like

Permutation(::typeof(reverse), n::Int) = new(reverse(1:n))

Or if you had a different binary operator on permutations like \pi^{-1}\sigma \pi.

Permutation(::typeof(conj), ::π::Permutation, σ::Permutation) = new(compose_perms(compose_perms(inv(π), σ), π)))

2 Likes

Whoa, that’s actually a pretty clever solution with the typeof. I hadn’t thought of that before.

For CAP we opted for the following strategy:

  1. The core function assumes correct input, otherwise “garbage in, garbage out”.
  2. In user mode a so-called pre-function does a quick, usually inexpensive but incomplete type-checking of the input and a post-function does the same for the output.
  3. The complete validity of input/output objects/morphisms can be checked using a separate function called IsWellDefined, which must be explicitly invoked.
  4. When we compile a categorical tower only the core functions are used and the pre-functions are ignored.
  5. A categorical tower is able to install an IsWellDefined for objects and morphisms once every layer in the tower knows how to install it.
3 Likes

I like this; I think as we move forward in AlgebraicJulia we would do well to adopt a systematic approach like this.

1 Like