Type system terminology

Hi,

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.

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

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

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

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

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.

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?

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?

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

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

Thanks!

Regards,
Matthias-Christian

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