This was already featured in the Weekly News a couple of weeks back, but I think maybe it deserves it’s own thread. I’ve tried to explain this approach to some people before, but I think this article does a much better job than I have.

I do think the “Defeating” in the title might be a little bit negative, it’s have preferred something neutral like “When your result type depends on your argument values”, but it’s still something useful to know from retaining your type safety.

This existentials and GADTs can be converted into a CPS style without type equality constraints (usually, with enough work) so that you can start from this description but use it in languages with less sophisticated type systems – as long as they have parametricity – like Haskell 2010.

  • lukewarm@kbin.social
    link
    fedilink
    arrow-up
    1
    ·
    9 months ago

    Well, I guess that I can see the value… Leaving copy-pasting problem aside, you might, for instance, want to have a type for a message with moderately complex envelope and a wide variety of possible payload types. It would be useful to have functions that act on the envelope, and treat payload as something opaque.

    Thanks for the conversation!