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)
- 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=<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...