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.