title: What does "exists" mean in Haskell type system?
body: <p>I'm struggling to understand the <code>exists</code> keyword in relation to Haskell type system. As far as I know, there is no such keyword in Haskell by default, but:</p>
  
  <ul>
  <li>There are <a href="http://hackage.haskell.org/trac/haskell-prime/wiki/ExistentialQuantification" rel="nofollow noreferrer">extensions</a> which add them, in declarations like these <code>data Accum a = exists s. MkAccum s (a -&gt; s -&gt; s) (s -&gt; a)</code></li>
  <li>I've seen a paper about them, and (if I recall correctly) it stated that <code>exists</code> keyword is unnecessary for type system since it can be generalized by <code>forall</code></li>
  </ul>
  
  <p>But I can't even understand what <code>exists</code> means.</p>
  
  <p>When I say, <code>forall a . a -&gt; Int</code>, it means (in my understanding, the incorrect one, I guess) "for every (type) <code>a</code>, there is a function of a type <code>a -&gt; Int</code>":</p>
  
  <pre><code>myF1 :: forall a . a -&gt; Int
  myF1 _ = 123
  -- okay, that function (`a -&gt; Int`) does exist for any `a`
  -- because we have just defined it
  </code></pre>
  
  <p>When I say <code>exists a . a -&gt; Int</code>, what can it even mean? "There is at least one type <code>a</code> for which there is a function of a type <code>a -&gt; Int</code>"? Why one would write a statement like that? What the purpose? Semantics? Compiler behavior?</p>
  
  <pre><code>myF2 :: exists a . a -&gt; Int
  myF2 _ = 123
  -- okay, there is at least one type `a` for which there is such function
  -- because, in fact, we have just defined it for any type
  -- and there is at least one type...
  -- so these two lines are equivalent to the two lines above
  </code></pre>
  
  <p>Please note it's not intended to be a real code which can compile, just an example of what I'm imagining then I hear about these quantifiers.</p>
  
  <hr>
  
  <p>P.S. I'm not exactly a total newbie in Haskell (maybe like a second grader), but my Math foundations of these things are lacking.</p>