Motivation for not having existential types and GADTs in Daml?

Questions
1

I’m curious to understand more the history and reasoning behind not having existential types and GADTs in Daml. Is this due to the challenges of serializing and deserializing such types?

2 Likes
2

There are two related questions here:

  1. Why is it not possible to use those features at all?
  2. Why are those types not serializable?

For 1, I don’t think there is a fundamental reason. It’s mainly a question of complexity. We only get Haskell features “for free” if we can compile them away (the classic example being syntax sugar). Both GADTs and Existentials (GADTs are implemented on top of existentials in Haskell) do not fall into that category and would need very significant changes in our intermediate language Daml-LF and add a lot of complexity. So far it didn’t seem like that complexity is worth the benefits but we continue evaluating that.

For 2, the situation is a bit different. Tooling like the Java and TypeScript codegen map the serializable fragment of Daml-LF data types to the type system of the respective language. For that to be feasible, the type system has to be simple that you can map it to those languages somewhat faithfully. The more complex features you add the harder it becomes. E.g., Java definitely doesn’t have GADTs or existentials the same way Haskell has. You can probably represent them in some way but it gets a bit ugly.
For existentials there is also the complexity that often you don’t just want an existential type parameter but you want to constraint it via a typeclass constraint. That would require serializing that typeclass dictionary which results in function types being serializable which is a large can of worms.

3 Likes
3

Thanks Moritz. This definitely helps me understand how difficult it would be to implement!

1 Like