We’re rewarding the question askers & reputations are being recalculated! Read more.

# Tag Info

## New answers tagged type-checking

0

If you interpret a type $\tau$ as a set of values $Set_\tau$, then a natural definition for the interpretation of a polymorphic type would be the following: $$Set_{\forall \alpha.\tau} = \bigcap_{\kappa \in Types} Set_{\tau[\alpha := \kappa]}$$ You need an intersection because intuitively a polymorphic type should work for all its instantiations. Of course, ...

2

I am not sure I understand your question, but I believe the answer is "yes". When describing monomorphic languages, an expression such as let id x = x : τ (where τ is understood as a type meta-variable) does not mean that you can write τ in the program text. Rather, it means an arbitrary expression of that shape, where the meta-variable is replaced by ...

3


3

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

Top 50 recent answers are included