2
$\begingroup$

At page 21 of this book: https://cs.au.dk/~amoeller/spa/spa.pdf I found this:

enter image description here

I started reading everything and understanding it pretty well, until this.

It's defining the possible types of a language. I'm very confused about what theta and alpha mean. What are those meta-variables? What is ua.t and t[ua.t/a]?

Could someone give me some context? I'm not into computer science, this may be something specific that I have never seen before. I'm from a math background.

$\endgroup$
4
$\begingroup$

A metavariable is a variable that denotes some hypothetical chunk of a program. This distinction is important in the theory of programming languages, where we need to distinguish variables representing program fragments from the variables contained in those programs.

The terminology, I think, comes from logic: if you're defining a logic, you need to define it in some language that's distinct from the thing you're defining. This is the "meta-language", and the variables it uses are metavariables. The history of formal logic and programming languages are deeply intertwined via the Curry-Howard correspondence, so the terminology carried over.

$\endgroup$
1
  • $\begingroup$ Unfortunately this didn't help, there are still many questions. What is ua.t and t[ua.t/a]? Could you give an example of a meta variable? Thank you very much! $\endgroup$
    – Paprika
    May 23 at 2:48
1
$\begingroup$

Meta-variable explanation by example

Consider the simply typed lambda calculus (STLC) with base types Int for integers and Bool for booleans. In this calculus, we can have an identity function for integers $(\lambda x:\mathrm{Int}.x)$ and another one for booleans $(\lambda x:\mathrm{Bool}.x)$. More generally,

For every type $A$ of STLC, there is an identity function $(\lambda x:A.x)$.

The above sentence does not belong to the STLC language. It belongs to a meta-language: the language that I used (english) to express a property about STLC. The $A$ in the above sentence is a meta-variable that ranges over the set of types of STLC.

The distinction here is perhaps clearer, because we know that STLC has no type variables. But if you want to express properties about a language that has type variables, you may need to explicitly clarify what are variables of the object language (the calculus/language you talk about) and what are meta-variables (variables that belong in the language you use to express properties about the object language).


Notation

The notation $\mu a.\tau$ is a type that is similar to System F's polymorphic type $\forall a.\tau$. They both bind the type variable $\alpha$ in $\tau$. The difference is in the semantics. As the text states,

A type of the form $\mu a.\tau$ is considered identical to the type $\tau[\mu a.\tau / \alpha]$.

and this allows us to introduce recursive types in our object-language (which is not the case about $\forall a.\tau$).

Generally, for types $\sigma$ and $\sigma'$ (btw, these are again meta-variables) the notation $\sigma[\sigma' / \alpha]$ denotes substitution of the type variable $\alpha$ with $\sigma'$ in $\sigma$. In the text, they set $\sigma = \tau$ and $\sigma' = \mu a.\tau$.


... and now I realized this is a bit of an old question. :P

$\endgroup$

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.