Databases
StackOverflow2013
Postsdbo
POWhat are type quantifiers?
 

Note that there are some explanatory texts on larger screens.

plurals
  1. POWhat are type quantifiers?
    primarykey
    data
    text
    <p>Many statically typed languages have parametric polymorphism. For example in C# one can define:</p> <pre><code>T Foo&lt;T&gt;(T x){ return x; } </code></pre> <p>In a call site you can do:</p> <pre><code>int y = Foo&lt;int&gt;(3); </code></pre> <p>These types are also sometimes written like this:</p> <pre><code>Foo :: forall T. T -&gt; T </code></pre> <p>I have heard people say "forall is like lambda-abstraction at the type level". So Foo is a function that takes a type (for example int), and produces a value (for example a function of type int -> int). Many languages infer the type parameter, so that you can write <code>Foo(3)</code> instead of <code>Foo&lt;int&gt;(3)</code>.</p> <p>Suppose we have an object <code>f</code> of type <code>forall T. T -&gt; T</code>. What we can do with this object is first pass it a type <code>Q</code> by writing <code>f&lt;Q&gt;</code>. Then we get back a value with type <code>Q -&gt; Q</code>. However, certain <code>f</code>'s are invalid. For example this <code>f</code>:</p> <pre><code>f&lt;int&gt; = (x =&gt; x+1) f&lt;T&gt; = (x =&gt; x) </code></pre> <p>So if we "call" <code>f&lt;int&gt;</code> then we get back a value with type <code>int -&gt; int</code>, and in general if we "call" <code>f&lt;Q&gt;</code> then we get back a value with type <code>Q -&gt; Q</code>, so that's good. However, it is generally understood that this <code>f</code> is not a valid thing of type <code>forall T. T -&gt; T</code>, because it does something <em>different</em> depending on which type you pass it. The idea of forall is that this is explicitly <em>not</em> allowed. Also, if forall is lambda for the type level, then what is exists? (i.e. existential quantification). For these reasons it seems that forall and exists are not really "lambda at the type level". But then what are they? I realize this question is rather vague, but can somebody clear this up for me?</p> <hr> <blockquote> <blockquote> <blockquote> <p>A possible explanation is the following:</p> <p>If we look at logic, quantifiers and lambda are two different things. An example of a quantified expression is:</p> <pre><code>forall n in Integers: P(n) </code></pre> <p>So there are two parts to forall: a set to quantify over (e.g. Integers), and a predicate (e.g. P). Forall can be viewed as a higher order function:</p> <pre><code>forall n in Integers: P(n) == forall(Integers,P) </code></pre> <p>With type:</p> <pre><code>forall :: Set&lt;T&gt; -&gt; (T -&gt; bool) -&gt; bool </code></pre> <p>Exists has the same type. Forall is like an infinite conjunction, where S[n] is the n-th elemen to of the set S:</p> <pre><code>forall(S,P) = P(S[0]) ∧ P(S[1]) ∧ P(S[2]) ... </code></pre> <p>Exists is like an infinite disjunction:</p> <pre><code>exists(S,P) = P(S[0]) ∨ P(S[1]) ∨ P(S[2]) ... </code></pre> <p>If we do an analogy with types, we could say that the type analogue of ∧ is computing the intersection type ∩, and the type analogue of ∨ computing the union type ∪. We could then define forall and exists on types as follows:</p> <pre><code>forall(S,P) = P(S[0]) ∩ P(S[1]) ∩ P(S[2]) ... exists(S,P) = P(S[0]) ∪ P(S[1]) ∪ P(S[2]) ... </code></pre> <p>So forall is an infinite intersection, and exists is an infinite union. Their types would be:</p> <pre><code>forall, exists :: Set&lt;T&gt; -&gt; (T -&gt; Type) -&gt; Type </code></pre> <p>For example the type of the polymorphic identity function. Here <code>Types</code> is the set of all types, and <code>-&gt;</code> is the type constructor for functions and <code>=&gt;</code> is lambda abstraction:</p> <pre><code>forall(Types, t =&gt; (t -&gt; t)) </code></pre> <p>Now a thing of type <code>forall T:Type. T -&gt; T</code> is a <em>value</em>, not a function from types to values. It is a value whose type is the intersection of all types T -> T where T ranges over all types. When we <em>use</em> such a value, we do not have to apply it to a type. Instead, we use a subtype judgement:</p> <pre><code>id :: forall T:Type. T -&gt; T id = (x =&gt; x) id2 = id :: int -&gt; int </code></pre> <p>This downcasts <code>id</code> to have type <code>int -&gt; int</code>. This is valid because <code>int -&gt; int</code> also appears in the infinite intersection.</p> <p>This works out nicely I think, and it clearly explains what forall is and how it is different from lambda, but this model is incompatible with what I have seen in languages like ML, F#, C#, etc. For example in F# you do <code>id&lt;int&gt;</code> to get the identity function on ints, which does not make sense in this model: id is a function on values, not a function on types that returns a function on values.</p> </blockquote> </blockquote> </blockquote> <hr> <p>Can somebody with knowledge of type theory explain what exactly are forall and exists? And to what extent is it true that "forall is lambda at the type level"?</p>
    singulars
    1. PO
      singulars
      1. PTAnswer
    1. This table or related slice is empty.
    1. PTQuestion
    1. USJules
    1. USJules
    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. PO
      singulars
      1. PTAnswer
    2. PO
      singulars
      1. PTAnswer
    3. PO
      singulars
      1. PTAnswer
    1. VO
      singulars
      1. POWhat are type quantifiers?
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. POWhat are type quantifiers?
      1. USMarcin
      1. VTFavorite
    3. VO
      singulars
      1. POWhat are type quantifiers?
      1. This table or related slice is empty.
      1. VTUpMod
    1. COIf you are into this kind of stuff, you should be *very* interested in [Types and Programming Languages](http://www.cis.upenn.edu/~bcpierce/tapl/).
      singulars
      1. POWhat are type quantifiers?
      1. USDan Burton
 

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