StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>I found an anwer in <a href="http://www.paultaylor.eu/stable/Proofs+Types.html" rel="noreferrer">Proofs and Types by Jean-Yves Girard, Yves Lafont and Paul Taylor</a>.</p> <p>Imagine we have some one-argument type <code>t :: * -> *</code> and construct an existential type that holds <code>t a</code> for some <code>a</code>: <code>exists a. t a</code>. What can we do with such a type? In order to compute something out of it we need a function that can accept <code>t a</code> for arbitrary <code>a</code>, that means a function of type <code>forall a. t a -> b</code>. Knowing this, we can encode an existential type simply as a function that takes functions of type <code>forall a. t a -> b</code>, supplies the existential value to them and returns the result <code>b</code>:</p> <pre><code>{-# LANGUAGE RankNTypes #-} newtype Exists t = Exists (forall b. (forall a. t a -> b) -> b) </code></pre> <p>Creating an existential value is now easy:</p> <pre><code>exists :: t a -> Exists t exists x = Exists (\f -> f x) </code></pre> <p>And if we want to unpack the existential value, we just apply its content to a function that produces the result:</p> <pre><code>unexists :: (forall a. t a -> b) -> Exists t -> b unexists f (Exists e) = e f </code></pre> <p>However, purely existential types are of very little use. We cannot do anything reasonable with a value we know nothing about. More often we need an existential type with a type class constraint. The procedure is just the same, we just add a type class constraint for <code>a</code>. For example:</p> <pre><code>newtype ExistsShow t = ExistsShow (forall b. (forall a. Show a => t a -> b) -> b) existsShow :: Show a => t a -> ExistsShow t existsShow x = ExistsShow (\f -> f x) unexistsShow :: (forall a. Show a => t a -> b) -> ExistsShow t -> b unexistsShow f (ExistsShow e) = e f </code></pre> <p>Note: Using existential quantification in functional programs is often considered a <a href="https://en.wikipedia.org/wiki/Code_smell" rel="noreferrer">code-smell</a>. It can indicate that we haven't liberated ourselves from OO thinking.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload