Haskell is the world’s best programming language1, but let’s face the harsh reality that a lot of times in life you’ll have to write in other programming languages. But alas you have been fully Haskell-brained and lost all ability to program unless it is type-directed, you don’t even know how to start writing a program without imagining its shape as a type first.
Well, fear not. The foundational theory behind Algebraic Data Types and Generalized Algebraic Data Types (ADTs and GADTs) are so fundamental that they’ll fit (somewhat) seamlessly into whatever language you’re forced to write. After all, if they can fit profunctor optics in Microsoft’s Java code, the sky’s the limit!
This is an “April Fools” joke in the tradition of my previous one in some of these ways that we are going to twist these other languages might seem unconventional or possibly ill-advised… but also the title is definitely a lie: these languages definitely should have them! :D
Normal ADTs
As a reminder, algebraic Data Types (ADTs) are products and sums; that’s why they’re algebraic, after all!
Product Types
Products are just immutable structs, which pretty much every language supports — as long as you’re able to make sure they are never mutated.
Structs in c, for example, look like:
But you’ll need proper immutable API for it:
Transaction createTransaction(uint32_t timestamp, double amount) {
return (Transaction){ timestamp, amount};
}
uint32_t getTimestamp(const Transaction* t) {
return t->timestamp;
}
double getAmount(const Transaction* t) {
return t->amount;
}
Transaction setTimestamp(const Transaction* t, uint32_t timestamp) {
return (Transaction){timestamp, t->amount};
}
Transaction setAmount(const Transaction* t, double amount) {
return (Transaction){t->timestamp, amount};
}This is much simpler in languages where you can associate functions with data, like OOP and classes. For example, this is the common “value object” pattern in java (roughly related to the java bean2):
public class Transaction {
private final long timestamp;
private final double amount;
public Transaction(long timestamp, double amount) {
this.timestamp = timestamp;
this.amount = amount;
}
public long getTimestamp() { return timestamp; }
public double getAmount() { return amount; }
public Transaction setTimestamp(long newTimestamp) {
return new Transaction(newTimestamp, this.amount);
}
public Transaction setAmount(double newAmount) {
return new Transaction(this.timestamp, newAmount);
}
}And there you go. Nothing too surprising there!
In this case, not only are these ADTs (algebraic data types), they’re also ADTs (abstract data types): you are meant to work with them based on a pre-defined abstract interface based on type algebra, instead of their internal representations.
Sum Types
If your language doesn’t support sum types, usually the way to go is with the visitor pattern: the underlying implementation is hidden, and the only way to process a sum type value is by providing handlers for every branch — a pattern match as a function, essentially. Your sum values then basically determine which handler is called.
For example, we can implement it for a network address type that can either be IPv4 or IPv6. Here we are using C++ just for generics and lambdas with closures, for simplicity, but we’ll discuss how this might look in C later.
#include <iostream>
#include <format>
#include <cstdint>
struct IPAddress {
bool isIPv4;
union {
uint32_t ipv4;
uint8_t ipv6[16];
};
};
template <typename R>
struct IPAddressVisitor {
R (*visitIPv4)(uint32_t);
R (*visitIPv6)(const uint8_t (&)[16]);
};
template <typename R>
R acceptIPAddress(const IPAddress& ip, IPAddressVisitor<R> visitor) {
return ip.isIPv4 ? visitor.visitIPv4(ip.ipv4)
: visitor.visitIPv6(ip.ipv6);
}You can create the values using:
IPAddress mkIPv4(uint32_t value) {
return { true, { value } };
}
IPAddress mkIPv6(const uint8_t (&value)[16]) {
IPAddress out = { false };
std::copy(std::begin(value), std::end(value), out.ipv6);
return out;
}And we can show an address:
std::string showIPAddress(const IPAddress& ip) {
IPAddressVisitor<std::string> visitor = {
[](uint32_t v) {
return std::format("{}.{}.{}.{}",
(v >> 24) & 0xFF, (v >> 16) & 0xFF,
(v >> 8) & 0xFF, v & 0xFF);
},
[](const uint8_t (&v)[16]) {
return std::format("{:02X}{:02X}:{:02X}{:02X}:{:02X}{:02X}:{:02X}{:02X}:"
"{:02X}{:02X}:{:02X}{:02X}:{:02X}{:02X}:{:02X}{:02X}",
v[0], v[1], v[2], v[3], v[4], v[5], v[6], v[7],
v[8], v[9], v[10], v[11], v[12], v[13], v[14], v[15]);
}
};
return acceptIPAddress(ip, visitor);
}Note that in this way, the compiler enforces that we handle every branch.
And, if we ever add a new branch, everything that ever consumes
IPAddress with an IPAddressVisitor will have to add a
new handler.
In a language without generics or powerful enough polymorphism, it’s difficult to enforce the “pure” visitor pattern because you can’t ensure that all branches return the same type.
One common pattern is to have an “effectful” visitor pattern, where the point isn’t to return something, but to execute something on the payload of the present branch. This is pretty effective for languages like C, javascript, python, etc. where types aren’t really a rigid thing.
For example, this might be how you treat an “implicit nullable”:
export const visitMaybe = (visitNothing, visitJust, val) =>
(val == null) ? visitNothing() : visitJust(val);This is basically for_ from Haskell: You can do something like
conditionally launch some action if the value is present.
visitMaybe(
() => console.log("Nothing to request"),
(reqPayload) => makeRequest("google.com", reqPayload),
maybeRequest
);On a simpler note, if your language as subtyping built in (maybe with classes and subclasses) or some other form of dynamic dispatch, you can implement it in terms of that, which is nice in python, java, C++, etc.
interface ExprVisitor<R> {
R visitLit(int value);
R visitNegate(Expr unary);
R visitAdd(Expr left, Expr right);
R visitMul(Expr left, Expr right);
}
abstract class Expr {
public abstract <R> R accept(ExprVisitor<R> visitor);
}Alternatively, you’re in a language where lambdas are easy, instead of
tupling up the visitor, you could just have accept itself take a
number of arguments corresponding to each constructor:
// Alternative definition without an explicit Visitor class
abstract class Expr {
public abstract <R> R accept(
Function<int,R> visitLit,
Function<Expr,R> visitNegate,
BiFunction<Expr,Expr,R> visitAdd,
BiFunction<Expr,Expr,R> visitMul
);
}(Note that C++ doesn’t allow template virtual methods — not because it’s not possible within the language semantics and syntax, but rather because the maintainers are too lazy to add it — so doing this faithfully requires a bit more creativity)
Now, if your language has dynamic dispatch or subclass polymorphism, you can
actually do a different encoding, instead of the tagged union. This will work in
languages that don’t allow or fully support naked union types, too. In this
method, each constructor becomes a class, but it’s important to only
allow access using accept to properly enforce the sum type
pattern.
class Lit extends Expr {
private final int value;
public Lit(int value) {
this.value = value;
}
@Override
public <R> R accept(ExprVisitor<R> visitor) {
return visitor.visitLit(value);
}
}
class Negate extends Expr {
private final Expr unary;
public Negate(Expr unary) { this.unary = unary; }
@Override
public <R> R accept(ExprVisitor<R> visitor) {
return visitor.visitNegate(unary);
}
}
class Add extends Expr {
private final Expr left;
private final Expr right;
public Add(Expr left, Expr right) {
this.left = left;
this.right = right;
}
@Override
public <R> R accept(ExprVisitor<R> visitor) {
return visitor.visitAdd(left, right);
}
}
class Mul extends Expr {
private final Expr left;
private final Expr right;
public Mul(Expr left, Expr right) {
this.left = left;
this.right = right;
}
@Override
public <R> R accept(ExprVisitor<R> visitor) {
return visitor.visitMul(left, right);
}
}(But, just wanted to note that if you actually are working in java, you can actually do something with sealed classes, which allows exhaustiveness checking for its native switch/case statements.)
Alternatively you could make all of the subclasses anonymous and expose them as factory methods, if your language allows it:
abstract class Expr {
public abstract <R> R accept(ExprVisitor<R> visitor);
public static Expr lit(int value) {
return new Expr() {
@Override
public <R> R accept(ExprVisitor<R> visitor) {
return visitor.visitLit(value);
}
};
}
public static Expr negate(Expr unary) {
return new Expr() {
@Override
public <R> R accept(ExprVisitor<R> visitor) {
return visitor.visitNegate(unary);
}
};
}
public static Expr add(Expr left, Expr right) {
return new Expr() {
@Override
public <R> R accept(ExprVisitor<R> visitor) {
return visitor.visitAdd(left, right);
}
};
}
// ... etc
}You’d then call using:
public class Main {
public static void main(String[] args) {
Expr expr = new Mul(new Negate(new Add(new Lit(4), new Lit(5))), new Lit(8));
// or
// Expr expr = Eval.mul(Eval.negate(Eval.add(Eval.lit(4), Eval.lit(5))), Eval.lit(8));
ExprVisitor<Integer> eval = new ExprVisitor<>() {
@Override public Integer visitLit(int value) {
return value;
}
@Override public Integer visitNegate(Expr unary) {
return -unary.accept(this);
}
@Override public Integer visitAdd(Expr left, Expr right) {
return left.accept(this) + right.accept(this);
}
@Override public Integer visitMul(Expr left, Expr right) {
return left.accept(this) * right.accept(this);
}
};
System.out.println("Result: " + expr.accept(eval));
}
}Passing around function references like this is actually pretty close to the scott encoding of our data type — and for non-recursive types, it’s essentially the church encoding.
Recursive Types
Speaking of recursive types…what if your language doesn’t allow recursive
data types? What if it doesn’t allow recursion at all, or what if recursively
generated values are just annoying to deal with? Just imagine writing that
Expr type in a language with explicit memory management, for
example. Or, what if you wanted a way to express your recursive types in a more
elegant and runtime-safe manner?
One thing you can instead do is have your visitor be in its “catamorphism”, or church encoding. Instead of having the “visitor” take the recursive sub-values, instead have it return the result of recursively applying itself.
Let’s do this in dhall, one of the most famous non-recursive languages. Dhall does have native sum types, so we won’t worry about manually writing a visitor pattern. But it does not have recursive data types.
Let’s define a type like:
But we can’t define data types in dhall that refer to themselves. So instead,
we can define them in their “church encoding”: give what you would do with an
Expr to consume it, where the consumption function is given as if
it were recursively applied.
let ExprF : Type -> Type
= \(r : Type) ->
{ lit : Natural -> r
, add : r -> r -> r
, mul : r -> r -> r
}
let Expr : Type
= forall (r : Type) -> ExprF r -> rNote that ExprF r is essentially
ExprVisitor<R>, except instead of add being
Expr -> Expr -> r, it’s r -> r -> r: the
input values aren’t the expression, but rather the results of recursively
folding on the expression. In fact, our original non-recursive
ExprVisitor<R> (to be more precise, the
R accept(ExprVisitor<R>)) is often called the “scott
encoding”, as opposed to the recursive “church encoding” fold.
For value creation, you take the visitor and recursively apply:
let lit : Natural -> Expr
= \(x : Natural) ->
\(r : Type) ->
\(handlers : ExprF r) ->
handlers.lit x
let add : Expr -> Expr -> Expr
= \(left : Expr) ->
\(right : Expr) ->
\(r : Type) ->
\(handlers : ExprF r) ->
handlers.add (left r handlers) (right r handlers)
let mul : Expr -> Expr -> Expr
= \(left : Expr) ->
\(right : Expr) ->
\(r : Type) ->
\(handlers : ExprF r) ->
handlers.mul (left r handlers) (right r handlers)And finally, using the data type involves providing the
handler to fold up from the bottom to top. Note that
add : \(left : Natural) -> \(right : Natural) -> left + right
already assumes that the handler has been applied to the sub-expressions, so you
get Naturals on both sides instead of Expr.
let eval : Expr -> Natural
= \(e : Expr) ->
e Natural
{ lit = \(x : Natural) -> x
, add = \(left : Natural) -> \(right : Natural) -> left + right
, mul = \(left : Natural) -> \(right : Natural) -> left * right
}
let testVal : Expr
= mul (add (lit 4) (lit 5)) (lit 8)
in assert : eval testVal === 72This pattern is useful even in languages with good datatype recursion, like Haskell — it’s actually the recursion-schemes refactoring of a recursive data type, and it can be useful to have it live alongside your normal recursive types. I’ve written this blog post talking about how useful this pattern is to have alongside your normal recursive types.
This pattern is pretty portable to other languages too, as long as you can scrounge together something like Rank-N types:
interface ExprFold<R> {
R foldLit(int value);
R foldNegate(R unary);
R foldAdd(R left, R right);
R foldMul(R left, R right);
}
interface Expr {
public abstract <R> R accept(ExprFold<R> fold);
public static Expr lit(int value) {
return new Expr() {
@Override
public <R> R accept(ExprFold<R> fold) {
return fold.foldLit(value);
}
};
}
public static Expr negate(Expr unary) {
return new Expr() {
@Override
public <R> R accept(ExprFold<R> fold) {
return fold.foldNegate(unary.accept(fold));
}
};
}
// etc.
}By “Rank-N types” here, I mean that your objects can generate polymorphic
functions: given an Expr, you could generate an
<R> R accept(ExprFold <R> fold) for any R,
and not something pre-determined or pre-chosen by your choice of representation
of Expr.
Generalized Algebraic Data Types
You’ve implemented ADTs in your language of choice, or you are currently in a language with native ADTs. Life is good, right? Until that sneaky voice starts whispering in your hear: “we need more type safety.” You resist that urge, maybe even get a lot done without it, but eventually you are compelled to give in and embrace the warm yet harsh embrace of ultimate type safety. Now what?
Singletons and Witnesses
In Haskell, singletons are essentially enums used to associate a value with a reifiable type. “Reifiable” here means that you can take the runtime value of a singleton and use it to bring evidence to the type-level. I ran into a real-world usage of this while writing https://coronavirus.jle.im/, a web-based data visualizer of COVID-19 data (source here) in purescript. I needed a singleton to represent scales for scatter plots and linking them to the data that can be plotted. And, not only did it need to be type-safe in purescript (which has ADTs but not GADTs), it had to be type-safe in the javascript ffi as well.
Here’s how it might look in Haskell:
-- | Numeric types
data NType :: Type -> Type where
NInt :: NType Int
NDouble :: NType Double
NPercent :: NType Percent
-- | Define a scale
data Scale :: Type -> Type where
ScaleDate :: Scale Date
ScaleLinear :: Bool -> NType a -> Scale a -- ^ whether to include zero in the axis or not
ScaleLog :: NType a -> Scale aYou’d then run it like this:
So, we have the type of the input tuples being determined by the
values you pass to plot:
But let’s say we only had ADTs. And then we’re passing them down to a javascript FFI which only has structs and functions. We could drop the type-safety and instead error on runtime, but…no. Type unsafety is not acceptable.
The fundamental ability we want to gain is that if we pattern match on
ScaleDate, then we know a has to be
Date. If we match on NInt, we know that a
has to be Int.
For the sake of this example, we’re going to be implementing a simpler function in purescript and in javascript: a function that takes a scale type and a list of points prints the bounds. In Haskell, this looks like:
data AxisBounds a = AB
{ minValue :: a
, minLabel :: String
, maxValue :: a
, maxLabel :: String
}
displayAxis :: Scale a -> [a] -> AxisBounds a
displayAxis = \case
ScaleDate -> \xs ->
let xMin = minimum xs
xMax = maximum xs
in AB xMin (showDate xMin) xMax (showDate xMax)
ScaleLinear hasZero nt -> \xs ->
displayNumericAxis (if hasZero then 0:xs else xs)
ScaleLog nt ->
displayNumericAxis nt xs
displayNumericAxis :: NType a -> [a] -> AxisBounds a
displayNumericAxis = \case
NInt -> \xs ->
let xMin = minimum xs
xMax = maximum xs
in AB xMin (printf "%d" xMin) xMax (printf "%d" xMax)
NDouble -> \xs ->
let xMin = minimum xs
xMax = maximum xs
in AB xMin (printf "%.4f" xMin) xMax (printf "%.4f" xMax)
NPercent -> \xs ->
let xMin = minimum xs
xMax = maximum xs
in AB xMin (printf "%.1f%%" (xMin*100)) xMax (printf "%.1f%%" (xMax*100))(Pretend the Percent type is just a newtype-wrapped
Float or something)
There are at least two main approaches to do this. We’ll be discussing runtime equality witnesses and Higher-Kinded Eliminators.
Runtime Witnesses and Coyoneda Embedding
The Yoneda Lemma is one of the most powerful tools that Category Theory has yielded as a branch of math, but its sibling coyoneda is one of the most useful Haskell abstractions.
This doesn’t give you GADTs, but it’s a very lightweight way to “downgrade” your GADTs into normal GADTs which is appropriate if you don’t need the full power.
The trick is this: if you have MyGADT a, and you know you are
going to be using it to produce as, you can do a covariant
coyoneda transform.
For example, if you have this type representing potential data sources:
data Source :: Type -> Type where
ByteSource :: Handle -> Source Word
StringSource :: FilePath -> Source String
readByte :: Handle -> IO Word
readString :: FilePath -> IO String
readSource :: Source a -> IO a
readSource = \case
ByteSource h -> readByte h
StringSource fp -> readString fpYou could instead turn Source into a non-GADT by making it a
normal parameterized ADT and adding a X -> a field, which is a
type of CPS transformation:
data Source a =
ByteSource Handle (Word -> a)
| StringSource FilePath (String -> a)
byteSource :: Handle -> Source Word
byteSource h = ByteSource h id
stringSource :: FilePath -> Source String
stringSource fp = StringSource fp id
readSource :: Source a -> IO a
readSource = \case
ByteSource h out -> out <$> readByte h
StringSource fp out -> out <$> readString fpA nice benefit of this method is that Source can now have a
Functor instance, which the original GADT could not.
And, if MyGADT a is going to be consuming
as, you can do the contravariant
coyoneda transform:
This gives it a free Contravariant instance too!
And, if you are going to be both consuming and producing as, you
can do the invariant coyoneda transform
data Interface a =
ByteInterface Handle (Word -> a) (a -> Word)
| StringInterface FilePath (String -> a) (Word -> a)However, in practice, true equality involves being able to lift under injective type constructors, and carrying every single continuation is unwieldy. We can package them up together with a runtime equality witness.
This is something we can put “inside” NInt such that, when we
pattern match on a NType a, the type system can be assured that
a is an Int.
You need some sort of data of type IsEq a b with functions:
refl :: IsEq a ato :: IsEq a b -> a -> bsym :: IsEq a b -> IsEq b atrans :: IsEq a b -> IsEq b c -> IsEq a cinj :: IsEq (f a) (f b) -> IsEq a b
If you have to and sym you also get
from :: IsEq a b -> b -> a.
From all of this, we can recover our original
IsEq a Word -> Word -> a and
IsEq a Word -> a -> Word functions, saving us from having to
put two functions.
Your language of choice might already have this IsEq. But one of
the more interesting ways to me is Leibniz equality (discussed a lot in this
Ryan Scott post), which works in languages with higher-kinded polymorphism.
Leibniz quality in languages with higher-kinded polymorphism means that
a and b are equal if
forall p. p a -> p b: any property of a is also
true of b.
In Haskell, we write this like:
The only possible way to construct a ‘Leibniz’ is with both type parameters
being the same: You can only ever create a value of type
Leibniz a a, never a value of Leibniz a b where
b is not a.
You can prove that this is actually equality by writing functions
Leibniz a b -> Leibniz b a and
Leibniz a b -> Leibniz b c -> Leibniz a c (this
Ryan Scott post goes over it well), but in practice we realize this equality
by safely coercing a and b back and forth:
newtype Identity a = Identity { runIdentity :: a }
to :: Leibniz a b -> a -> b
to (Leibniz f) = runIdentity . f . Identity
newtype Op a b = Op { getOp :: b -> a }
from :: Leibniz a b -> b -> a
from (Leibniz f) = getOp (f (Op id))So, if your language supports higher-kinded Rank-2 types, you have a solution!
There are other solutions in other languages, but they will usually all be language-dependent.
Let’s write everything in purescript. The key difference is we use
map (to isNumber) :: Array a -> Array Number, etc., to get our
Array as something we know it has the type of.
import Text.Printf
newtype Leibniz a b = Leibniz (forall p. p a -> p b)
to :: Leibniz a b -> a -> b
from :: Leibniz a b -> b -> a
data NType a =
NInt (Leibniz a Int)
| NNumber (Leibniz a Number)
| NPercent (Leibniz a Percent)
type AxisBounds a =
{ minValue :: a
, minLabel :: String
, maxValue :: a
, maxLabel :: String
}
displayNumericAxis :: NType a -> Array a -> AxisBounds a
displayNumericAxis = \case
NInt isInt -> \xs ->
let xMin = minimum $ map (to isInt) xs
xMax = maximum $ map (to isInt) xs
showInt = show
in { minValue: xMin
, minLabel: showInt xMin
, maxValue: xMax
, maxLabel: showInt xMax
}
NNumber isNumber -> \xs ->
let xMin = minimum $ map (to isNumber) xs
xMax = maximum $ map (to isNumber) xs
showFloat = printf (Proxy :: Proxy "%.4f") -- it works a little differently
in { minValue: xMin
, minLabel: showFloat xMin
, maxValue: xMax
, maxLabel: showFloat xMax
}
NPercent isPercent -> \xs ->
let xMin = minimum $ map (to isPercent) xs
xMax = maximum $ map (to isPercent) xs
showPercent = printf (Proxy :: Proxy "%.1f%%") <<< (_ * 100.0)
in { minValue: xMin
, minLabel: showPercent xMin
, maxValue: xMax
, maxLabel: showPercent xMax
}To work with our [a] as if it were [Int], we have
to map the coercion function over it that our Leibniz a Int gave
us. Admittedly, this naive way adds a runtime cost of copying the array. But we
could be more creative with finding the minimum and maximum in this way in
constant space and no extra allocations.
And, if we wanted to outsource this to the javascript FFI, remember that javascript doesn’t quite have sum types, so we can create a quick visitor:
type NVisitor a r =
{ nvInt :: Leibniz a Int -> r
, nvNumber :: Leibniz a Number -> r
, nvPercent :: Leibniz a Percent -> r
}
type NAccept a = forall r. NVisitor a r -> r
toAccept :: NType a -> NAccept a
toAccept = case _ of
NInt isInt -> \nv -> nv.nvInt isInt
NNumber isNumber -> \nv -> nv.nvNumber isNumber
NPercent isPercent -> \nv -> nv.nvPercent isPercent
foreign import _formatNumeric :: forall a. Fn2 (NAccept a) a String
formatNumeric :: NType a -> a -> String
formatNumeric nt = runFn2 _formatNumeric (toAccept nt)The FFI binding looks like: (taken from my actual source code)
import * as d3 from "d3-format";
export const _formatNumeric = (naccept, xs) =>
naccept(
{ nvInt: (isInt) => d3.format("~s")
, nvNumber: (isNumber) => d3.format(".3~s")
, nvPercent: (isPercent) => d3.format("+.3~p")
}
);Admittedly in the javascript we are throwing away the “GADT type safety” because we throw away the equality. But we take what we can — we at least retain the visitor pattern for sum-type type safety and exhaustiveness checking. I haven’t done this in typescript yet so there might be a way to formalize Leibniz equality to do this in typescript and keep the whole chain type-safe from top to bottom.
Higher-Kinded Eliminators
This is essentially the higher-kinded version of the visitor pattern, except in dependent type theory these visitors are more often called “eliminators” or destructors, which is definitely a cooler name.
In the normal visitor you’d have:
data User = TheAdmin | Member Int
data UserHandler r = UH
{ uhTheAdmin :: r
, uhMember :: Int -> r
}But note that if you have the right set of continuations, you have something
that is essentially equal to User without having to actually use
User:
type User' = forall r. UserHandler r -> r
fromUser :: User -> User'
fromUser = \case
TheAdmin -> \UH{..} -> uhTheAdmin
Member userId -> \UH{..} -> uhMember userId
toUser :: User' -> Foo
toUser f = f $ UH { fhTheAdmin = TheAdmin, fhMember = Member }This means that User is actually equivalent to
forall r. UserHandler r -> r: they’re the same type, so if your
language doesn’t have sum types, you could encode it as
forall r. UserHandler r -> r instead. Visitors, baby.
But, then, what actually does the r type variable represent
here, semantically? Well, in a UserHandler r, r is the
“target” that we interpret into. But there’s a deeper relationship between
r and User: A UserHandler r essentially
“embeds” a User into an r. And, a
UserHandler r -> r is the application of that embedding to an
actual User.
If we pick r ~ (), then UserHandler () embeds
User into (). If we pick r ~ String, then
UserHandler () embeds User into String
(like, “showing” it). And if we pick r ~ User, a
UserHandler User embeds a User into…itself?
So here, r is essentially the projection that we view the user
through. And by making sure we are forall r. UserHandler r -> r
for all r, we ensure that we do not lose any information:
the embedding is completely 1-to-1. It lets you “create” the User
faithfully in a “polymorphic” way.
In fact, to hammer this home, some people like to use the name of the type as
the type variable: UserHandler user:
-- | The same thing as before but with things renamed to prove a point
data MakeUser user = MakeUser
{ uhTheAdmin :: user
, uhMember :: Int -> user
}
type User' = forall user. MakeUser user -> userThe forall user. lets us faithfully “create” a User
within the system we have, without actually having a User data
type. Essentially we can imagine the r in the forall r
as “standing in” for User, even if that type doesn’t actually
exist.
Now, here’s the breakthrough: If we can use forall (r :: Type)
to substitute for User :: Type, how about we use a
forall (p :: Type -> Type) to substitute for a
Scale :: Type -> Type?
data Scale :: Type -> Type where
ScaleDate :: Scale Date
ScaleLinear :: Bool -> LType a -> Scale a
ScaleLog :: NType a -> Scale a
data ScaleHandler p a = SH
{ shDate :: p Date
, shLinear :: Bool -> NType a -> p a
, shLog :: NType a -> p a
}
type Scale' a = forall p. ScaleHandler p a -> p a
fromScale :: Scale a -> Scale' a
fromScale = \case
ScaleDate -> \SH{..} -> shDate
ScaleLinear hasZero lt -> \SH{..} -> shLinear hasZero lt
ScaleLog nt -> \SH{..} -> shLog nt
toScale :: Scale' a -> Scale a
toScale f = f $ SH { shDate = ScaleDate, shLinear = ScaleLinear, shLog = ScaleLog }So in our new system, forall p. ScaleHandler p a -> p a is
identical to Scale: we can use p a to substitute in
Scale in our language even if our language itself cannot support
GADTs.
So let’s write formatNType in purescript. We no longer have an
actual Scale sum type, but its higher-kinded church encoding:
type NType a = forall p.
{ int :: p Int
, number :: p Number
, percent :: p Percent
} -> p a
type Scale a = forall p.
{ date :: p Date
, linear :: Bool -> NType a -> p a
, log :: NType a -> p a
} -> p a
ntInt :: NType Int
ntInt nth = nth.int
ntNumber :: NType Number
ntNumber nth = nth.number
ntPercent :: NType Percent
ntPercent nth = nth.percent
formatNType :: NType a -> a -> String
formatNType nt = f
where
Op f = nt
{ int: Op show
, number: Op $ printf (Proxy "%.4f")
, percent: Op $ printf (Proxy "%.1f%%") <<< (_ * 100.0)
}Here we are using
as our “target”: turning an NType a into an
Op String a. And an Op String a is an
a -> String, which is what we wanted! The int field
is Op String Int, the number field is
Op String Number, etc.
In many languages, using this technique effectively requires having a newtype
wrapper on-hand, so it might be unwieldy in non-trivial situations. For example,
if we wanted to write our previous axis function which is
NType a -> [a] -> String, we’d have to have a newtype wrapper
for [a] -> String that has a as its argument:
or you could re-use Compose:
and your p projection type would be Compose Op [].
So, you don’t necessarily have to write a bespoke newtype wrapper, but you do
have to devote some brain cycles to think it through (unless you’re in a
language that doesn’t need newtype wrappers to have this work, like we’ll
discuss later).
By the way, this method generalizes well to multiple arguments: if you have a
type like MyGADT a b c, you just need to project into a
forall (p :: k1 -> k2 -> k3 -> Type).
I believe I have read somewhere that the two methods discussed here (runtime equality witness vs. higher-kinded eliminator) are not actually fully identical in their power, and there are GADTs where one would work and not the other … but I can’t remember where I read this and I’m also not big-brained enough to figure out what those situations are. But if you, reader, have any idea, please let me know!
Existential Types
Let’s take a quick break to talk about something that’s not technically related to GADTs but is often used alongside them.
What if we wanted to store a value with its NType and hide the
type variable? In Haskell we’d write this like:
data NType :: Type -> Type where
NInt :: NType Int
NDouble :: NType Double
NPercent :: NType Percent
data SomeNType = forall a. SomeNType (NType a) a
formatNType :: NType a -> a -> String
formatNType nt x = ...
formatSomeNType :: SomeNType -> String
formatSomeNType (SomeNType nt x) = formatNType nt x
myFavoriteNumbers :: [SomeNType]
myFavoriteNumbers = [SomeNType NInt 3, SomeNType NDouble pi]But what if our language doesn’t have existentials? Remember, this is
basically a value SomeNType that isn’t a Generic, but
contains both a NType a and an a of the
same variable.
One strategy we have available is to CPS-transform our existentials into their CPS form (continuation-passing style form). Basically, we write exactly what we want to do with our contents if we pattern matched on them. It’s essentially a Rank-N visitor pattern with only a single constructor:
type SomeNType = forall r. (forall a. NType a -> a -> r) -> r
someNType :: NType a -> a -> SomeNType
someNType nt x = \f -> f nt x
formatSomeNumeric :: SomeNType -> String
formatSomeNumeric snt = snt
\nt x -> formatNumeric nt xYou can imagine, syntactically, that snt acts as its “own”
pattern match, except instead of matching on
SomeNType nt x -> .., you “match” on
\nt x -> ..
This general pattern works for languages with traditional generics like Java too:
interface SomeNTypeVisitor<R> {
<A> R visit(NType<A> nt, A val);
}
interface SomeNType {
public abstract <R> R accept(SomeNTypeVisitor<R> visitor);
// One option: the factory method
public static <A> SomeNType someNType(NType<A> nt, A val) {
return new SomeNType() {
@Override
public <R> R accept(SomeNTypeVisitor<R> visitor) {
return visitor.visit(nt, val);
}
};
}
}
// Second option: the subtype hiding a type variable, which you have to always
// make sure to upcast into `SomeNType` after creating
class SomeNTypeImpl<A> extends SomeNType {
private NType<A> nt;
private A val;
public SomeNTypeImpl(NType<A> nt, A val) {
this.nt = nt;
this.val = val;
}
@Override
public <R> R accept(SomeNTypeVisitor<R> visitor) {
return visitor.visit(nt, val);
}
}Does…anyone write java like this? I tried committing this once while at Google and I got automatically flagged to be put on a PIP.
Recursive GADTs
The climax of this discussion: what if your language does not support GADTs or recursive data types?
We’re going to be using dhall as an example again, but note that the lessons applied here are potentially useful even when you do have recursive types: we’re going to be talking about a higher-kinded church encoding, which can be a useful form of your data types that live alongside your normal recursive ones.
Let’s imagine Expr as a GADT, where Expr a
represents an Expr that evaluates to an a:
data Expr :: Type -> Type where
NatLit :: Natural -> Expr Natural
BoolLit :: Bool -> Expr Bool
Add :: Expr Natural -> Expr Natural -> Expr Natural
LTE :: Expr Natural -> Expr Natural -> Expr Bool
Ternary :: Expr Bool -> Expr a -> Expr a -> Expr a
eval :: Expr a -> a
eval = \case
NatLit n -> n
BoolLit b -> b
Add x y -> eval x + eval y
LTE a b -> eval a <= eval b
Ternary b x y -> if eval b then eval x else eval yAdding this type variable ensures that our Expr is type-safe:
it’s impossible to Add an Expr Bool, and the two
branches of a Ternary must have the same result type, etc. And, we
can write eval :: Expr a -> a and know exactly what type will be
returned.
Now, let’s combine the two concepts: First, the church encoding, where our
handlers take the “final result” of our fold r instead of the
recursive value Expr. Second, the higher-kinded eliminator pattern
where we embed Expr :: Type -> Type into
forall (p :: Type -> Type).
And finally, we get:3
let ExprF =
\(p : Type -> Type) ->
{ natLit : Natural -> p Natural
, boolLit : Bool -> p Bool
, add : p Natural -> p Natural -> p Natural
, ternary : forall (a : Type) -> p Bool -> p a -> p a -> p a
}
let Expr
: Type -> Type
= \(a : Type) -> forall (p : Type -> Type) -> ExprF p -> p a
let eval
: forall (a : Type) -> Expr a -> a
= \(a : Type) ->
\(e : Expr a) ->
e
(\(q : Type) -> q)
{ natLit = \(x : Natural) -> x
, boolLit = \(x : Bool) -> x
, add = \(x : Natural) -> \(y : Natural) -> x + y
, ternary =
\(a : Type) ->
\(b : Bool) ->
\(x : a) ->
\(y : a) ->
if b then x else y
}Again, now instead of add taking Expr, it takes
p Natural: the “Natural result of the fold”.
p not only stands in for what we embed Expr into, it
stands in for the result of the recursive fold. That’s why in eval,
the first arguments of add are the Natural results of
the sub-evaluation.
These values can be created in the same way as before, merging the two techniques, sending the handlers downstream:
let natLit
: Natural -> Expr Natural
= \(n : Natural) ->
\(p : Type -> Type) ->
\(handlers : ExprF p) ->
handlers.natLit n
let boolLit
: Bool -> Expr Bool
= \(n : Bool) ->
\(p : Type -> Type) ->
\(handlers : ExprF p) ->
handlers.boolLit n
let add
: Expr Natural -> Expr Natural -> Expr Natural
= \(x : Expr Natural) ->
\(y : Expr Natural) ->
\(p : Type -> Type) ->
\(handlers : ExprF p) ->
handlers.add (x p handlers) (y p handlers)
let ternary
: forall (a : Type) -> Expr Bool -> Expr a -> Expr a -> Expr a
= \(a : Type) ->
\(b : Expr Bool) ->
\(x : Expr a) ->
\(y : Expr a) ->
\(p : Type -> Type) ->
\(handlers : ExprF p) ->
handlers.ternary (b p handlers) (x p handlers) (y p handlers)
let testVal
: Expr Natural
= add (natLit 5) (add (natLit 6) (natLit 7))
in assert : eval testVal === 18If all of this is difficult to parse, try reviewing both the recursive ADT section and the higher-kinded eliminator section and making sure you understand both well before tackling this, which combines them together!
Admittedly in Haskell (and purescript) this is a lot simpler because we don’t have to explicitly pass in type variables:
data ExprF p = ExprF
{ natLit :: Natural -> p Natural
, boolLit :: Bool -> p Bool
, add :: p Natural -> p Natural -> p Natural
, ternary :: forall a. p Bool -> p a -> p a -> p a
}
type Expr a = forall p. ExprF p a -> p a
eval :: Expr a -> a
eval e = runIdentity $
e
{ natLit = Identity
, boolLit = Identity
, add = \(Identity x) -> \(Identity y) -> Identity (x + y)
, ternary = \(Identity b) -> \(Identity x) -> \(Identity y) -> if b then x else y
}
ternary :: Expr Bool -> Expr a -> Expr a -> Expr a
ternary b x y handlers = handlers.ternary (b handlers) (x handlers) (y handlers)But one nice thing about the dhall version that’s incidental to dhall is that it doesn’t require any extra newtype wrappers like the Haskell one does. That’s because type inference tends to choke on things like this, but dhall doesn’t really have any type inference: all of the types are passed explicitly. It’s one of the facts about dhall that make it nice for things like this.
Congratulations
In any case, if you’ve made it this far, congratulations! You are a master of ADTs and GADTs. Admittedly every language is different, and some of these solutions have to be tweaked for the language in question. And, if your program gets very complicated, there is a good chance that things will become ergonomically unfeasible.
But I hope, at least, that this inspires your imagination to try to bring your haskell principles, techniques, standards, practices, and brainrot into the language of your choice (or language you are forced to work with).
And, if you ever find interesting ways to bring these things into a language not discussed here (or a new interesting technique or pattern), I would absolutely love to hear about it!
Until next time, happy “Haskelling”!
Special Thanks
I am very humbled to be supported by an amazing community, who make it possible for me to devote time to researching and writing these posts. Very special thanks to my supporter at the “Amazing” level on patreon, Josh Vera! :)
I bet you thought there was going be some sort of caveat in this footnote, didn’t you?↩︎
I didn’t think I’d ever write “java bean” non-ironically on my blog, but there’s a first time for everything.↩︎
Be aware that this implementation is not necessarily appropriately lazy or short-circuiting in
Ternary: it might evaluate both sides returning the chosen branch.↩︎
can be used to engrave any of the
three syllables 송 승 숭 the operator has actually used it
to engrave the first of these.
</noscript>
</noscript>
</noscript>
</noscript>
</noscript>
Submission Deadline: 9 February 2025
Never spoken before? No worries! We’re committed to supporting speakers from all backgrounds, especially those from underrepresented groups in tech.
.jpeg){kind=link}