Haskell

8 readers

1 users here now

**The Haskell programming language community.** Daily news and info about all things Haskell related: practical stuff, theory, types, libraries, jobs, patches, releases, events and conferences and more... ### Links - Get Started with Haskell

founded 1 year ago

Defeating Return Type Polymorphism (philipphagenlocher.de)

submitted 1 year ago by [email protected] to c/[email protected]

12 comments fedilink hide all child comments

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.

you are viewing a single comment's thread
view the rest of the comments

[–] [email protected] 1 points 1 year ago (6 children)

This gives a nice practical motivation for GADTs and existential quantification.

This existentials and GADTs can be converted into a CPS style without type equality constraints

That sounds interesting. I can't easily imagine what that would look like. Do you have an example?

[–] [email protected] 2 points 1 year ago

@jaror @bss03 Maybe I was wrong, but I think you can do Scott encoding of the GADT underneath the standard codensity representation of existentials via CPS. Still need higher-rank types, not "just" parametricity.

I should write up some code to check myself against GHC.

load more comments (5 replies)