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


Skip to first unread message

Aram Hăvărneanu's profile photo
unread,
10:25 AM (5 hours ago) 10:25 AM
Sign in to reply to author
You do not have permission to delete messages in this group
Sign in to report message as abuse
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
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