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?
[ Parent
| on HN ]
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/