I was studying polymorphic types and I was finding the distinction with monomorphic types difficult to pin down (context CS 421). From the course I linked the have the following (vague attempt) at a definition:
- Monomorphic Types ($\tau$):
- Basic Types: $int,bool,float,string,unit, \dots$
- Type types: $\alpha, \beta, \gamma, \delta, \epsilon$.
- Compund Types: $\alpha \to \beta, int * string, bool list, \dots$
- Polymorphic Types:
- Monomorphic types $\tau $
- Universally quantified monomorphic types
- $\forall \alpha_1, \dots, \alpha_n . \tau $ (Question: is this not just universally quantified monomophism? If not what's the difference?)
- Can think of $\tau$ (I assume they mean monomorphic types) the same as $\forall . \tau$
I guess I find MANY things in this definition rather confusing. But was seems to be the core about my confusion is the difference between:
$$ expr: \alpha \to \beta$$
vs
$$ expr : \forall \alpha, \beta . \alpha \to \beta$$
I don't understand why they are not the same. What is the difference?
After writing this question I have some ideas of what might be going on and want to double check. Is what is going on that $\alpha \to \beta $ (the first one) saying that the expression $expr$ has a monomorphic type as its type (so it just has a real "fixed" type as a type)... Perhaps what's confusing me are type variables. Because nothing can be of a type "type variable". Type variables are just (meta) variables that can later be filled in with a real "basic type", right? So $\alpha \to \beta$ in my first example just stands for "some function type from one type to another but we have not decided which type to choose later, but the expression really just has a fixed basic type as a type once used in a real programming context". Is that right? So saying $fun x \to x$ has type $\alpha \to \alpha$ when reasoning in the meta-theory just means that the function really just has a fixed basic type except we have not specified it. While saying (in a more expressive type system) that $fun x \to x$ has type $\forall \alpha . \alpha \to \alpha$ means that that expression actually has the capability of encompassing all the monomorphic types at once. i.e. in the monomorphic version we actually have to define each identity function separately for each type (for the sake or argument) while in the polymorphic version we have only have 1 single programming construct for all of them...so the type variable basically just stands for a real monomorphic type (at least in the context of this definition).
I guess if we allowed type variables to be anything, then I'd be confused...I think my main worry is about type variables.
More rambling cuz I'm confused:
Lets look at this from FOL or as if we were trying to construct or define what an L-term is with an L-structure (see mathematical logic MATH 570). I think right now what confuses me is that this mapping between this vague definition of types (that seems to attempt to define an L-term) is not clear to me. Where is the recursion? What is the L-structure? This type definition is vague for me to really believe it. Something like this would be much better:
Related question: What does $ \forall \alpha_1, \dots , \alpha_n . \tau $ mean formally as a type?