- Canonical Structures
- Unification Hints
- Functional Dependencies
- Associated Types
basic 1 parametr type classes
class Eq a
class Coerc a b
class Collect e ce
Quantified class constraints harrop extension to typeclass clauses
Typeclasses vs Canonical Structures. I don’t get it. Could I make a model? Maybe in prolog? Diamond problem Inheritance. What are typeclasses? “Kind of like prolog” Things are incompatible for some reason? Canonical structures add unification hints? canonical structures ofr the working coq user - mahboubi tassi
How to Make Ad Hoc Proof Automation Less Ad Hoc Type parameters on the outside vs inside. Canonical structures have them inside. packed records
Dependently Typed Records for Representing Mathematical Structure - Pollack “pebble style” pakced vs unpacked
First Class Type Classes - Sozeau and Oury not canonical structures but it is in coq.
Hints in unification Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi interesting paper. Describes how typeclasses and canonical structures can be put under a similar umbrella as extesnible unification mechanisms.
Coherence - typeclass systems can have diamonds
Diamonds are what are feared and dreaded. Why exacty?
trait coherence little orphan impls Overlapping - typeclass systems often take prolog style unification without backtracking, i.e. only one instance is allowed to apply. This is smart in the sense that it makes thge performance of the system simpler and more reliable, and performance here is compilation time for your users. It is of course also limitting
Instance Chains: Type Class Programming Without Overlapping Instances Non-overlapping means no heads are unifiable
non-overlapping means no backtracking. Can use egglog for unification then. Hmm. but head unification itself needs backtracking.
To me it looks like a refactoring or multiparam typeclasses. Build syntatic rep of rust traits and then compiel to prology stuff from there. impl(Trait(A,B,C), T).
Something to think about: Applications of egglog to typeclass resolution modulo equality. https://arxiv.org/abs/2001.04301 I don’t really have a feel for the relation between tabled top down and magic set transformed bottom up although there clearly is one. I guess I’m also not clear on how magic set works in egglog for that matter. I don’t know how to execute egglog top down in the first place. An example would be finding a typeclass for Vec n a where you take the assoc/comm mult and add axioms on the size index. Presumably the equational axioms must also be associated with instance dictionaries. Hmm. Maybe this is not as straightforward as I thought. You also need instances for congruence? There isn’t a problem with ordinary bottom up egglog, it just seems very wasteful on a query driven application like this
Chalk is also a very good point. The cahlk blog posts exliciitly talk about specialized equality. That is intriguing. I should contact Niko Matsakis. https://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/ Prolog + euqliaty reasoning he syas he’s looking for
Chalk even talks about making a union find.
asscoaited types IntoIterator Item
intoiter(vec(T)) :- intoiter(T). iter_item(vec(T)) = T :- intoiter(vec(T)). eq(T,U) query: into_iter(vec(T))
Good examples of multi arg typeclasses?
Provenance of chalk or polonius are importatn for good error messages.
Guess missing clauses?
We need harrop for generic problems?
stuckey sulzmann - a theory of overloading HM(X) + CHR
Associated types are of some relationship to functional dependencies
Does class Foo a b c | a -> b, a -> c work like class Foo a where type b type c
Typeclasses look like prolog predicates
instances are prolog rules. The proof of a successful resolution is a recipe for building the appropriate
Associated types means a piercing of this barrier
implements(clone,life(A,T)) impl(tostring, life(A,i64)). impl(tostring, vec(T)) :- impl(tostring, T). % associate what trait owns fields traitfield(tostring, tostring). dotcall( foo, tostring ) :- type(foo, T), traitfield(Trait, tostring), impl(Trant, T). % dotcall(TEnv, foo, tostring) % annotate everything with lifetimes? % https://stevedonovan.github.io/rustifications/2018/09/08/common-rust-traits.html % display, default, format, clone, % sized % borrow % from to % iterator
Original Wadler paper
Rust Chalk for Trait inference
BAP universal valures OCaml typeclasss system Oleg modellign typeclasses as prolog https://inbox.ocaml.org/caml-list/20190904152517.GA2014@Melchior.localnet/ http://okmij.org/ftp/ML/index.html#trep
So what is the synctatic condition that precludes search?
Would it be more interesting to just What am I understanding here?
Canonical structures was suggesting that some kind of inconstency would manifest. Maybe lambda prolog gets us closer. We can have existential variables and such.
nat === (carrier nat_abGrp) :- A === A.
nat == carrier(Eq) :- Eq == natEq. carrier(Eq,nat).
nonunifiable(L) :- all( /= , L ).
% haskell has no backtracking % every case has a cut. eq(tup()) :- !. eq(tup(A,B)) :- !, eq(A), eq(B)
eq(int, prim__equal_int). eq(tup(A,B), lambda( x, case( x, tup(a,b) => bool_and( apply(EqualA, a) , apply(EqualB, b ) ) ) ) ) :- eq(A, EqualA), eq(B, EqualB). eq(tup(A,B), comp(and, par(EqualA,EqualB)))
eq(int). eq() eq(tup(A,B)) :- eq(A), eq(B).
functor( maybe ) functor(compose(F,G)) := functor(F), functor(G)
% superclass class(ord(A)) :- call(ord, A), class(eq(A))
“diamonds appear evertwhere. See pullbacks” ~ Hale