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
--
You received this message because you are subscribed to the Google Groups
"golang-nuts" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to golang-nuts+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/golang-nuts/CAEAzY381kQ0hptu1GbPwKHWAjyUXCj31HoVnOVcCvuXZhSo4rw%40mail.gmail.com.
