Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <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>, (&lambda;<em>x</em>. <em>x</em>, &lambda;<em>x</em>. <em>x</em>)) : &exist; <em>T</em>. (<em>Int</em> &rarr; <em>T</em>) &times; (<em>T</em> &rarr; <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 &Pi;-type (where T1&rarr;T2 = &Pi;(x:T1).T2 and &forall;A.T = &Pi;(A:&ast;).T) and likewise exists and tupling can be generalised to &Sigma;-types (where T1&times;T2 = &Sigma;(x:T1).T2 and &exist;A.T = &Sigma;(A:&ast;).T). Here, the type &ast; is the "type of types".</p></li> </ul>
    singulars
    1. This table or related slice is empty.
    1. POWhat are type quantifiers?
      singulars
      1. PTQuestion
    1. PTAnswer
    1. This table or related slice is empty.
    1. USAndreas Rossberg
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. POWhat are type quantifiers?
      singulars
      1. PTQuestion
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    3. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    1. COSo a value of type `forall T. Q` is a function of type `* -> Q`, and in priciple it can be any such function, except that some languages only allow you to express a certain subset that happens to obey parametricity? And the model that I described in "A possible explanation..." is invalid, or at least not used in type theory? The Π and Σ seem very similar to the forall and exists that I described there, except that they do product & tagged union rather than union & intersection?
      singulars
      1. PO
      1. USJules
    2. COYes, pretty much. In type theory, you usually work with fully explicit proof terms, i.e. all products and sums, whether finite or infinite, come with explicit introduction and elimination forms. That said, people have also looked into notions of union and intersection types without such explicit forms, but those tend to have rather hairy meta-theoretical properties even in the finite case (e.g. type checking often is undecidable).
      singulars
      1. PO
      1. USAndreas Rossberg
    3. COSo just like you can violate parametricity if you can dispatch based on the type passed in (like `f<int>` and `f<T>` above), you can also violate the information hiding of existentials in the same way? For example if you have a package `(T, (a,b))`, you can analyze the first component, and if it is a type you know about you can violate information hiding. For example if you checked whether `T` is an Int, and if it is, you can now read the values returned by `a`?
      singulars
      1. PO
      1. USJules
 

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.

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