2
$\begingroup$

ML-style languages have a concept of "extensible" or "open" sum types, where variants can be declared at any point, and there's not a fixed number of constructors for the type. They're usually used to model exceptions and handling, where users can declare their own exception types.

I'm wondering, is there a way that we can encode an extensible sum type using dependent types (lacking a primitive for extensible sums?) This seems like the sort of thing we could get away with when we mix types and terms, but I haven't been able to find any references.

Thanks!

$\endgroup$
  • $\begingroup$ I wonder if this is indeed possible... if you have pattern matching on extensible sums then this is sufficient to encode something akin to nominal type theory: the generation of fresh variants are an effect after all. $\endgroup$ – Daniel Gratzer Nov 20 '19 at 16:06
  • $\begingroup$ Do you need them to have reasonable run-time behavior? You could encode "extensible" Sums similar to Hlists (wiki.haskell.org/Heterogenous_collections) in non-dependent type theories. If you went with an encoding like that dependent types would make your life easier. $\endgroup$ – user833970 Nov 22 '19 at 21:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.