Skip to content

Instantly share code, notes, and snippets.

@nmcb
Created July 29, 2018 21:48
Show Gist options
  • Save nmcb/02a9c1e46c0623ad15089091890af127 to your computer and use it in GitHub Desktop.
Save nmcb/02a9c1e46c0623ad15089091890af127 to your computer and use it in GitHub Desktop.

Both the Haskell and Scala communities rely heavily on the type class pattern. Both communities do so in different ways. In application, function, encoding, and compiler and runtime support. Both implement many huge applications constrained in complexity only by the separation of concerns possible and enforced mathematically by type classes. Because type classes have laws. Mathematical laws!

The possibility to write "complex polymorphic recursive encodings of type class instances" is basically what the Scala community is founded upon. Give me some implicit evidence of an implicit type class instance to do some type level algebraic voodoo. That's Scala's 'The Applied Functional Programmers' motto? No? Well, Yes, that is definitely what is cool about Scala. It may be a bit or even a much less principled than Haskell, Scala's seemingly loose dealings with pureness have yielded many good functional type level ideas this past ten year or so. Not everything FP in Scala is a "Haskell Port".

When we zoom in on the compile time guarantees that can be provided to the programmer, the person that actually writes the code that defines a certain type class. The person using them, or provides instances of them. When we zoom in on those guarantees, Haskell trumps Scala. Haskell has keyword support for type class definitions and implementations, they are a first class construct in the machinery of the compiler, but more importantly, other then Scala, Haskell is build on top of a small typed, core language, SystemFC, in which, to quote Peyton Jones, "the syntax of a term encodes its type derivation". Since that derivation for a given type class expression may yield only one possible instance expression of the type that can be used at the type class call site, the Haskell compiler requires only so called 'non-overlapping type class instances' to be in scope. To validate that to be indeed the case, the Haskell compiler coerces the types of possible candidate instances during type derivation in SystemFC. If that yields only one instance of the right type, the code must be typed.

Simply put, the machinery to do type level computations is provided in both Haskell and Scala by the "type derivational phase" of a compiler. Complex polymorphic recursive type class instances, are coerced during this phase and should yield, one and only one type class instance of the right polymorphic type, for each type class call site. Haskell does this type derivation during compilation of its core language representation, thus SystemFC above, and hooks the coerced single instance at compile time into the call site as a function call. This is the reason that Haskell does not require implicit parameters to pass type class instances. Scala, on the other hand, not having language support for type classes, uses its implicit parameter features to implement type class instance derivation at compile time, which yields the same result functionally as Haskell, with the difference being that the actual single coerced type class instance at runtime will be passed as a parameter to the call site, not as a function call as with Scala. These are the mechanical difference between Scala and Haskell: the algebra of the type derivation algorithm used, specially the coercion algebraic part of it, as well as the type system of the language, i.e. SystemF in case of Haskell and the DOT calculus in case of Scala 3.0. to be.

At this stage I don't want to go into how type class instances are resolved by the Scala compiler, firstly because I have no idea, I fiddle till it works, and secondly because I don't want to rant about implicit resolution. Suffice to say that the Scala compiler allows, as far as I know, arbitrary complex polymorphic type class instances, I only saw the compiler complain when either no instance was in scope, or when two instances of the same type were in scope. (With, the same, I mean two instances coerced into the same polymorphic type, the same. There is also no restriction to instances being of a polymorphic, overlapping type).

So, what's the catch with Haskell? Well, remember those mathematical guarantees I was talking about? Type classes having laws and all? In Haskell they are actually not that mathematically proven. Because the type derivation coercion rules in SystemFC, the rules that ultimately decide which type class instance to choose, and what type of overlapping and polymorphism left in the one and only instance to allow. Well, those rules, or actually the axioms they're build upon, are not yet mathematically proven to be sound. The algebra used for coercion is only conjectured to be consistent.

Don't get me wrong, the axioms are very stable, already for aprox 30 years, and in comparison with Scala, Haskell does provide more safety and a more principled way to implement type classes and their instances. (I'll only note the term 'instance chains' here, a principled way to replace multiple instances representing a part of the same type level algebraic computation, with one instance implementing that same computational part as a chained type level conditional expression. It's beautiful). But the underlying algebras that facilitate type level computations, called coercion algebras, are yet to be proven sound, even for Haskell. Coercion algebras as a whole, and specifically the relation between coercion algebras and type algebras is a (less known) area of foundational research, and a (much less known) area bound to have a huge impact on language support for type level algebraic computational support in general and type classes particularly. As both compilers execute type level computations (such as type class instance resolution) during type derivation, it is perhaps better to dignify both goals with different terms. "Type evidence algebra" versus "Type derivation algebra"? I don't know, the sky is the limit. We have all the time in the world. (While we're proving Haskell's algebraic coercion axioms sound).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment