type

ATS is perhaps more advanced than any other languages when it comes to applying type theory an actual language, though this is not its only merit.

For dependent types and linear types, also see the FAQ.

A type is one of the many sorts that a static expression or static identifier can be. Other sorts are:

Ground sorts: int, bool, char, addr. They form the basis of dependent type indices. View, which are linear (in the sense of linear logic) propositions. Prop, which are classical propositions.

A t@ype or (any)t@ype may be any size, whereas a type must be the size of a pointer; a polymorphic or template function taking some t@ype as an argument should also take a type. Please not that, in some places, a '0' may replace the '@' in some type-related keywords. For instance, t0ype is introduced as an alpha-numeric alternative to t@ype . However, @[...] can not be changed into 0[...].

Viewtype, which are linear types. It can be seen as a type combined with a view. You can define a new sort using datasort. The first few lines of sllist.dats demonstrate how to define a sort that resembles a list. You can also alias sorts using sortdef, which also lets you piggy-back constraints to a sort called subset sort. See prelude/sortdef.sats for examples. A constraint is simply a static expression of a boolean sort.

For each of the type, view, prop, it is possible to alias, declare abstract quantities, and form algebraic constructors.

	Static	Type	View	Prop	Viewtype
Aliasing	stadef	typedef	viewdef	propdef	viewtypedef
Abstract	sta	abstype	absview	absprop	absviewtype
Algebraic	(N/A)	datatype	dataview	dataprop	dataviewtype

Type, view, prop, and viewtype are special cases of statics, so whenever you see typedef, viewdef, propdef and viewtypedef, you can just use stadef. Similarly, for abstract declarations, you can use sta for abstype, absview, absprop, and absviewtype. However, datasort, datatype, dataview, dataprop and dataviewtype are not interchangeable. They define algebraic constructors for a new "thing" (e.g. datatype gives you constructors for a new type, dataview gives you constructors for a new view, and so on). Reference and further discussion.

---

Type Annotation

For type annotation during value binding, it is important to remember the following:

There is a subtle difference between

val x = e: T

and

val x: T = e

It is almost always the case that one requires the former style of annotation in ATS.

The latter only checks that the type of e is a subtype of T.

This is most commonly addressed when dealing with case or if-then-else expressions.