StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
primarykey
Id
13654649
data
AcceptedAnswerId
0
AnswerCount
0
ClosedDate
CommentCount
1
CommunityOwnedDate
CreationDate
2012-11-30T23:27:53.280
FavoriteCount
0
LastActivityDate
2013-06-10T13:41:46.410
LastEditDate
2013-06-10T13:41:46.410
LastEditorUserId
700253
OwnerUserId
700253
ParentId
13653532
PostTypeId
2
Score
24
ViewCount
0
LastEditorDisplayName
text
Body
It turns out that existential types are just a special case of Σ-types (sigma types). What are they? <h2>Sigma types</h2> Just as Π-types (pi types) generalise our ordinary function types, allowing the resulting type to depend on the value of its argument, Σ-types generalise pairs, allowing the type of second component to depend on the value of the first one. In a made-up Haskell-like syntax, Σ-type would look like this: <pre><code>data Sigma (a :: *) (b :: a -> *) = SigmaIntro { fst :: a , snd :: b fst } -- special case is a non-dependent pair type Pair a b = Sigma a (\_ -> b) </code></pre> Assuming <code>* :: *</code> (i.e. the inconsistent <code>Set : Set</code>), we can define <code>exists a. a</code> as: <pre><code>Sigma * (\a -> a) </code></pre> The first component is a type and the second one is a value of that type. Some examples: <pre><code>foo, bar :: Sigma * (\a -> a) foo = SigmaIntro Int 4 bar = SigmaIntro Char 'a' </code></pre> <code>exists a. a</code> is fairly useless - we have no idea what type is inside, so the only operations that can work with it are type-agnostic functions such as <code>id</code> or <code>const</code>. Let's extend it to <code>exists a. F a</code> or even <code>exists a. Show a => F a</code>. Given <code>F :: * -> *</code>, the first case is: <pre><code>Sigma * F -- or Sigma * (\a -> F a) </code></pre> The second one is a bit trickier. We cannot just take a <code>Show a</code> type class instance and put it somewhere inside. However, if we are given a <code>Show a</code> dictionary (of type <code>ShowDictionary a</code>), we can pack it with the actual value: <pre><code>Sigma * (\a -> (ShowDictionary a, F a)) -- inside is a pair of "F a" and "Show a" dictionary </code></pre> This is a bit inconvenient to work with and assumes that we have a <code>Show</code> dictionary around, but it works. Packing the dictionary along is actually what GHC does when compiling existential types, so we could define a shortcut to have it more convenient, but that's another story. As we will learn soon enough, the encoding doesn't actually suffer from this problem. <hr> Digression: thanks to constraint kinds, it's possible to reify the type class into concrete data type. First, we need some language pragmas and one import: <pre><code>{-# LANGUAGE ConstraintKinds, GADTs, KindSignatures #-} import GHC.Exts -- for Constraint </code></pre> GADTs already give us the option to pack a type class along with the constructor, for example: <pre><code>data BST a where Nil :: BST a Node :: Ord a => a -> BST a -> BST a -> BST a </code></pre> However, we can go one step further: <pre><code>data Dict :: Constraint -> * where D :: ctx => Dict ctx </code></pre> It works much like the <code>BST</code> example above: pattern matching on <code>D :: Dict ctx</code> gives us access to the whole context <code>ctx</code>: <pre><code>show' :: Dict (Show a) -> a -> String show' D = show (.+) :: Dict (Num a) -> a -> a -> a (.+) D = (+) </code></pre> <hr> We also get quite natural generalisation for existential types that quantify over more type variables, such as <code>exists a b. F a b</code>. <pre><code>Sigma * (\a -> Sigma * (\b -> F a b)) -- or we could use Sigma just once Sigma (*, *) (\(a, b) -> F a b) -- though this looks a bit strange </code></pre> <h2>The encoding</h2> Now, the question is: can we encode Σ-types with just Π-types? If yes, then the existential type encoding is just a special case. In all glory, I present you the actual encoding: <pre><code>newtype SigmaEncoded (a :: *) (b :: a -> *) = SigmaEncoded (forall r. ((x :: a) -> b x -> r) -> r) </code></pre> There are some interesting parallels. Since dependent pairs represent existential quantification and from classical logic we know that: <pre><code>(∃x)R(x) ⇔ ¬(∀x)¬R(x) ⇔ (∀x)(R(x) → ⊥) → ⊥ </code></pre> <code>forall r. r</code> is almost <code>⊥</code>, so with a bit of rewriting we get: <pre><code>(∀x)(R(x) → r) → r </code></pre> And finally, representing universal quantification as a dependent function: <pre><code>forall r. ((x :: a) -> R x -> r) -> r </code></pre> Also, let's take a look at the type of Church-encoded pairs. We get a very similar looking type: <pre><code>Pair a b ~ forall r. (a -> b -> r) -> r </code></pre> We just have to express the fact that <code>b</code> may depend on the value of <code>a</code>, which we can do by using dependent function. And again, we get the same type. The corresponding encoding/decoding functions are: <pre><code>encode :: Sigma a b -> SigmaEncoded a b encode (SigmaIntro a b) = SigmaEncoded (\f -> f a b) decode :: SigmaEncoded a b -> Sigma a b decode (SigmaEncoded f) = f SigmaIntro -- recall that SigmaIntro is a constructor </code></pre> The special case actually simplifies things enough that it becomes expressible in Haskell, let's take a look: <pre><code>newtype ExistsEncoded (F :: * -> *) = ExistsEncoded (forall r. ((x :: *) -> (ShowDictionary x, F x) -> r) -> r) -- simplify a bit = ExistsEncoded (forall r. (forall x. (ShowDictionary x, F x) -> r) -> r) -- curry (ShowDictionary x, F x) -> r = ExistsEncoded (forall r. (forall x. ShowDictionary x -> F x -> r) -> r) -- and use the actual type class = ExistsEncoded (forall r. (forall x. Show x => F x -> r) -> r) </code></pre> Note that we can view <code>f :: (x :: *) -> x -> x</code> as <code>f :: forall x. x -> x</code>. That is, a function with extra <code>*</code> argument behaves as a polymorphic function. And some examples: <pre><code>showEx :: ExistsEncoded [] -> String showEx (ExistsEncoded f) = f show someList :: ExistsEncoded [] someList = ExistsEncoded $ \f -> f [1] showEx someList == "[1]" </code></pre> Notice that <code>someList</code> is actually constructed via <code>encode</code>, but we dropped the <code>a</code> argument. That's because Haskell will infer what <code>x</code> in the <code>forall x.</code> part you actually mean. <h2>From Π to Σ?</h2> Strangely enough (although out of the scope of this question), you can encode Π-types via Σ-types and regular function types: <pre><code>newtype PiEncoded (a :: *) (b :: a -> *) = PiEncoded (forall r. Sigma a (\x -> b x -> r) -> r) -- \x -> is lambda introduction, b x -> r is a function type -- a bit confusing, I know encode :: ((x :: a) -> b x) -> PiEncoded a b encode f = PiEncoded $ \sigma -> case sigma of SigmaIntro a bToR -> bToR (f a) decode :: PiEncoded a b -> (x :: a) -> b x decode (PiEncoded f) x = f (SigmaIntro x (\b -> b)) </code></pre>
Tags
Title
singulars
PostAcceptedAnswerId
1. This table or related slice is empty.
PostParentId
1. POHow to express existential types using higher rank (rank-N) type polymorphism?
 singulars
 PostTypePostTypeId
 PTQuestion
PostTypePostTypeId
1. PTAnswer
UserLastEditorUserId
1. USVitus
UserOwnerUserId
1. USVitus
plurals
PostLinksPostIdRelatedPostId
1. This table or related slice is empty.
PostLinksRelatedPostIdPostId
1. This table or related slice is empty.
PostsAcceptedAnswerId
1. POHow to express existential types using higher rank (rank-N) type polymorphism?
 singulars
 PostTypePostTypeId
 PTQuestion
PostsParentIdCreationDate
1. This table or related slice is empty.
VotesPostIdCreationDate
1. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
2. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
3. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
CommentsPostId
1. This table or related slice is empty.

Querying!

Guidance

A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.