You might not need GADTs for that in Unison

🦜

This blog post was written using the Unison documentation format, which supports hyperlinked code, syntax highlighting for most languages, LaTeX, diagrams, etc. Learn more here.

Generalized algebraic data types (GADTs) are data types where not all the constructors have the same return type. For example, the Either type is not a GADT:

►

structural type Either a b = base.Either.Right b | base.Either.Left a

If we look at the signatures of Left and Right, we see they both return a value of the same type, instantiating the type variables in the same way:

Left  : a -> Either a b
Right : b -> Either a b

In a GADT, the constructors can instantiate type variables however they like. Here's some Haskell syntax. The type is Expr e but notice that the constructors have different return types. They're all still of the shape Expr but for instance one returns an Expr Int while another produces an Expr Float.

data Expr e where
  I          : Int -> Expr Int
  F          : Float -> Expr Float
  IntTimes   : Expr Int -> Expr Int -> Expr Int
  FloatTimes : Expr Float -> Expr Float -> Expr Float

In Haskell or other languages that support GADTs, you can then write nicely typechecked interpreters of the type:

eval : Expr a -> a
eval e = case e of 
  I i -> i
  F f -> f
  IntTimes x y -> eval x * eval y
  FloatTimes x y  -> eval x * eval y

But because we have the syntax tree as a data structure, we could also (for instance), convert an Expr to JSON, or generate some C or CUDA code for a simple compiler.

Overall, GADTs are a flexible way of creating nicely typed DSLs that can be introspected for tasks like code generation or serialization.

🤓

When pattern matching on a GADT, the typechecker will introduce equality constraints and make use of them when comparing types. For instance, in eval, the return type must be a, right? When matching on I i, that introduces the equality a ~ Int such that returning an Int in this branch is considered to typecheck.

When you can easily get away with using abilities

Unison doesn't have GADTs, but it does have abilities, and the constructors of an ability are allowed to have different return types, for instance:

►

ability Expr1 where
  float : Float ->{Expr1} E Float
  float.times : E Float -> E Float ->{Expr1} E Float
  nat.times : E Nat -> E Nat ->{Expr1} E Nat
  nat : Nat ->{Expr1} E Nat

►

type E a = E ('a)

And some interpreters are straightforward:

►

Expr1.eval : '{Expr1} a -> a
Expr1.eval e =
  use Expr1 eval
  handle e()
  with cases
    { a }                                    -> a
    { Expr1.nat n -> k }                     -> eval do k (E do n)
    { Expr1.float n -> k }                   -> eval do k (E do n)
    { Expr1.nat.times (E e1) (E e2) -> k }   ->
      use Nat *
      e1r = e1()
      e2r = e2()
      r = e1r * e2r
      eval do k (E do r)
    { Expr1.float.times (E e1) (E e2) -> k } ->
      use Float *
      e1r = e1()
      e2r = e2()
      r = e1r * e2r
      eval do k (E do r)

Which kinds of interpreters are straightforward? Any interpreter which doesn't care about the structure of the original syntax tree. Notice we don't really care about how the original Expr1 thunk was formed or what its internal structure is. The handler is really just processing a sequence of calls to the operations of the ability.

But not all use cases are like this. What if we want to convert thunks of an ability like this to Json? Now we very much do care about the structure of the syntax tree. Our interpreter isn't trying to produce an evaluated result, we're instead trying to encode the structure of the expression to Json.

This use case is relevant not just for producing JSON. It would also come up if you were (say), writing a DSL in Unison that could compile to CUDA code, or really any sort of code generation task. So what do we do?

📘

While Unison supports serialization of arbitrary values, including functions, and there are some low-level utilities for working with the bytecode tree of an arbitrary serialized form, this probably isn't what you want to do for many domains.

If you're building a DSL in Unison, you don't want to have to write a full code generator from the general purpose Unison programming language with all its features to (say) CUDA or whatever your code generation target.

Applying the "fundamental theorem of software engineering"

There is a jokey aphorism, the "fundamental theorem of software engineering", that all problems in computing can be solved by introducing an extra level of indirection, and we can apply that here.¹

In our interpreters, rather than directly producing a value, we will instead add the value to a Map, and return a key into this Map. Let's have a look at an interpreter that evaluates an Expr2, which uses this strategy:

►

type E2 a = E2 Nat

►

ability Expr2 where
  nat : Nat ->{Expr2} E2 Nat
  float.times : E2 Float -> E2 Float ->{Expr2} E2 Float
  nat.times : E2 Nat -> E2 Nat ->{Expr2} E2 Nat
  float : Float ->{Expr2} E2 Float

►

Expr2.eval : '{Expr2} E2 a -> a
Expr2.eval e =
  use Map put
  use Nat +
  get : Map Nat Any -> Nat -> x
  get env i =
    Map.get i env |> getOrBug ("not found", i) |> unsafeExtract
  go env i e =
    handle e()
    with cases
      { E2 ri } -> get env ri
      { Expr2.nat n -> k } ->
        go (put i (Any n) env) (i + 1) do k (E2 i)
      { Expr2.float n -> k } ->
        go (put i (Any n) env) (i + 1) do k (E2 i)
      { Expr2.nat.times (E2 x) (E2 y) -> k } ->
        use Nat *
        r = get env x * get env y
        go (put i (Any r) env) (i + 1) do k (E2 i)
      { Expr2.float.times (E2 x) (E2 y) -> k } ->
        use Float *
        r = get env x * get env y
        go (put i (Any r) env) (i + 1) do k (E2 i)
  go Map.empty 0 e

So E2 is just a key into the environment Map built up in the handler Expr2.eval. As this Map will accumulate values in it of various types, we'll wrap them in Any and cast on the way out. As long as people aren't manually constructing E2 values, this is perfectly safe. (We might give the E2 constructor a scarier name like UnsafeEnvironmentKey or somesuch.)

Here it is in action:

Expr2.eval do Expr2.nat.times (Expr2.nat 2) (Expr2.nat 3)

Notice that this approach works regardless of the type of value we are producing in our interpreter. So if we want to produce Json, easy peasy, and since Json is already dynamically typed, no need to bother with wrapping things in Any, instead our environment can just be of type env : Map Nat Json.

Here it is working:

toJson do Expr2.nat.times (Expr2.nat 3) (Expr2.nat 2)

Object
  [ ("tag", Text "nat.times")
  , ("arg1", Unparsed "3")
  , ("arg2", Unparsed "2")
  ]

And the code for toJson is much the same as before, just with the different environment map in the handler:

►

toJson : '{Expr2} E2 a -> Json
toJson e =
  use Json text
  use Map put
  use Nat +
  get : Map Nat Json -> Nat -> Json
  get env i = Map.get i env |> getOrBug ("not found", i)
  go env i e =
    handle e()
    with cases
      { E2 ri } -> get env ri
      { Expr2.nat n -> k } ->
        go (put i (Json.nat n) env) (i + 1) do k (E2 i)
      { Expr2.float n -> k } ->
        go (put i (Json.float n) env) (i + 1) do k (E2 i)
      { Expr2.nat.times (E2 x) (E2 y) -> k } ->
        json =
          object
            [ ("tag", text "nat.times")
            , ("arg1", get env x)
            , ("arg2", get env y)
            ]
        go (put i json env) (i + 1) do k (E2 i)
      { Expr2.float.times (E2 x) (E2 y) -> k } ->
        json =
          object
            [ ("tag", text "float.times")
            , ("arg1", get env x)
            , ("arg2", get env y)
            ]
        go (put i json env) (i + 1) do k (E2 i)
  go Map.empty 0 e

Not bad!

🧠

Use a fancier key to get common subexpression elimination

With this general approach, if you key the Map in your interpreter not by a fresh Nat, but by a hash of the expression you're interpreting, you can build interpreters that do common-subexpression elimination and recover sharing of subexpressions.

This is a potentially powerful optimization in many DSLs to avoid repeated work!

Making this more statically typed

One downside with this approach is that the interpreters are now dynamically typed and have some tedious bookkeeping dealing with this environment map. If you goof something up or mix up some indexes, your handler will crash and burn horribly. Can we do better? Sure, how about an ability to handle all this nonsense for us once and for all:

►

ability Env where
  save : a ->{Env} E2 a
  restore : E2 a ->{Env} a

And now look how pretty our eval2 is now:

►

eval2 : '{Expr2} E2 a -> a
eval2 e =
  go e =
    handle e()
    with cases
      { ri }                         -> restore ri
      { Expr2.nat n -> k }           -> go do k (save n)
      { Expr2.float n -> k }         -> go do k (save n)
      { Expr2.nat.times x y -> k }   ->
        use Nat *
        r = restore x * restore y
        go do k (save r)
      { Expr2.float.times x y -> k } ->
        use Float *
        r = restore x * restore y
        go do k (save r)
  Env.run do go e

Likewise, check out our toJson2:

►

toJson2 : '{Expr2} E2 a -> Json
toJson2 e =
  use Json text
  _ = "environment is untyped json"
  saveJ : Json -> E2 x
  saveJ json =
    (E2 n) = save json
    E2 n
  restoreJ : E2 x -> Json
  restoreJ k = restore (match k with E2 n -> E2 n)
  go e =
    handle e()
    with cases
      { ri } -> restoreJ ri
      { Expr2.nat n -> k } -> go do k (saveJ (Json.nat n))
      { Expr2.float n -> k } -> go do k (saveJ (Json.float n))
      { Expr2.nat.times x y -> k } ->
        json =
          object
            [ ("tag", text "nat.times")
            , ("arg1", restoreJ x)
            , ("arg2", restoreJ y)
            ]
        go do k (saveJ json)
      { Expr2.float.times x y -> k } ->
        json =
          object
            [ ("tag", text "float.times")
            , ("arg1", restoreJ x)
            , ("arg2", restoreJ y)
            ]
        go do k (saveJ json)
  Env.run do go e

This isn't too shabby. We're still casting the E2 values in the saveJ and restoreJ helper functions, but this is just because our compilation target, Json, is dynamically typed and we're fine with throwing out type information.

Do we ever really need GADTs?

So far, we've shown how to craft abilities that give us some of the advantages of GADTs. You can write interpreters that convert to Unison functions and data types, and by adding an extra level of indirection in your handlers of these abilities, you can also express tasks like code generation and serialization.

So when do you really need GADTs?

One thing that GADTs support is "interesting pattern matching" on the structure of the data type. For instance, we may want to implement the optimization that anything multiplied by 0 is 0, and have our toJson generator just simplify this in advance.

With proper GADTs, this is as simple as adding a line like this to the interpreter:

Apply (Apply NatTimes 0) x -> Json.nat 0

And in general, you get to deeply inspect the syntax tree for whatever patterns you want to recognize and handle in a special way.

What about with abilities?

toJson3 do Expr2.nat.times (Expr2.nat 0) (Expr2.nat 100)

Unparsed "0"

Looks good, but the implementation isn't great:

►

toJson3 : '{Expr2} E2 a -> Json
toJson3 e =
  use Json text
  _ = "environment is untyped json"
  saveJ : Json -> E2 x
  saveJ json =
    (E2 n) = save json
    E2 n
  restoreJ : E2 x -> Json
  restoreJ k = restore (match k with E2 n -> E2 n)
  go e =
    handle e()
    with cases
      { ri } -> restoreJ ri
      { Expr2.nat n -> k } -> go do k (saveJ (Json.nat n))
      { Expr2.float n -> k } -> go do k (saveJ (Json.float n))
      { Expr2.nat.times x y -> k } ->
        use Json nat
        json =
          match (restoreJ x, restoreJ y) with
            (Unparsed "0", _) -> nat 0
            (_, Unparsed "0") -> nat 0
            (x, y) ->
              object
                [("tag", text "nat.times"), ("arg1", x), ("arg2", y)]
        go do k (saveJ json)
      { Expr2.float.times x y -> k } ->
        json =
          object
            [ ("tag", text "float.times")
            , ("arg1", restoreJ x)
            , ("arg2", restoreJ y)
            ]
        go do k (saveJ json)
  Env.run do go e

Awkward. Notice that we're having to pattern match on the interpreted result of type Json rather than the original syntax tree. For JSON, the pattern is still easy enough to recognize, but for a more complex pattern or a different compilation target, it might be much more difficult compared to just recognizing the pattern in the original syntax tree, which we don't have.

Put another way, abilities only conveniently give us a single level of the syntax tree at a time for pattern matching. So what do you do if you need to do interesting or deep pattern matching as part of an ability interpreter?

I don't have a nice general trick for this, but one technique is you can always propagate information that you need for optimizations up the tree. For example, if you need to know if a subexpression is 0 for some optimization, just have handlers return a (Json, Is0) pair.

What gets awkward about this is that the information you might need could have different shapes for different parts of your interpreter. Having to cram all these bits of info into a single type isn't great.

If you know of a nice alternate approach for dealing with this, I'd be very curious to hear it.

Aside from not being able to use nice multi-level pattern matching syntax in your interpreter, another annoyance is the lack of proper equality constraints that GADTs would provide. This can sometimes lead to needing casts where proper GADTs would just work.

Conclusion

GADTs are useful! We're still planning to add them to Unison, but this post shows how you just might be able to get away without them for your use case.