5
$\begingroup$

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:

  1. Why is there a dot separating the quantifier and the type

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

  3. Is $\tau$ a function of the (meta?) variables $$ \forall \alpha_1, \dots , \alpha_n $$?
  4. What do $$ \forall \alpha_1, \dots , \alpha_n $$ stand for?
  5. Are $$ \forall \alpha_1, \dots , alpha_n $$ meta-variables? What is their domain?
  6. Could I have a couple of concrete examples of what they are

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


Crossposted: https://www.quora.com/unanswered/What-does-forall-alpha_1-dots-alpha_n-tau-mean-formally-as-a-type

$\endgroup$
3
$\begingroup$

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$.

  1. 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.

  1. 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.

  1. 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.

  1. What do $ \forall \alpha_1, \dots , \alpha_n $ stand for?
  2. 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.

  1. 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.

$\endgroup$
  • 1
    $\begingroup$ “τ is not a function, it's a monomorphic type” — it may or may not be considered a monomorphic type depending on the chosen terminology. In the ML type system, it's a type expression which may contain variables. In System F, it's a type which can contain further quantifiers so there's definitely no restriction that would force it to be monomorphic. $\endgroup$ – Gilles 'SO- stop being evil' Oct 25 '19 at 15:45
  • 1
    $\begingroup$ “when you use [] in your real code when it usually will be specialized to intlist” — actually, no. [] itself is polymorphic. A variable that sometimes happens to have the value [], on the other hand, is often monomorphic (but not always: not when you're writing polymorphic functions like List.length or List.map). $\endgroup$ – Gilles 'SO- stop being evil' Oct 25 '19 at 15:47
  • $\begingroup$ @Gilles slides 54 of the course notes I have defines what is a monomorphic types and polymorphic types. I think thats what the answer is referring to. $\endgroup$ – Pinocchio Oct 25 '19 at 16:38
  • $\begingroup$ 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? $\endgroup$ – Pinocchio Oct 25 '19 at 16:41
  • $\begingroup$ @Gilles That note about a monomorphic $\tau$ was in the context of the course material, which explicitly requires it to be monomorphic (which is also in accordance with standard HM, as far as I know). $\endgroup$ – siracusa Oct 26 '19 at 0:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.