CODEWITHSUNDEEP
haskellexistential-type
typesanitizer
typesanitizer

Reputation: 2775

Existential quantification without data constructors

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?

Upvotes: 1

Views: 90

Answers (1)

typesanitizer
typesanitizer

Reputation: 2775

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.

Upvotes: 4

Related Questions