Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>A few remarks to complement the two already-excellent answers.</p> <p>First, one cannot say that <code>forall</code> is lambda at the type-level because there already is a notion of lambda at the type level, and it is different from <code>forall</code>. It appears in system F_omega, an extension of System F with type-level computation, that is useful to explain ML modules systems for example (<a href="http://www.mpi-sws.org/~rossberg/papers/Rossberg,%20Russo,%20Dreyer%20-%20F-ing%20Modules.pdf" rel="nofollow">F-ing modules</a>, by Andreas Rossberg, Claudio Russo and Derek Dreyer, 2010).</p> <p>In (a syntax for) System F_omega you can write for example:</p> <pre><code>type prod = lambda (a : *). lambda (b : *). forall (c : *). (a -&gt; b -&gt; c) -&gt; c </code></pre> <p>This is a definition of the "type constructor" <code>prod</code>, such as <code>prod a b</code> is the type of the church-encoding of the product type <code>(a, b)</code>. If there is computation at the type level, then you need to control it if you want to ensure termination of type-checking (otherwise you could define the type <code>(lambda t. t t) (lambda t. t t)</code>. This is done by using a "type system at the type level", or a <em>kind</em> system. <code>prod</code> would be of kind <code>* -&gt; * -&gt; *</code>. Only the types at kind <code>*</code> can be inhabited by values, types at higher-kind can only be applied at the type level. <code>lambda (c : k) . ....</code> is a type-level abstraction that cannot be the type of a value, and may live at any kind of the form <code>k -&gt; ...</code>, while <code>forall (c : k) . ....</code> classify values that are polymorphic in some type <code>c : k</code> and is necessarily of ground kind <code>*</code>.</p> <p>Second, there is an important difference between the <code>forall</code> of System F and the Pi-types of Martin-Löf type theory. In System F, polymorphic values <em>do the same thing on all types</em>. As a first approximation, you could say that a value of type <code>forall a . a -&gt; a</code> will (implicitly) take a type <code>t</code> as input and return a value of type <code>t -&gt; t</code>. But that suggest that there may be some computation happening in the process, which is not the case. Morally, when you instantiate a value of type <code>forall a. a -&gt; a</code> into a value of type <code>t -&gt; t</code>, the value does <em>not</em> change. There are three (related) ways to think about it:</p> <ul> <li><p>System F quantification has type erasure, you can forget about the types and you will still know what the dynamic semantic of the program is. When we use ML type inference to leave the polymorphism abstraction and instantiation implicit in our programs, we don't really let the inference engine "fill holes in our program", if you think of "program" as the dynamic object that will be run and compute.</p></li> <li><p>A <code>forall a . foo</code> is not a something that "produces an instance of <code>foo</code> for each type <code>a</code>, but a single type <code>foo</code> that is "generic in an unknown type <code>a</code>".</p></li> <li><p>You can explain universal quantification as an infinite conjunction, but there is an <em>uniformity</em> condition that all conjuncts have the same structure, and in particular that their proofs are all alike.</p></li> </ul> <p>By contrast, Pi-types in Martin-Löf type theory are really more like function types that take something and return something. That's one of the reason why they can easily be used not only to depend on <em>types</em>, but also to depend on <em>terms</em> (dependent types).</p> <p>This has very important implications once you're concerned about the soundness of those formal theories. System F is <em>impredicative</em> (a forall-quantified type quantifies on all types, itself included), and the reason why it's still sound is this uniformity of universal quantification. While introducing non-parametric constructs is reasonable from a programmer's point of view (and we can still reason about parametricity in an generally-non-parametric language), it very quickly destroys the logical consistency of the underlying static reasoning system. Martin-Löf <em>predicative</em> theory is much simpler to prove correct and to extend in correct way.</p> <p>For a high-level description of this uniformity/genericity aspect of System F, see Fruchart and Longo's 97 article <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.1911" rel="nofollow">Carnap's remarks on Impredicative Definitions and the Genericity Theorem</a>. For a more technical study of System F failure in presence of non-parametric constructs, see <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.5163" rel="nofollow">Parametricity and variants of Girard's J operator</a> by Robert Harper and John Mitchell (1999). Finally, for a description, from a language design point of view, on how to abandon <em>global</em> parametricity to introduce non-parametric constructs but still be able to locally discuss parametricity, see <a href="http://www.mpi-sws.org/~rossberg/papers/Neis,%20Dreyer,%20Rossberg%20-%20Non-Parametric%20Parametricity%20%5BJFP%5D.pdf" rel="nofollow">Non-Parametric Parametricity</a> by George Neis, Derek Dreyer and Andreas Rossberg, 2011. </p> <p>This discussion of the difference between "computational abstraction" and "uniform abstract" has been revived by the large amount of work on representing variable binders. A binding construction feels like an abstraction (and can be modeled by a lambda-abstraction in HOAS style) but has an uniform structure that makes it rather like a data skeleton than a family of results. This has been much discussed, for example in the LF community, "representational arrows" in Twelf, "positive arrows" in Licata&amp;Harper's work, etc.</p> <p>Recently there have been several people working on the related notion of "irrelevance" (lambda-abstractions where the result "does not depend" on the argument), but it's still not totally clear how closely this is related to parametric polymorphism. One example is the work of Nathan Mishra-Linger with Tim Sheard (eg. <a href="http://web.cecs.pdx.edu/~sheard/papers/FossacsErasure08.pdf" rel="nofollow">Erasure and Polymorphism in Pure Type Systems</a>).</p>
    singulars
    1. This table or related slice is empty.
    1. POWhat are type quantifiers?
      singulars
      1. PTQuestion
    1. PTAnswer
    1. USgasche
    1. USgasche
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    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. COYes! That is exactly what I mean. In ML a type `forall a. a -> a` means that there is a *single* value that has both type `int -> int`, `string -> string`, etc. That is what made me confused and still feels a little dirty about modeling that as a function that takes a type and returns the same value every time. The only thing that guarantees that it's the same value is the absence of certain features from ML. Having an explicit way of saying "this *single* value has *all* the types `a -> a`" seems cleaner (e.g. the intersection of `a -> a` where `a` ranges over types). But this doesn't exist?
      singulars
      1. PO
      1. USJules
    2. CO"The only thing that guarantees that it's the same value is the absence of certain features from ML." I don't think this is an accurate description, or rather I don't think that this is an *useful* description. You can always lose a good property by messing things up, it does not mean that the property is not well-justified. System F is at the edge of inconsistency because it is very powerful logically and computationally, so it is to be expected that small changes break the system.
      singulars
      1. PO
      1. USgasche
    3. COYou have the impression that System F parametricity is not robust because you have a syntactic point of view. If you instead studied the system as a Curry-style system complemented with type derivations -- untyped terms plus proofs of well-typing -- the type-erasability property would jump in your face. Similarly if you defined typings semantically, using for example a logical relation model (see for example neelk's [Adding Equations to System F Types](www.cs.cmu.edu/~neelk/esop12.pdf)), you would define `forall` as an intersection. Yet it's the exact same language you would be talking about.
      singulars
      1. PO
      1. USgasche
 

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