StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>Let me address your questions separately.</p> <ul> <li><p>Calling forall "a lambda at the type level" is inaccurate for two reasons. First, it is <em>the type of</em> a lambda, not the lambda itself. Second, that lambda lives on the term level, even though it abstracts over types (lambdas on the type level exist as well, they provide what is often called generic types).</p></li> <li><p>Universal quantification does not necessarily imply "same behaviour" for all instantiations. That is a particular property called "parametricity" that may or may not be present. The plain polymorphic lambda calculus is parametric, because you simply cannot express any non-parametric behaviour. But if you add constructs like typecase (a.k.a. intensional type analysis) or checked casts as a weaker form of that, then you loose parametricity. Parametricity implies nice properties, e.g. it allows a language to be implemented without any runtime representation of types. And it induces very strong reasoning principles, see e.g. Wadler's paper "Theorems for free!". But it's a trade-off, sometimes you want dispatch on types.</p></li> <li><p>Existential types essentially denote pairs of a type (the so-called witness) and a term, sometimes called <em>packages</em>. One common way to view these is as implementation of abstract data types. Here is a simple example:</p> <p>pack (<em>Int</em>, (λ<em>x</em>. <em>x</em>, λ<em>x</em>. <em>x</em>)) : ∃ <em>T</em>. (<em>Int</em> → <em>T</em>) × (<em>T</em> → <em>Int</em>)</p> <p>This is a simple ADT whose representation is <em>Int</em> and that only provides two operations (as a nested tuple), for converting ints in and out of the abstract type <em>T</em>. This is the basis of type theories for modules, for example.</p></li> <li><p>In summary, universal quantification provides client-side data abstraction, while existential types dually provides implementor-side data abstraction.</p></li> <li><p>As an additional remark, in the so-called <em>lambda cube</em>, forall and arrow are generalised to the unified notion of Π-type (where T1→T2 = Π(x:T1).T2 and ∀A.T = Π(A:&ast;).T) and likewise exists and tupling can be generalised to Σ-types (where T1×T2 = Σ(x:T1).T2 and ∃A.T = Σ(A:&ast;).T). Here, the type &ast; is the "type of types".</p></li> </ul>

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