StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<blockquote> <p>if forall is lambda ..., then what is exists</p> </blockquote> <p>Why, tuple of course!</p> <p>In <a href="http://en.wikipedia.org/wiki/Intuitionistic_type_theory" rel="noreferrer">Martin-Löf type theory</a> you have Π types, corresponding to functions/universal quantification and Σ-types, corresponding to tuples/existential quantification.</p> <p>Their types are very similar to what you have proposed (I am using <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php" rel="noreferrer">Agda</a> notation here):</p> <pre><code>Π : (A : Set) -> (A -> Set) -> Set Σ : (A : Set) -> (A -> Set) -> Set </code></pre> <p>Indeed, Π is an infinite product and Σ is infinite sum. Note that they are not "intersection" and "union" though, as you proposed because you can't do that without additionally defining where the types intersect. (which values of one type correspond to which values of the other type)</p> <p>From these two type constructors you can have all of normal, polymorphic and dependent functions, normal and dependent tuples, as well as existentially and universally-quantified statements:</p> <pre><code>-- Normal function, corresponding to "Integer -> Integer" in Haskell factorial : Π ℕ (λ _ → ℕ) -- Polymorphic function corresponding to "forall a . a -> a" id : Π Set (λ A -> Π A (λ _ → A)) -- A universally-quantified logical statement: all natural numbers n are equal to themselves refl : Π ℕ (λ n → n ≡ n) -- (Integer, Integer) twoNats : Σ ℕ (λ _ → ℕ) -- exists a. Show a => a someShowable : Σ Set (λ A → Σ A (λ _ → Showable A)) -- There are prime numbers aPrime : Σ ℕ IsPrime </code></pre> <p>However, this does not address parametricity at all and AFAIK parametricity and Martin-Löf type theory are independent.</p> <p>For parametricity, people usually refer to the <a href="http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html" rel="noreferrer">Philip Wadler's work</a>.</p>

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