3
$\begingroup$

For example, $\forall x \in X, P(x)$ can be viewed as a map $P : X \to \text{TrueProp}$ the collection of true propositions.

Why do we make the distinction in type theory, which seems to want to reduce all constructions down to a few building blocks? In type theory $\forall$ is a handled using what's called a Pi-type, usually, but why didn't they just handle it using a mapping of types?

Certain $\forall$ statements become even more obviously just a map, as in $\forall x \in X, f(x) \in Y$ is the same thing as $f: X \to Y$.

I'm experimenting with software implementations of logic / math, so that's why I've asked this.

$\endgroup$
12
  • 2
    $\begingroup$ For background: are you familiar with the more standard Curry-Howard correspondence which treats a proposition as being identical to the type of valid proofs of the proposition, and then a $\forall$ universal quantifier becomes a special case of the Pi-type? (And similarly, an implication proposition $P \rightarrow Q$ has proofs which are functions taking a proof of $P$ as input and returning a proof of $Q$ as output; so it's a special case of a function type, which in turn is a special case of a Pi-type.) $\endgroup$
    – Daniel Schepler
    Sep 21, 2021 at 22:02
  • 2
    $\begingroup$ Terms of a function type are not themselves types that can have terms. Pi types are types that can have terms. All a function to Prop gives you is a type family, which is not the same thing as the Pi type of that family. $\endgroup$
    – Malice Vidrine
    Sep 21, 2021 at 22:53
  • 2
    $\begingroup$ Function types do have terms. The terms of such a type are not generally types, so don't have terms. $\endgroup$
    – Malice Vidrine
    Sep 21, 2021 at 22:57
  • 1
    $\begingroup$ @MaliceVidrine, well they're both not types as you said yourself. So they have that alike. $\endgroup$
    – D Left Adjoint to U
    Sep 21, 2021 at 23:12
  • 1
    $\begingroup$ In a complete type system any function f has a fixed (exponential) type given its abstraction and application types, but for universal quantified version, all those formulas are not of same type but a family (resemblance) of parameterized product types dependent on the objects denoted by the quantified variable. Curious why simply treating it as category arrows will make your programming easier as compared to a strongly typed programming language? In Haskell function map has type and is a first class citizen... $\endgroup$
    – mohottnad
    Sep 22, 2021 at 6:29

1 Answer 1

Reset to default
4
$\begingroup$

I'm going to assume we're talking about a standard type theory, something that's only a minor variation on the lambda cube systems. This said, the two things differ in several important ways.

For one, the $f$ in $f:A\to \mathsf{Prop}$ is not a thing which can have terms of its own; $x:f$ makes no sense in the language. On the other hand, the whole point of $\Pi(x:A).B(x)$ is it's a type which can have terms.

The term $f$ also does something entirely different from a term $g:\Pi(x:A).B(x)$. If $a:A$, then $f(a)$ is a term of type $\mathsf{Prop}$. On the other hand, $g(a)$ is a term of type $B(a)$, not $\mathsf{Prop}$. This is really the central purpose of Pi-types. There are no inference rules that let you take $f$ and generate a term of type $f(a)$ when given an $a:A$. Certainly, if we have a proof of $\forall (x:A).B(x)$, we should expect to be able to derive a proof of each instance $B(a)$, and this is something you can't do with just a map $B:A\to\mathsf{Prop}$.

$\endgroup$
9
  • 1
    $\begingroup$ If you have a proof of $\forall (x:A).B(x)$ then you have shown that $B : A \to$ universe $U$, given a definition of $B$, is indeed a map from $A$ into types, each of which we naturally denote by $B(a), a \in A$. If you have a proof that $B: A \to U$ is a map from $A$ into types, then you can write $\forall (x:A).B(x):U$. So I'm still not seeing the distinction. Why can't we do with a map what we can do with a Pi-type? The argument you gave is not convincing me that Pi-type is not just a special case of the Map type. $\endgroup$
    – D Left Adjoint to U
    Sep 21, 2021 at 23:47
  • 1
    $\begingroup$ Also, I'm saying $A \to \textbf{Prop}$ is the type, not $f$. You keep saying that I'm saying $f$ needs to be a type. I'm saying $f$ is a variable and $f: A \to \textbf{Prop}$ is a declaration of the variables type. Also there can indeed be maps that are sets - see category theory where a map can be anything not simply a function on sets. $\endgroup$
    – D Left Adjoint to U
    Sep 21, 2021 at 23:52
  • 1
    $\begingroup$ Yes, $B:A\to U$ is a map into types. But you do not get from $B$ and $a:A$ a term of type $B(a)$. A term $g:\forall(x:A).B(x)$ is not a map into types. I don't know how to be clearer that the two do patently different things. $\endgroup$
    – Malice Vidrine
    Sep 22, 2021 at 0:02
  • 1
    $\begingroup$ If you would like to argue that $B:A\to Prop$ and $a:A$ can be used to somehow give you a term $t:B(a)$, I invite you to tell me what rules of inference you think will give you this. $\endgroup$
    – Malice Vidrine
    Sep 22, 2021 at 0:04
  • 1
    $\begingroup$ can the rules of inference in the two perspectives be so different - in fact they are essentially the same thing. You say "is not a map" into types as if that's a proof in and of itself. I'm still not seeing what you meant. $\endgroup$
    – D Left Adjoint to U
    Sep 22, 2021 at 0:07

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .