Closed dylan-thinnes closed 3 years ago
Haha no problem - you can think of existential quantification roughly as a way of deferring the actual passing in of an argument until later, by carrying around the forall with you, i.e.
isEmpty :: forall a. [a] -> Bool
isEmpty [] = True
isEmpty _ = False
For this definition of isEmpty, you can pass it a variable end in essence "erase" the a
type, so
isEmpty [1,2,3] => False :: Bool
isEmpty "" => True :: Bool
in a sense the program is magical (though for us Haskellers it's not actually magical, we're used to this behaviour) - it hides the a
type from any future function which consumes the resulting Bool
. The isEmpty
function kills the a
type so that no future consumers need to be polymorphic in a
, because we've built a function proving we can always reduce it to a Bool
.
ExistentialQuantification lets you defer that, by saying "I have a value of type a
, and a function that consumes it, but for now we're not going to erase it." Then, when you destructure the a
back out, because it could be any type, you can only manipulate it using its handler, because that's the only function that has a proof of being a valid handler.
Thus, when I see ExistentialQuantification turned on, there's a chance it's just being used to defer a function application for no reason, like it was in this case.
What it says on the tin, really. I didn't check comments / haddocks - maybe some of them need amending?