Existential quantification without data constructors

Question

It is easy to get existential quantification by packing dictionaries in data constructors.

{-# LANGUAGE GADTs #-}

data S where
  MkS :: Show a => a -> S

f :: Int -> S
f x = case x of
  0 -> MkS 0
  _ -> MkS "non-zero"

The relevant section in the GHC guide explicitly talks about "Existentially quantified data constructors". Is it possible to write the same code but without introducing extra data types and constructors, i.e., something with a signature like

f :: Int -> (exists a. Show a => a)
f x = case x of
  0 -> 0
  _ -> "non-zero"

If not, is there a documented reason for why this limitation exists? Avoiding adding a new quantifier?

(exists a. Show a => a) can always be rewritten as something like forall c. Show b => (forall a. Show a => a -> c) -> b -> c. This is similar to the connection in logic between existential quantification and universal quantification. — Colin Barrett
@ColinBarrett Did you really mean the b stuff to be there, and not just, say, forall c. (forall a. Show a => a -> c) -> c? — Daniel Wagner

typesanitizer typesanitizer · Accepted Answer · 2019-03-13T22:23:49

Borrowing from Colin's comment and looking at this answer, it is possible to write a CPS-ed version of the same code without an exists quantifier.

f' :: Int -> ((forall a. Show a => a -> r) -> r)
f' x = case x of
  0 -> \k -> k 0
  _ -> \k -> k "non-zero"

While this is not ideal, it certainly solves the problem without introducing extra data types.

Existential quantification without data constructors

1 Answers