Typed DSL in Go (or sum types and GADTs in Go)

[Aram Hăvărneanu]

Dear Go community,

For your delight, bemusement, or horror, I present to you generalized
algebraic data types in Go: https://play.golang.org/p/83fLiHDTSdY

| This file implements a deep embedding of a typed-DSL in Go.
| The representation is type-safe (we cannot construct ill-typed
| terms) and accepts multiple interpretations. The type system
| of the target language is identity-mapped to the Go type
| system such that type checking of the DSL is hoisted up to
| type-checking the Go code that contains the target language
| expression.
|
| Normally this requires either GADTs or higher-rank types.
| I show that it is possible to encode it in Go, a language
| which doesn't have GADTs (nor regular ADTs for that matter),
| nor higher-rank types. I exploit the duality between universal
| and existential quantification and encode sum types using
| the existential dual of the Boehm-Berarducci isomorphism.
| Unlike the Boehm-Berarducci encoding, my encoding is not
| universally-quantified, but existentially quantified, and
| does not require higher-rank polymorphism capitalizing on
| the fact that Go interfaces are existential types.
|
| Just like an algebraic data type, my encoding is closed,
| its usage is type safe, and the match operations are checked
| at compile-time for exhaustivness.
|
| A related, alternative encoding would be to encode the GADT
| into tagless-final style. This requires polymorphic terms,
| which in Go can only be functions, which are not serializable.
| My encoding is bidirectionally serializable.
|
| As presented, the encoding is closed because I want to show
| that I can encode every GADT property. It is also possible,
| and perhaps desirable to make the encoding open, which
| solves the Expression Problem.
|
| Although GADT invariants are encoded using Go generics
| (which are a form of universal quantification) the encoding
| does not require that the Curry–Howard isomorphism holds,
| it is purely existential. In fact, if one only wants plain
| ADTs, generics are not needed at all. Go can encode sum
| types, and was always able to.

You will need Go tip to compile this.

--
Aram Hăvărneanu

[Aram Hăvărneanu]

And now updated to Go 1.18: https://gotipplay.golang.org/p/kmLRcsXGxSs

While this code looks like performance art, it establishes an
important result. We always felt that generics are extremely
powerful in Go and one of the reasons why we could achieve so much
in Go without generics. But this shows this is true in a strict
mathematical sense, not just in our intuition.

More importantly, I think, is that this shows to other prospective
programming language researchers that designing their future
language starting from existential types instead of universal types
(as it is usually done), is both feasible and perhaps even
desirable.

What's missing is a way to abstract over type constructors, and it
is an open research problem how a language based on existential
types, but with abstraction over type constructors would look and
feel like. We know in a practical setting Go interfaces "don't blow
up", while it's very easy for code that uses generics to "blow up".
It is unclear whether this property will continue to hold if we
introduce abstraction over type constructors.

--
Aram Hăvărneanu