Our great sponsors
-
chalk
An implementation and definition of the Rust trait system using a PROLOG-like logic solver (by rust-lang)
-
pny1-assignment
College assignment writing in which I ramble about type classes and dependent types.
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
The other secret about typeclasses is that it is an embedded logic programming language in disguise. This is made more explicit in Rust than Haskell, where you have the chalk project https://github.com/rust-lang/chalk which plans to use a logic programming language implementation for trait resolution. An instance declaration like Monoid a => Monoid [a] corresponds to a clause like Monoid(List(A)) :- Monoid(a) in Prolog. Coherence corresponds to a restriction on clauses which guarantees that you will find at most one solution to every query. I think the logic programming aspect were acknowledged more explicitly, good things might come from that. For instance, most logic programming languages have decent debugging tools for analyzing the proof search procedure.
Actually, you can, in a dependently typed language, in a first class way: You require a suitable equality proof. See here for an exploration of how this can work.