PureScript GADTs Alternatives — Recap
GADTs (“Generalized Algebraic Data Types”) provide an explicit instantiation of the ADT as the type instantiation of their return value. This gives you power to define type safe data structures with more advanced type behavior. Unfortunately, in the time of this post, latest version or PureScript (0.12) hasn’t supported GADTs yet.
However, we can overcome the limit with alternative methods. This post is just a recap from what I researched.
The Problem
With GADTs extension, we could write a little eDSL for arithmetic and comparison expressions something like this:
Without GADTs it seems like this eval function would be impossible to write, since we wouldn’t have the information to determine the result type that matching on a data constructor of a GADT gives us.
Leibniz equality
This is recap from Approximating GADTs in PureScript
Two types are equal if they are equal in all contexts.
We can’t directly encode type equalities using the type system in PureScript, but we can take advantage of “Leibniz equality” and encode it in a value instead:
(a ~ b) is a Leibniz value, with a is a variable that is identical with some type b. This allows us to coerce one type to another.
The symm function is used when we have a type equality that we need to “turn around” so that we can coerce in either direction based on a provided Leibniz value. This is possible thanks to the fact that equality relations are symmetric (for every a and b, if a = b then b = a), and is where the name symm comes from.
Go back to the example. In the GADT-defined Expr, the final part of the type annotation for each data constructor, … -> Expr SomeType, is essentially saying “a ~ SomeType for this constructor”.
When a constructor of a GADT is pattern-matched, the type-checker gains knowledge of this equality and then lets us return a value of the appropriate type, rather than being stuck with the rigid type variable a.
We can now write eval using the coerce function to safely cast the result type back to a in each case:
The only thing we haven’t covered is how to actually construct a Leibniz value in the first place. What possible function could we provide that satisfies forall f. f a -> f b where a equals b? The identity function! Leibniz also has a Category instance, so actually we can just use identity directly:
And finally, we can run our original example cases again:
Limitations
As the title of original post, Gary Burgess called it Approximating GADTs. This method can't solve all cases, especially in more complicated eDSLs. For example in polymorphism rank N-type DSL:
Since PureScript doesn’t support existential types in AST, this method is useless.
Tagless Final comes to rescue
In the final approach, object language terms are represented as expressions built from a small set of combinators, which are ordinary functions rather than data constructors. The values of these expressions give denotations of the corresponding object terms. An object term is hence represented not by its abstract syntax but by its denotation in a semantic domain. Abstracting over the domain gives us a family of interpretations. Typed Tagless Final Interpreters — Oleg Kiselyov
The solution
In Tagless Final approach, instead of declaring AST data type directly, we use type class as a set of operations:
It accepts all interpreters that implement those operations
The syntax is similar to Leibniz approach
Tagless Final has more advantages than GADTs and Leibniz approaches:
- Flexible, easy to extend the language with new operations.
- Easier to implement
- Requires less boilerplate.
- Combine different parts of the DSL very easily, without change the existed code
Limitations
From what I researched, because Haskell hasn’t supported impredicative polymorphism. That means that we can’t specialize an existing data type to hold a polymorphic value like this:
Maybe (LambdaSym repr => repr Int)Fortunately, PureScript support impredicative polymorphism. We no need to worry about it.
Conclusion
Compared to Leibniz, or even GADTs, Tagless Final style has many advantage as well as easy to grasp. It is wide adoption in functional programming world. Tagless Final style is a good alternative to GADTs
Originally published at hgiasac.github.io on December 18, 2018.