As an aside, I’d be curious to know if anyone has suggestions for related work around this area of “customizable equality”. In particular, I’m not aware of logic languages that have to prove goals to prove equality
Indeed, as @tupshin mentioned, this topic is covered by Homotopy Type Theory where type equality is the real cornerstone. I am strongly advising you to have a look.
By the way, the book is freely distributed on the official site: https://homotopytypetheory.org/
I think that the encouragements to look at Homotopy Type Theory (HoTT) are well-meaning but rather off-topic. What you are looking for for associated types is type-level computation, in a form that has been formalized in various ways in programming language theory (for example ML module system’s research uses singleton types to compute with type definitions) and is essentially unrelated to the higher-dimensional nature of HoTT. Equality in general is a deep problem in type theory, and HoTT has a lot of exposure right now, so it is natural for people to think of a relation, but I don’t think there is any here. (In technical terms, F-omega already has a type-equality relation in its type system that does type-level computation, while it doesn’t have any notion of propositional equality.)
On the other hand, my comment on reading the blog post was that there was a bit too much Prolog and a bit too little type theory, in the following sense: you are not only solving a proof search problem, you are building a program fragment that has computational meaning – the execution behavior of your program depends on the fragment fragment that is inferred during trait elaboration
By elaboration, I am referring to the idea of transforming the source code that people write into a more explicit form in which the calls to trait-bound functions are replaced/enriched/annotated with the path of the specific implementation of the function that is actually going to run, and calls to methods with trait assumptions on their generic parameters are enriched/annotated with an extra argument carrying the specific implementation of the trait for the call’s instance. (This does not mean that trait dispatch has to be implemented this way in practice; you can always explain the specialization as inlining and specialization of these extra explicit arguments.) In particular, while the code before the elaboration does not satisfy the type erasability property (if you erase all information about types, you cannot execute the program anymore), the explicited program after elaboration has a type-erased semantics that is faithful to the language semantics. Understanding this transformation pass is important because (1) having an intermediate form that permits type erasure is an interesting property of your language (it tells you the minimum information a programmer needs to understand to accurately predict program execution) and (2) this intermediate form is a good way to think about human-program interactions in an IDE: it is precisely what you want to show (under some nice syntax) when a programmer wonders “what is going to happen with this trait-bound call here?”, and understanding the syntax of this elaborated forms also helps you write better error messages when elaboration fails (because there is an ambiguity, for example).
If you are lucky, you can design this elaboration in such a way that the post-elaboration program are expressed in exactly the same syntax as the pre-elaboration program that users wrote. This property trivially holds of Scala’s implicit parameters (an implicit parameter is just a value/term that the user could have written themselves), but it is a bit less obvious of Haskell’s type classes or Rust’s traits. Using the Haskell syntax that I am more familiar with, you could elaborate something like:
class Eq a where
eq :: a -> a -> Bool
instance EqInt where
eq n1 n2 = ...
instance Eq a => Eq (List a) where
eq [] [] = True
eq (x:xs) (y:ys) = eq x y && eq xs ys
eq _ _ = False
discr :: Eq a => a -> a -> Int
discr x y = if eq x y then 1 else 0
assert (discr [1] [2] == 0)
into the more explicit transformed program
type eq a = (a -> a -> bool)
eqInt :: eq Int = ...
eqList :: eq a -> eq (List a)
eqList eqA [] [] = True
eqList eqA (x:xs) (y:ys) = eqA x xs && eqList eqA xs ys
eqList eqA _ _ = False
discr :: eq a -> a -> a -> Int
discr eqA x y = if eqA x y then 1 else 0
assert (discr (eqList eqInt) [1] [2] == 0)
Notice that:
Eq a becomes the type eq a of comparison functionsInt is in the class Eq) is turned into a value of that type, eq Int
a is in the class Eq, so are lists of a) becomes a function from values of type eq a to values of type eq (List a)
discr [1] [2] in the source version has a behavior that depends on “which definition of the equality will be chosen”. In the explicit version, we can easily describe which definition has been chosen by a source term: (eqList eqInt). I could show this to the user; if there was a conflict with two possible definitions, I could show both sides to explain the conflict.The prolog rules presented in the blog post explain whether there exists a solution to this elaboration problem, but not what the solution is. There are two ways to describe the relation between these two questions:
eq (List Int) in my example), and that the reason this looks like Prolog is the Curry-Howard isomorphism (the type system of your elaboration terms also describes a logic).Of course, none of these two views is intrisically better than the other: they are both perfectly correct, and it is interesting to keep both perspectives in mind. Which one matters depends on the specific problem you are asking about the system you are studying. (I think this is important to point out because the original blog post is not balanced in this respect, it only presents the logic-programming view of the problem.)
Here are some reasons why I think also working out the type-theroetic views (that elaboration witnesses are terms that we are doing a search for) is important:
Eq Int compared to Ord Int => Eq Int in Haskell (the witness of the latter resolution path is equivalent, as a term, to the witness of the former resolution path). Equalities between types matter as part of the type-directed search for witnesses. The blog post explains that trait queries are lowered to propositions in some unspecified logic whose propositions are given a somewhat Rust-like syntax; but what really happens is that the goals of elaboration precisely use Rust types, and the equalities are the equality relations in the Rust type system.If you see trait search as elaboration into an existing logic, you will be able to apply existing proof search techniques exactly unchanged, but every desirable property of your design will have to be checked through the encoding from types to logic propositions, and from logic proof terms to programs or elaboration witnesses. If you see trait search as term search in your existing type system, you will have to re-interpret existing proof search methods inside a slightly different setting, but the terms and the types manipulated will be those that users know and think about. You need to combine both views to productively think about the problem.
Heh, I’m glad you think so, because to be honest I know absolutely nothing about homotopy type theory and I don’t relish reading into another big area of work. 
Yes, so – to start, I agree with everything you wrote, for the most part. =) I started out taking the “logic-centric” view that you described, where the proof tree defines the program semantics. But I’ve since shifted gears into a different approach.
The key is that, in Rust, every (monomorphized) function definition has a unique type. This is true of closures (of course), but also of function items. These types are zero-sized, but they can be “reified” into a function pointer. You can see that in the following program:
use std::mem;
fn foo() { }
fn main() {
let f = foo;
println!("{}", mem::size_of_val(&f)); // prints 0
}
The only time that it trait resolution affects program semantics is basically when it decides what code will execute. For example, when I call x.clone(), we will take the (monomorphized) type of x (let’s call it X) and then find the appropriate version of clone for X. In my view, this is just associated type normalization.
In other words, you can view the impl of Clone as supplying a (special) associated type clone which is guaranteed to point to one of these unique function types after normalization (this could be modeled as a normal associated type with a further bound, if you cared to do so). My point is that “resolving” x.clone() to a specific bit of code, in this view, is basically equivalent to normalizing the associated type <X as Clone>::clone (where X is the type of x).
So let’s say there is a normalization predicate: <X as Clone>::clone ==> T (as, indeed, there is). In this case, it doesn’t matter what the proof tree is; if I can prove the normalization judgement, and because I know that T will be some unique function type, I have figure out what code to call – I just have to reify T into a function pointer. Of course all of this relies on coherence to ensure that, indeed, every normalization has a specific and unique outcome.
(For trait objects, the way I view is that there is an (implicit) impl of Trait for the type Trait. That implementation is fixed to extract a pointer out of a vtable and call it.)
What this means for the proof search is that we don’t mind if there are multiple proof trees, so long as they all prove the same judgement (i.e., they all normalize <X as Clone>::clone to the same type T). But we have to be very careful for those cases where we infer some parts of the judgement from others. As an example, if you have only impl Foo for i32, and you ask us to prove ?T: Foo, we will infer that (a) it is true and (b) ?T = i32 must hold. It would be bad if we did that even in the case where there existed more impls, since then we’d be arbitrarily deciding on a semantics for you. But in any case this process of inferring bits of the judgement is exactly the elaboration you were talking about, I believe.
Does that make sense to you?
So Rust’s traits have always felt less type-theoretic to me too. I think a big reason is that in Haskell dictionaries often do get passed around so the proof tree does matter computationally even if coherence guarantees that the evaluated value is unique. Now, I’d like to really be able to explicitly work with vtables and existential types in Rust someday, but until then, yes, the approaches here will work.
BTW, the conversation for https://github.com/ghc-proposals/ghc-proposals/pull/32 is very interesting and somewhat tangentially relevant, and I do recommend it.
@nikomatsakis [hope this isn’t veering off-topic too much.] The function types approach does work, but IMO ultimate doesn’t feel completely satisfactory because working with singleton-type proxies alone is quite indirect. Thinking back to https://github.com/rust-lang/rfcs/issues/1037 what if every function singleton type inhabited a trait like
trait Fn<'a, Params, Ret> where Self::Size = 0 {
const ptr: &'a TrueFn<Params, Ret>;
}
Where 'a would always be 'static today, and TrueFn is a custom Meta = () unsized type. One thing I like about this is it puts tupled parameter types “at the root”, which I think is good for any future variadics work.
Not sure what to do for unsafety and ABI, but heavy solutions do exist (e.g. Haskell’s data promotion for an ABI enum).
So Rust’s traits have always felt less type-theoretic to me too
Actually, logic programming can be very type-theoretic. Twelf is a great example, in this language propositions are literally types and programming is specifying types.
See Introduction to Twelf and the Twelf wiki for more details.
After further reflection (and a lot of experimentation) on Rust’s trait system I believe its logic ends up being very similar to that made possible by Scala’s Path Dependent Types, and that there are enough similarities that it would be worth reviewing http://lampwww.epfl.ch/~amin/dot/fpdt.pdf as some very relevant prior art.
On the applicative/projective bikeshed: “applicative projections” are quite an odd animal, because they aren’t necessarily distinct to other applicative projections. IIRC the term for non-projection applicatives is “nominal types”.
In Haskell, I think they are called generative type functions.
Definition (Generativity). If
fandgare generative, thenf a ∼ g bimpliesf ∼ g.
Source: R. Eisenberg, Dependent types in Haskell: theory and practice, §4.2.4, p. 58
Dead link
Indeed. Unification gives a negative answer – but just because A = B cannot be proven does not mean that A != B can be proven. (Relevant code in chalk here.) The same is true of skolemized type parameters.
In terms of the “simplified grammar”, at least, it may be worth making a category for “normalized projection” and skolemized type parameters that is distinct from other nominal types. I was debating about presenting it that way, but I couldn’t think of a good reason to distinguish them.
Huh, yeah, in retrospect that seems like the obvious term to use. =) Not sure why I didn’t adopt that, I think because my head was in the “classifications of functions” space (e.g., injective etc) and I wasn’t really thinking about terms for types.
Yeah, so I was using the term “generative” at one point – in specific, in the congruence closure code I was writing – but it didn’t seem quite right to me here. I think because I had in mind applicative vs generative functors. If you then view Vec as a module, it acts more like an applicative functor (that is, Vec<T> = Vec<U> if T = U). Anyway, generative seems like also an ok term, but I think @arielb1 is right that the best term is nominal type, which has no other use.
So having thought about it, I think that probably the best way to think about things is that there are four categories of types:
Vec)T within a generic function, or T::Item when we can’t normalize in any other way)?T)The unification procedure will normalize unnormalize types when it encounters them. Normalizing a nominal type has no effect (and we can “eagerly” do it). Normalizing a projection works as I described, but the fallback is to a skolemized type (both skolemied and nominal types fall into the “applicative” category).
The difference between skolemized and nominal types is slight, and has to do with the amount of certainty we get in a negative result. In terms of the yes-maybe-no results that @aturon discussed in his post on negative and modal logic, if you have some skolemized type T, then T = U (where U is some other type) is not provable, but it yields a “maybe” result. In contrast, Vec<T> = Rc<T> yields a “no” result. (This is not how chalk currently behaves, actually, it will give a No result for both; this is because I had not imagined the Maybe results being used in quite this way, and instead imagined a distinct A != B predicate – I’m not quite sure how this all works out, but I think @aturon’s approach will wind up more compact.)
Where does Vec<T> = Vec<U> fit on that nominal/skolemized line?
i.e. can Vec be nominal while the T inside is still skolemized?
Yes, the category is just the outermost type, basically (the one being “applied” to other types).
Oh, I forgot to point out something: we have other instances of unnormalized types in Rust beyond associated types. In particular, type aliases can be thought of in the same way. This would allow us to fix the long-standing issue where trait bounds in type aliases are ignored (like type Foo<T: Iterator>).
I have been working in this area for a while, although my approach is more around defining the language around what is natural for the ‘logic’ of the type system. If you look at my GitHub i have a couple of related projects, one is a compositional type system, and the other is Clors which is my equivalent of Chalk. There is an example Clors program that implements the same type compositional type system as my C++ code in tiny amount of code. I have taken the approach of keeping unification simple, but that is because i am defining type equality as unification.
The comment i wanted to make is that Prolog solvers have a common way of dealing with the problem you encountered with associated types, and it is “deferred goals”. In this way you do not need to introduce a new constraint beyond equality to solve associated types, you just add a deferred goal for the reduction that you cannot yet solve. You then replace the type variable with a special “deferred” type variable, which triggers the re-evaluation of the deferred goal if the variable is unified with a ground type in the future. This keeps things ordered and deterministic, instead if introducing a different kind of solver (as constraint solvers have no ordering, and may never terminate).
You will also find this necessary to implement the “does not equal” constraint, and in fact it’s powerful enough to handle general inequalities when you add an integer kind into the mix.
I could probably discuss this whole topic a lot more, as i have spent years on it, most of it getting nowhere on negation. It turns out disequality is easy and safe, but the definition of negation is problematic. Lots of papers have been written on negation as failure (it’s unsound), negation as contradiction, negation as inconsistency etc. In the end the only sound option to me appears to be to rewrite the logic program using disequality, which is easy for simple clauses, but gets really tricky with recursion.
A final comment is i don’t think you need ‘forall’ from first order logic in the logic-language. Prolog like languages generalise variables on instantiation, in other words every clause is implicitly university quantified at the outermost position of the clause head. You can rewrite clauses that have an inner forall into a set of clauses that do not. It really depends on your approach to ‘proof’. My approach has been to keep the core logic small, so it is trivial to prove correct, and then to implement features like type classes by translation into the simple core logic. I guess i may need to reconsider to keep things neet and solving time down, but i have put this kind of decision off until i have implemented negation.
For anyone interested, here is my compositional type-inference algorithm written as a Clors program:
member(Key, cons(Head, Tail), Val) :-
dif(Key,Head),
member(Key, Tail, Val).
member(Key, cons(def(Key, Val), Tail), just(Val)).
member(Key, nil, nothing).
append(cons(H, T1), L, cons(H, T2)) :-
append(T1, L, T2).
append(nil, L, L).
unifyall(cons(T, Tail), T) :-
unifyall(Tail, T).
unifyall(nil, T).
unifyeach(cons(Tapp, Tail), Tdef, Cxt) :-
duplicate_term(Tdef, pair(C1, Tapp)),
unifyeach(Tail, Tdef, Csub),
append(Csub, C1, Cxt).
unifyeach(nil, T, nil).
split(X, cons(def(Y, T), Tail1), Tail2, cons(def(Y, T), Tail3)) :-
dif(X, Y),
split(X, Tail1, Tail2, Tail3).
split(X, cons(def(X, T), Tail1), cons(T, Tail2), Tail3 ) :-
split(X, Tail1, Tail2, Tail3).
split(X, nil, nil, nil).
#-----------------------------------------------------------------------------
nat(zero).
nat(succ(X)) :-
nat(X).
bool(true).
bool(false).
#-----------------------------------------------------------------------------
# type inference
expr(var(X), cons(def(X, Type), nil), Type).
expr(nat(X), nil, nat) :-
nat(X).
expr(bool(X), nil, bool) :-
bool(X).
expr(pair(X, Y), C3, prod(A, B)) :-
expr(X, C1, A),
expr(Y, C2, B),
append(C1, C2, C3).
expr(app(Fun, Arg), Cxt, B) :-
expr(Fun, C1, arrow(A, B)),
expr(Arg, C2, A),
append(C1, C2, Cxt).
expr(lam(Var, Body), Cxt, arrow(A, B)) :-
expr(Body, C1, B),
split(Var, C1, Def, Cxt),
unifyall(Def, A).
expr(let(Var, Body, Rhs), Cxt, T2) :-
expr(Body, C1, T1),
expr(Rhs, C2, T2),
split(Var, C2, Def, C3),
unifyeach(Def, pair(C1, T1), C4),
append(C3, C4, Cxt).
:- expr(
let(cast2, lam(f, lam(x, lam(y, app(app(var(f), var(x)), var(y))))), var(cast2)),
Cxt, Typ).
:- expr(lam(x, let(y, var(x), var(y))), C, T).
:- expr(let(id, lam(x, var(x)), var(id)), C, T).
Its worth noting this is a pure prolog like logic language. The interpreter has no built-in definitions except ‘dif’ which is the disequality constraint, and ‘duplicate_term’ which takes a fresh instantiation of the first argument (with fresh type-variables) and unifies it with the second argument. At the top are the four helper definitions needed for the algorithm, and then we define a couple of primitive types (Bool, and Nat). Finally the algorithm itself which is very short and neat, and some examples. This algorithm infers compositional principal typings. Because it is bottom-up variable capture is not a problem for the algorithm, and we do not need to add first class names or other complexities to cope with variable capture.
Thanks for the tip. Sorry for not writing back earlier, got distracted. I was not aware of this term (“deferred goals”) but what you wrote all made sense to me, and seems indeed to be very similar to what chalk is doing (that is, chalk already has a way to defer goals that it can’t make progress on and come back to them later, as well – it doesn’t really take the typical DFS approach of a standard prolog engine).
I’m not sure I agree with this, though. When you universally quantify in a clause, that’s quite different from having universal quantification in a goal, no? In particular, when we instantiate the forall from a clause, we replace all the variables with fresh inference variables, rather than skolemized variables? Perhaps there is some way to rewrite the queries to achieve the same goals. Even so, adding support for “forall goals” is not particularly complex, and it certainly makes typing generic functions as well as things like higher-ranked trait bounds much more natural.
You might be right about forall, I have ended up adding a primitive that creates an instantiation of a clause with fresh type variables, which might be implementable with universal quantification, although I am not sure, I don’t really have the time to think about it right now as I have some other deadlines to meet 
I need to look if this is solving the same problem or a different one. I suspect this may be an example of tackling things in a different order, as negation has been a sticking point for me for some time.
The advantage of the Prolog approach to deferred goals is that reduction is deterministic and you know you have either got a solution or it is unsolvable, whereas with constraint solvers you can be unsure all the possible orders of constraints have been tried due to the combinatorial explosion.