patternMinor
What does $ \forall \alpha_1, \dots , \alpha_n . \tau $ mean formally as a type?
Viewed 0 times
alpha_1forallformallywhatdotsmeantypealpha_ntaudoes
Problem
I was learning about polymorphic types but I couldn't understand the notation, can someone explain it means (context cs421 UIUC):
$$ \forall \alpha_1, \dots , \alpha_n . \tau $$
its supposed to be a type but I have no idea what it's suppose to mean.
Perhaps writing some of my thoughts or questions might be helpful in clarifying what I'm confused about:
-
Why is there a dot separating the quantifier and the type
-
How does this relate to normal FOL? e.g. if I had $$ \forall x \phi(x) $$ that would mean that for all values x can take in the universe at hand, the proposition $\phi(x)$ is true (assuming the whole expression is true, which it may not be but whatever)
-
Could I have a couple of concrete examples of what they are
-
I am still confused what entails a monomorphic type vs a polymorphic type. In slide 54 they define that a monomorphic type can be a "type variable $\alpha, \beta, \gamma, \delta, \epsilon $". However, I find that very very confusing because consider the value $e$ with type $\alpha$ ($e:\alpha=$). What confuses me is that $\alpha$ can be ANY value, so doesn't that mean $e$ is polymorphic? How is that different from specifying the type value pair for that expression $e:\forall \alpha. \alpha$. They both seem the same to me. This is confusing me a lot. Whats the difference?
I think the lectures assume the definition of them its clear but it really isn't. Can I have a more formal specification of it?
For example when we are told $$x:\tau$$ as a notation its not clear at all it really just means the tuple $$ \langle x, \tau \rangle$$ (until I looked it up at Wikipedia). But Wikipedia didn't save my day for this question, unfortunately...
Crossposted: https://www.quora.com/unanswered/What-does-forall-al
$$ \forall \alpha_1, \dots , \alpha_n . \tau $$
its supposed to be a type but I have no idea what it's suppose to mean.
Perhaps writing some of my thoughts or questions might be helpful in clarifying what I'm confused about:
-
Why is there a dot separating the quantifier and the type
-
How does this relate to normal FOL? e.g. if I had $$ \forall x \phi(x) $$ that would mean that for all values x can take in the universe at hand, the proposition $\phi(x)$ is true (assuming the whole expression is true, which it may not be but whatever)
- Is $\tau$ a function of the (meta?) variables $$ \forall \alpha_1, \dots , \alpha_n $$?
- What do $$ \forall \alpha_1, \dots , \alpha_n $$ stand for?
- Are $$ \forall \alpha_1, \dots , alpha_n $$ meta-variables? What is their domain?
-
Could I have a couple of concrete examples of what they are
-
I am still confused what entails a monomorphic type vs a polymorphic type. In slide 54 they define that a monomorphic type can be a "type variable $\alpha, \beta, \gamma, \delta, \epsilon $". However, I find that very very confusing because consider the value $e$ with type $\alpha$ ($e:\alpha=$). What confuses me is that $\alpha$ can be ANY value, so doesn't that mean $e$ is polymorphic? How is that different from specifying the type value pair for that expression $e:\forall \alpha. \alpha$. They both seem the same to me. This is confusing me a lot. Whats the difference?
I think the lectures assume the definition of them its clear but it really isn't. Can I have a more formal specification of it?
For example when we are told $$x:\tau$$ as a notation its not clear at all it really just means the tuple $$ \langle x, \tau \rangle$$ (until I looked it up at Wikipedia). But Wikipedia didn't save my day for this question, unfortunately...
Crossposted: https://www.quora.com/unanswered/What-does-forall-al
Solution
The notation is explained in your course material, e.g. here starting on slide 47.
In the notation $$T = \forall \alpha_1, \dots, \alpha_n.\tau$$ $\alpha_i$ are type variables, the $\tau$ is a monomorphic type, and $T$ is a universally quantified, polymorphic type. While free type variables may occur in $\tau$, the quantified variables $\alpha_i$ do not occur free in $\tau$.
This is a just a syntactic convention used in type theory. The dot separates the quantifier part from the type it applies to.
There's a strong relationship between logical formulas and types in programming languages, called Curry-Howard isomorphism.
$\tau$ is not a function, it's a monomorphic type. You can think of the quantification as adding more context to this monomorphic type thus making it polymorphic. The quantification basically "hides" the variables from the context the whole expression appears in.
$\alpha_i$ are type variables that (typically) occur free in $\tau$, but are bound by the quantification and do not occur free in $\forall\alpha_i.\tau$ anymore. Like variables in a mathematical expression represent placeholders for concrete values, type variables represent placeholders for more concrete types.
The most common example of a polymorphic type is the list type $\forall \alpha . \alpha\;\mathsf{list}$ (this is the notation for Ocaml, in Haskell the notation would be $\forall \alpha.[\alpha]$). In your real code this polymorphic type might be used as a monomorphic type when $\alpha$ is replaced by a concrete type like $\mathsf{int\;list}$, $\mathsf{bool\;list}$ or even $\mathsf{(int\;list)\;list}$.
Sometimes you may still deal with polymorphic types, for example the empty list literal $[\,]$ has the polymorphic type $\forall\alpha.\alpha\;\mathsf{list}$. Note that this is different from when you use $[\,]$ in your real code when it usually will be specialized to $\mathsf{int\;list}$ (or whatever concrete lists you are dealing with) when type inference happens. So $[\,]$ may have one polymorphic type or one of many monomorphic types, where the latter are all very different.
The above linked PDF gives more examples on slide 55.
In the notation $$T = \forall \alpha_1, \dots, \alpha_n.\tau$$ $\alpha_i$ are type variables, the $\tau$ is a monomorphic type, and $T$ is a universally quantified, polymorphic type. While free type variables may occur in $\tau$, the quantified variables $\alpha_i$ do not occur free in $\tau$.
- Why is there a dot separating the quantifier and the type
This is a just a syntactic convention used in type theory. The dot separates the quantifier part from the type it applies to.
- How does this relate to normal FOL? e.g. if I had $ \forall x \phi(x) $ that would mean that for all values x can take in the universe at hand, the proposition $\phi(x)$ is true
There's a strong relationship between logical formulas and types in programming languages, called Curry-Howard isomorphism.
- Is $\tau$ a function of the (meta?) variables $ \forall \alpha_1, \dots , \alpha_n $?
$\tau$ is not a function, it's a monomorphic type. You can think of the quantification as adding more context to this monomorphic type thus making it polymorphic. The quantification basically "hides" the variables from the context the whole expression appears in.
- What do $ \forall \alpha_1, \dots , \alpha_n $ stand for?
- Are $ \forall \alpha_1, \dots , \alpha_n $ meta-variables? What is their domain?
$\alpha_i$ are type variables that (typically) occur free in $\tau$, but are bound by the quantification and do not occur free in $\forall\alpha_i.\tau$ anymore. Like variables in a mathematical expression represent placeholders for concrete values, type variables represent placeholders for more concrete types.
- Could I have a couple of concrete examples of what they are
The most common example of a polymorphic type is the list type $\forall \alpha . \alpha\;\mathsf{list}$ (this is the notation for Ocaml, in Haskell the notation would be $\forall \alpha.[\alpha]$). In your real code this polymorphic type might be used as a monomorphic type when $\alpha$ is replaced by a concrete type like $\mathsf{int\;list}$, $\mathsf{bool\;list}$ or even $\mathsf{(int\;list)\;list}$.
Sometimes you may still deal with polymorphic types, for example the empty list literal $[\,]$ has the polymorphic type $\forall\alpha.\alpha\;\mathsf{list}$. Note that this is different from when you use $[\,]$ in your real code when it usually will be specialized to $\mathsf{int\;list}$ (or whatever concrete lists you are dealing with) when type inference happens. So $[\,]$ may have one polymorphic type or one of many monomorphic types, where the latter are all very different.
The above linked PDF gives more examples on slide 55.
Context
StackExchange Computer Science Q#116271, answer score: 3
Revisions (0)
No revisions yet.