I wrote an answer over at Stack Overflow that somehow grew to article length. Here it is, recorded for posterity.

I'll paraphrase the original question as:

What's the difference between the types

`forall a. [a]`

and`[forall a. a]`

, andHow does this relate to existential types?

Well, the short answer to the second question is "It doesn't relate". But there's still a natural flow in discussing both topics.

# Notation

Polymorphic values are essentially functions on types, but Haskell's syntax leaves both type abstraction and type application implicit. To better understand what's going on, we'll use a pidgin syntax of Haskell combined with a typed lambda calculus like System F.

In System F, polymorphism involves explicit type abstractions and type application. For example, the familiar `map`

function would be written as:

`map :: ∀a. ∀b. (a → b) → [a] → [b]`

map = Λa. Λb. λ(f :: a → b). λ(xs :: [a]). case xs of

[] → []

(y:ys) → f y : map @a @b f ys

`map`

is now a function of *four* arguments: types `a`

and `b`

, a function, and a list.

At the term level, we have one new syntactic form: Λ (upper-case lambda). A polymorphic value is a function from types to values, written `Λx. e`

, much as a function from values to values is written `λx. e`

.

At the type level, we have the symbol ∀ ("for all"), corresponding to GHC's `forall`

keyword. A term containing Λ gives rise to a type containing ∀, just as a term containing λ gives rise to a type containing →.

Since we have functions of types, we also need application of types. I use the notation `@a`

(as in GHC Core) to denote application of a type argument. So we might use `map`

like so:

`map @Char @Int ord "xzy"`

Note also that I've provided an explicit type on each λ abstraction. Type inference for System F is, in general, undecidable (Wells, 1999). The restricted form of polymorphism available in vanilla Haskell 98 has decidable inference, but you lose this if you enable certain GHC extensions like `RankNTypes`

.

We don't need annotations on Λ abstractions, because we have only one "kind" of type. In actual Haskell, or a calculus like System Fω, we also have type constructors, and we need a system of kinds to describe how they combine. We'll ignore this issue here.

So a value of polymorphic type is like a function from types to values. The caller of a polymorphic function gets to choose a type argument, and the function must comply.

One last bit of notation: I'll use the syntax

`⊥@t`

to mean an undefined value of type `t`

, similar to Haskell's `undefined`

.

# ∀a. [a]

How, then, would we write a term of type `∀a. [a]`

? We know that types containing ∀ come from terms containing Λ:

`term1 :: ∀a. [a]`

term1 = Λa. ?

Within the body marked `?`

we must provide a term of type `[a]`

. However, we know nothing concrete about `a`

, since it's an argument passed in from the outside. So we can return an empty list

`term1 = Λa. []`

or an undefined value

`term1 = Λa. ⊥@[a]`

or a list containing undefined values only

`term1 = Λa. [⊥@a, ⊥@a]`

but not much else.

To use this value, we apply a type, removing the outer ∀. Let's arbitrarily instantiate `∀a. [a]`

to `[Bool]`

:

`main = print @Int (length @Bool (term1 @Bool))`

```
```

# [∀a. a]

What about `[∀a. a]`

, then? If ∀ signifies a function on types, then `[∀a. a]`

is a list of functions. We can provide as few as we like:

`term2 :: [∀a. a]`

term2 = []

or as many:

`term2 = [f, g, h]`

But what are our choices for `f`

, `g`

, and `h`

?

`f :: ∀a. a`

f = Λa. ?

Now we're well and truly stuck. We have to provide a value of type `a`

, but we know nothing whatsoever about the type `a`

. So our only choice is

`f = Λa. ⊥@a`

So our options for `term2`

look like

`term2 :: [∀a. a]`

term2 = []

term2 = [Λa. ⊥@a]

term2 = [Λa. ⊥@a, Λa. ⊥@a]

etc. And let's not forget

`term2 = ⊥@(∀a. [a])`

Unlike the previous example, our choices for `term2`

are already lists, and we can pass them to `length`

directly. As before, we have to pass the element type to `length`

:

`main = print @Int (length @(∀a. a) term2)`

```
```

# Existential types

So a value of universal (∀) type is a function from types to values. A value of existential (∃) type is a *pair* of a type and a value.

More specifically: A value of type

`∃x. T`

is a pair

`(S, v)`

where S is a type, and where `v :: T`

, assuming you bind the type variable `x`

to `S`

within `T`

.

Here's an existential type signature and a few terms with that type:

`term3 :: ∃a. a`

term3 = (Int, 3)

term3 = (Char, 'x')

term3 = (∀a. a → Int, Λa. λ(x::a). 4)

In other words, we can put any value we like into `∃a. a`

, as long as we pair that value with its type.

The *user* of a value of type `∀a. a`

is in a great position; they can choose any specific type they like, using the type application `@T`

, to obtain a term of type `T`

. The *producer* of a value of type `∀a. a`

is in a terrible position: they must be prepared to produce any type asked for, so (as in the previous section) the only choice is `Λa. ⊥@a`

.

The *user* of a value of type `∃a. a`

is in a terrible position; the value inside is of some unknown specific type, not a flexible polymorphic value. The *producer* of a value of type `∃a. a`

is in a great position; they can stick any value they like into the pair, as we saw above.

So what's a less useless existential? How about values paired with a binary operation:

`type Something = ∃a. (a, a → a → a, a → String)`

term4_a, term4_b :: Something

term4_a = (Int, (1, (+) @Int , show @Int))

term4_b = (String, ("foo", (++) @Char, λ(x::String). x))

Using it:

`triple :: Something → String`

triple = λ(a, (x :: a, f :: a→a→a, out :: a→String)).

out (f (f x x) x)

The result:

`triple term4_a ⇒ "3"`

triple term4_b ⇒ "foofoofoo"

We've packaged up a type and some operations on that type. The user can apply our operations but cannot inspect the concrete value — we can't pattern-match on `x`

within `triple`

, since its type (hence set of constructors) is unknown. This is more than a bit like object-oriented programming.

# Using existentials for real

The direct syntax for existentials using ∃ and type-value pairs would be quite convenient. UHC partially supports this direct syntax. But GHC does not. To introduce existentials in GHC we need to define new "wrapper" types.

Translating the above example:

`{-# LANGUAGE ExistentialQuantification #-}`

data Something = forall a. MkThing a (a -> a -> a) (a -> String)

term_a, term_b :: Something

term_a = MkThing 1 (+) show

term_b = MkThing "foo" (++) id

triple :: Something -> String

triple (MkThing x f out) = out (f (f x x) x)

There's a couple differences from our theoretical treatment. Type application, type abstraction, and type pairs are again implicit. Also, the wrapper is confusingly written with `forall`

rather than `exists`

. This references the fact that we're declaring an *existential* type, but the *data constructor* has *universal* type:

`MkThing :: forall a. a -> (a -> a -> a) -> (a -> String) -> Something`

Often, we use existential quantification to "capture" a type class constraint. We could do something similar here:

`data SomeMonoid = forall a. (Monoid a, Show a) => MkMonoid a`

```
```

# Further reading

For an introduction to the theory, I highly recommend *Types and Programming Languages* by Pierce. For a discussion of existential types in GHC, see the GHC manual and the Haskell wiki.

A small typo : in the ∀a.[a] section, the type application for the first undefined should be on the list type, not the element type :

ReplyDeleteterm1 = Λa. ⊥@[a]

@gasche Fixed. Thanks for catching that!

ReplyDeleteTechnically you should use (/\a. [] @a) :: forall a, [a]. Since the constructors are polymorphic too, so []@a is the nil of type [a].

ReplyDeletein

ReplyDeleteterm4_b = (String, ("foo", (++) @Char, λ(x::String). x))

I think @Char should say @String.

@winterkoninkje: You're right. I'm being less than precise with my treatment of type constructors and polymorphic data, since I wanted to talk only about System F and not Fω. To be honest, I know a lot less about Fω! Maybe I'll review that part of TaPL and post a follow-up.

ReplyDeleteAnonymous: No. (++)'s type is "forall a. [a] -> [a] -> [a]". If you use @String instead of @Char, it will become "[String] -> [String] -> [String]", which is not what you want.

ReplyDeleteShouldn't `term2 = ⊥@(∀a. [a])` in the `[∀a. a]` subsection be `term2 = ⊥@([∀a. a])`?

ReplyDeletehttps://dltutuapp.com/tutuapp-download/ . https://kodi.software/ . https://showbox.run/

ReplyDeleteLooking for opportunities to join Pak Navy? Then ease your tensions as you can find all the latest job opportunities in Pak Navy Jobs here at Latest Jobs In Pak Navy 2020

ReplyDeletehttps://softscracked.com

ReplyDeletePro crack software free download

https://crackedhere.com

ReplyDeleteCrack torrent software is free here

https://approvedcrack.com/

ReplyDeleteCrack torrent software is free here

http://crackswall.com/

ReplyDeleteget all type of paid software

all type of mac windows software here

ReplyDeletehttps://crackedpcgame.com/

https://crackedget.com/

ReplyDeleteFull version crack software is here

https://crackeypc.com/

ReplyDeleteFree downlaod crack software Free

https://vikipc.com/

ReplyDeletePro crack software free download

https://productkeyhere.com/

ReplyDeleteCrack torrent software is free here

https://productkeybox.com/

ReplyDeleteget all type of paid software

https://pcgamesfully.com/

ReplyDeletepc games free download full version.

The ultimate goal of descriptive essay help services is to provide Descriptive Essay Writing Services and descriptive essay services since descriptive essay writing help seekers lack time to complete their custom descriptive essay writing services.

ReplyDeletelAmazin Content

ReplyDeleteWonderful!

ReplyDeleteWonderful!

ReplyDeleteNice Post!

ReplyDeleteNice Post!

ReplyDeletevery nice… i really like your blog…!

ReplyDeleteImpressive！Thanks for the post!

ReplyDeleteAppreciated...

ReplyDeleteMy goodness, how impressive!

ReplyDeleteThank you for getting right to work.

ReplyDeleteSuccessful effort!

ReplyDeleteGood work/Good job!

ReplyDeleteFavorable!

ReplyDeleteThanks for the real post!

ReplyDelete123.hp.com/setup - Visit 123.com.setup to download &a 123.hp.com setup for , Multifunctional InkJet,HP DeskJet, LaserJet, and other printer drivers.

ReplyDeletefix norton not opening windows 10 or norton won't open windows 10, if you need any help from technical person call

ReplyDeleteThis is my blog. Click here.

ReplyDeletebloglovin"

You should be so proud of yourself.!

ReplyDeleteYou're amazing!

ReplyDeleteYou're a true gift to the people in your life.

ReplyDeleteYou're an incredible friend.

ReplyDeleteA good website is useful.

ReplyDeletejoventuthandbolmataro.com/

joventuthandbolmataro.com/

Your positively is infection!

ReplyDeleteYou should be so proud of your self.

ReplyDeleteYou're a true gift to the people in your life.

ReplyDeleteI really appreciate everything that you do.

ReplyDeleteAmazing content

ReplyDeleteAmazing content <3 \

ReplyDeleteInformative content

ReplyDeleteExecellent Work <3

ReplyDeletePerfect content <3

ReplyDeleteWell Work

ReplyDeleteHBSE 10th Syllabus 2021- Haryana Board has released the revised syllabus of the HBSE 10th 2021 exams. Students can check HBSE Syllabus for Class 10 exams on the official website, bseh.org.in. Haryana Board 10th syllabus 2021 is available for all the subjects namely English, Physical Education, Home Science, Mathematics, Science, etc. Students preparing for HBSE 10th 2021 board exams can check subject-wise important topics in HBSE 10th syllabus 2021. Haryana 10th Syllabus 2021-2022 Knowing the HBSE Syllabus for Class 10 helps students reducing their efforts and time in figuring out what to prepare for board exams. Haryana Board of School Education (HBSE) will conduct class 10th board exams from April 22 to May 12, 2021. Students are advised to go through the HBSE 10th syllabus 2021 carefully and make sure that no topic is left unprepared. Read the HBSE 10th syllabus 2021-22 to get the details of subject-wise topics that need to be covered.

ReplyDeleteIf you are looking for GTA 5 iOS, then you have landed on the right page. Here you will get all information about GTA 5 iOS Apk including a tutorial on how to download and install GTA 5 on iOS. GTA 5 mod APK GTA 5 iOS

ReplyDelete

ReplyDeleteاسس اختيار الاثاث المناسب للمنزل

اولا عليك وضع مساحة منزلك فى الحسبان لان على أساسها سيتم تحديد كل تفاصيل منزلك ومحتوياته حيث سيتم تحديد مساحة الاثاث, نوعه فإذا كان منزلك ذو مساحة كبيرة فيمكنك اختيار الاثاث المشغول بتفاصيل كثيرة والاثاث كبير الحجم او ما يسمى بـ “الاثاث الكلاسيك”, ولكن إذا كانت مساحة منزلك محدودة فـ “الاثاث المودرن” والبسيط هو أفضل ما يناسبه إلى جانب اختيار أثاث صغير الحجم لا يشغل مساحات كبيرة

عليك تخيل التصميم الذي ترغب فى اقتنائه ومعرفة التصميمات الحديثة للأثاث عن طريق الانترنت حتى لا يتم تشتيت انتباهك بالتصميمات و أنواع الأثاث التي لا حصر لها

عليك بتحديد القطع الضرورية لمنزلك حتى تتجنب شراء قطع أثاث لست بحاجة لها

عليك بتحديد ميزانيتك وقدرتك المالية لمعرفة ما يمكن أو لا يمكن شرائه وتحديد تفاصيل ذلك فمثلا وضع مقدرة مالية معينة لغرفة النوم حتى لا تنساق وراء أشياء ثانوية لن تكن بنفس أهمية الاثاث الذى قمت بتحديده

التضحية قد تكون إحدى ما يميز تلك المرحلة وخاصة إذا كانت مقدرتك المالية لا تسمح بشراء كل ما ترغب ففي تلك الحالة عليك بأختيار الذي سوف تتأثر أكثر بفقدانه

شركة تركيب اثاث ايكيا بالرياض

تركيب غرف نوم بالرياض

تفصيل طاولات خشب بالرياض

You can protect your files from third party modifications. No one can change the content of your files without your permission. Keep your files safe and secure.https://crackcool.com/iobit-protected-folder-crack/

ReplyDeleteIObit Protected Folder Serial Key is one of the useful software when your computer is connected to multiple users and you want to protect your important files, documents

ReplyDeleteVLC Media Player Crack is magnificent software for greater results of your task. It provides the best features to its users.

ReplyDeleteAlso it has a simple and easy to use interface. I've been using it for a long time and it is the best one indeed.

You can Download it free of cost.

Daemon Tools crack serial number works in conjunction with almost all currently available image formats, plus installation to create physical copies of CD / DVD and Blu-ray images after being trusted

ReplyDeletegood job amazing

ReplyDeletehttps://start-crack.com/winrar-crack/

Nitro Pro Crack

ReplyDelete