4 ms·
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 wh
by CMCDragonkai 8y ago
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?
- tome 8y agoI don't have a good answer but I did write something about this once http://h2.jaguarpaw.co.uk/posts/exists/ http://h2.jaguarpaw.co.uk/posts/exists/
- matt-noonan 8y agoI'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-existentials/ 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.