4 ms·

That blog post was a nice read, thanks! I realize this is just one example, but you might be interested to know that I've done some work making this kind of in

That blog post was a nice read, thanks! 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 https://github.com/matt-noonan/justified-containers Or the tutorial module here: https://hackage.haskell.org/package/justified-containers-0.3.0.0/docs/Data-Map-Justified-Tutorial.html 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 http://kataskeue.com/gdp.pdf

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 ago
  I 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 ago
  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-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.

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 ago
I 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 ago
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-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.