Forall as an intersection over these sets
I read the existential section on Wikibooks and this is what it says there:
First, forall really means "to everyone." One way to think of types is as values of values with that type, for example, Bool is set {True, False, ⊥} (remember that the bottom, ⊥, is a member of every type!), Integer is a collection of integers ( and bottom), String is the set of all possible strings (and bottom), etc. forall serves as the intersection over these sets. For example forall a. a - intersection for all types, which must be {⊥}, that is, a type (ie a set), the only value (ie an element) is the bottom.
How does it forall
serve as an intersection over these sets?
forall
in formal logic means that it can be any value from the universe of discourse. How does it translate to a crossroads in Haskell?
source to share
You need to view types in negative or positive context - i.e. either under construction or in use (eat / receive, and this is probably best understood in Semantics of the Game, but I'm not familiar with them). In the meantime, there is no need to know about it. ”
If I "give you" a type forall a . a
, then you know that I built it somehow. The only way for a particular constructed meaning to have a type forall a . a
is that it can be standard for all types in the universe of discourse - this is, of course, the intersection of their functionality. In normal languages there is no such meaning ( Void
), but in Haskell we have a bottom.
bottom :: forall a . a
bottom = let a = a in a
On the other hand, if I somehow magically have a meaning forall a . a
, and I try to use it, then we get the opposite effect - I can see it as something in the unification of all types in the universe of discourse (this is what you were looking for) and so I
absurd :: (forall a . a) -> b
absurd a = a
source to share
Haskell forall
-s can be thought of as limited types of dependent functions, which in my opinion are conceptually the most enlightened approach, and also the most suitable for set-theoretic or logical interpretations.
In a dependent language, you can bind the values of arguments in function types and specify those values in return types.
-- Idris
id : (a : Type) -> (a -> a)
id _ x = x
-- Can also leave arguments implicit (to be inferred)
id : a -> a
id x = x
-- Generally, an Idris function type has the form "(x : A) -> F x"
-- where A is a type (or kind/sort, or any level really) and F is
-- a function of type "A -> Type"
-- Haskell
id :: forall (a : *). (a -> a)
id x = x
The most important difference is that Haskell can only bind types, overridden types and type constructors using forall
, while dependent languages can bind anything.
In the literature, dependent functions are called dependent products. Why would they call that when they, well, function? It turns out that we can implement algebraic Haskell types using only dependent functions.
Typically, any function a -> b
can be thought of as a search function for some product, where keys are of type a
and items are of type b
. Bool -> Int
can be interpreted as a pair of Int
-s. This interpretation is not very interesting for independent functions, since all product fields must be of the same type. With dependent functions, our pair can be polymorphic:
Pair : Type -> Type -> Type
Pair a b = (index : Bool) -> (if index then a else b)
fst : Pair a b -> a
fst pair = pair True
snd : Pair a b -> b
snd pair = pair False
setFst : c -> Pair a b -> Pair c b
setFst c pair = \index -> if index then c else pair False
setSnd : c -> Pair a b -> Pair a c
setSnd c pair = \index -> if index then pair True else c
We've restored all the essential pairing functionality here. In addition, using Pair
, we can create products of arbitrary arity.
So what does this have to do with interpreting forall
-s? Well, we can interpret ordinary products and create some intuition for them, and then try to translate them into forall
-s.
So let's first take a look at the algebra of conventional products. Algebraic types are called algebraic because we can define the number of their values with algebra. Link to detailed explanation. If it a
has a |A|
number of values and b
has a |B|
number of values, then it Pair A B
has a |A| * |B|
number of possible values. With the sums, we add up the number of inhabitants. As a -> b
can be considered as a product with fields |A|
, all of which are of the type b
, the number of inhabitants a -> b
of |A|
the number |B|
-s, multiplied together, which is equal to|B|^|A|
... Hence, the name "exponential type" is sometimes used to refer to functions. When the function depends, we fall back to the interpretation of "product of several different types", since the exponential formula no longer works.
Armed with this understanding, we can interpret forall (a :: *). t
as a product type with type indices *
and fields having a type t
where a
you can specify it internally t
, and hence the field types can vary depending on the selection a
. We can search for fields by making Haskell invoke a specific type for forall
, effectively applying a function to the type argument.
Note that this product has as many fields as there are index values, which is almost infinite here given the potential number of Haskell types.
source to share
How does it
forall
serve as an intersection over these sets?
Here you can start reading a little bit about the Curry-Howard correspondence . In short, you can think of type as a logical proposition, linguistic expressions as proofs of their types, and values as normal proofs of forms (proofs that cannot be simplified further). So, for example, it "Hello world!" :: String
reads " "Hello world!"
is a proof of proposal String
."
So now think of forall a. a
as a proposal. Intuitively think of it as a second-order quantitative expression over a propositional variable: "For all statements a
, a
". This is basically the approval of all proposals. This means that if it x
is a proof forall a. a
, then for any proposition P
x
it is also a proof P
. So, since proofs forall a. a
are proofs that prove any proposition, it follows that the proof forall a. a
should be the same as you if you compared each proposition with its set of proofs and intersected them. And the only proof of normal form (ie "Meaning") that is common to all of these sets is the bottom.
Another informal way of looking at this is that universal quantification is like infinite conjunction ( ∀x.P(x)
like P(c0) ∧ P(c1) ∧ ...
). The conjunction visible from the model-theoretic representation is given by the intersection; the set of evaluation environments where A ∧ B
is true is the intersection of environments where a
is true and those where is B
true.
source to share