Re:Clojure at Netflix (2013) [slides]
by CMCDragonkai on Thursday November 01, 2018 @12:21AM
(#18351436)
I found your explanation of the relationship between an existentially quantified type and rank 2 polymorphism to be quite illuminating. Do you have any ideas why Haskell didnt have the direct way to express existential quantification in the type signature? Is it a technical limitation or something else?
Re:Clojure at Netflix (2013) [slides]
by matt-noonan on Thursday November 01, 2018 @05:49PM
(#18358803)
I'm not sure about the history. It looks like UHC supported existential types at some point, but I'm not sure how that would interact with what I am presuming is a more sophisticated system in GHC Haskell.
This post had some interesting tidbits about technical challenges, but I didn't fully grasp everything on first read: http://blog.ezyang.com/2016/04/hindley-milner-with-top-level...
I really like tome's observation in the other comment: universally-quantified types have a direct encoding in System F as type abstractions, but there is no such direct encoding for existentially-quantified types.
I don't have a good answer but I did write something about this once http://h2.jaguarpaw.co.uk/posts/exists/
I realize this is just one example, but you might be interested to know that I've done some work making this kind of invariant enforceable via static types (though in practice, you need a combination of features that aren't found in many mainstream language besides Haskell afaik).
See the README here for motivation and some examples (in Haskell, but hopefully the idea is still clear): https://github.com/matt-noonan/justified-containers
Or the tutorial module here: https://hackage.haskell.org/package/justified-containers-0.3...
Or this paper, if you really want to go off the deep end: http://kataskeue.com/gdp.pdf