Re: Type system terminology

On Tue, Sep 1, 2015 at 1:14 PM, Matthias-Christian Ott <[email protected]> wrote:
> I'm a bit confused about type system terminology because a lot of terms
> seem to be used sloppily and it seems that some terms are synonymous.
> Perhaps someone can clarify the type system terminology that is used in
> Standard ML.
>
> Suppose that I have the following type declarations:
>
> type 'a t1 = 'a list
>
> datatype 'a t2 = C1 of 'a | C2 of 'a | C3
>
> type t3 = int t2
>
> As I understand it after searching "The Definition of Standard ML,
> Revised" and "Programming in Standard ML" , the following statements
> describe the type declarations:
>
> "type 'a t1 = 'a list", "datatype 'a t2 = C1 of 'a | C2 of 'a | C3" and
> "type t3 = int t2" are type declarations that declare the types t1, t2,
> t3 and the type constructors t1, t2, t3. t3 is a constant type
> constructor and t1 and t2 are non-constant type constructors.

It is more common to refer to t3 as a "nullary type constructor" and
t1 and t2 as "unary type constructors".

> "'a list", "'a" and "int t2" are type expressions that denote the types
> t1, t2 and t3.

That's not quite right.  "'a list", "'a", and "int t2" are type
expressions, but you wouldn't say that they denote the types t1, t2,
and t3.  In particular, as non-nullary type constructors, t1 and t2 by
themselves aren't types.

> "'a list" and "'a" are type schemes.

Whether or not a type expression is a type scheme is somewhat context
dependent.  Since Standard ML doesn't have explicit binding of type
variables in types, you need to know a little more about the context
in which a type expression appears to know whether or not it is a type
scheme.  For example, consider the following:

val mkpair : 'a -> ('a * 'a) : fn x => (x, x)

We would say that mkpair has the type scheme "'a -> 'a * 'a", which
means that we think of the type of mkpair as "forall 'a, 'a -> 'a *
'a".  On the other hand, we wouldn't call "'a * 'a" a type scheme in
this context, because it isn't the body of an implicit forall.

> t1, t2 are polymorphic types that are parametrized by the type variable
> 'a and t3 is a monomorphic type.

Yes.

> t1 and t3 are type bindings and t2 is a data type.

Yes.

> Values of the type t2 can be constructed by the value constructors C1,
> C2 and C3. C3 is a constant value constructor and C1 and C2 are
> non-constant value constructors.

Again, it would be more common to refer to C3 as a nullary value
constructor and C1 and C2 as unary value constructors.  It is also
fairly common to refer to these as "data constructors" (or sometimes
variants).

> t3 instantiates the type t2 by applying the type constructor t2 to type
> int as the positional argument 1 (or 0 depending on how you count).
>
> Are the terms used in the statements being used correctly?
>
> What is the difference between a type scheme, polymorphic type and
> polymorphic type constructor?

Many people use type scheme and polymorphic type interchangeably.
But, in the formal setting of the Definition and other careful
presentations of type inference, a val-bound variable always has a
type scheme, possibly with an empty set of type variables.  That is,
consider:

val inc = fn x => x + 1
val proj1 = fn (x,y) => x

inc has the type scheme "forall , int -> int" and proj1 has the type
scheme "forall 'a 'b, 'a * 'b -> 'a".  We generally call inc a
monomorphic function and proj1 a polymorphic function, but the are
both described with type schemes.  So, a polymorphic type is a type
scheme with a non-empty set of type variables.

A polymorphic type constructor is a non-nullary type constructor --- a
type constructor that you need to apply to other well-formed type
expressions to form a type.

> Is there a difference between a constant and a nullary type constructor?
> Is there a difference between a constant and a nullary value
> constructor? If not, which terms are preferred?

As noted above, nullary type constructor and nullary value (or data)
constructor are the preferred terms.

> What is the difference between a type constructor application, type
> construction and type instantiation?

I don't know the term "type construction", other than possibly as a
synonym of type expression.

Type constructor application and type instantiation are very different.

Type constructor application is the syntax for building well-formed
type expressions from non-nullary type constructors.  So, "int list",
"(bool ref) option", "(int, int) map", etc are type constructor
applications.  The syntax of SML doesn't allow it, but one might even
consider nullary type constructors to be applied, just to an empty
list of type expressions: "(() int) list" or "((() bool) ref) option".

Type instantiation is the (implicit, during type inference/checking)
process of substituting type expressions for type variables in a type
scheme.  For instance, with our proj1 function above, the expression
"proj1 (1, true)" requires an instantiation of the type scheme with
int for "'a" and bool for "'b" to obtain "int * bool -> int".

> What is the difference between a type binding and a type expression in a
> type system with structural type equivalence?

Well, they are different syntactic categories. But, it is true that
one could "expand away" all type bindings in a program and have an
equivalent program; indeed, that's effectively their treatment in the
definition of SML type system.

Hope that helps.

-Matthew

To unsubscribe from this group and stop receiving emails from it, send an email to [email protected].

------------------------------------------------------------------------------
Monitor Your Dynamic Infrastructure at Any Scale With Datadog!
Get real-time metrics from all of your servers, apps and tools
in one place.
SourceForge users - Click here to start your Free Trial of Datadog now!
http://pubads.g.doubleclick.net/gampad/clk?id=241902991&iu=/4140