Authoritative source: How to read a tulam type

How to read a tulam type

Types in tulam use the same general expression language as terms, subject to universe and phase checking. The quickest way to read a large type is to find its loosest-binding construct first.

Application

Maybe(Int)
Either(String, Int)
Matrix(Float32, rows, cols)

The name before parentheses is a type constructor; the arguments may themselves be types or values. Matrix(Float32, rows, cols) records an element type and two dimensions.

Function types

Int -> Bool
Int -> Int -> Int
(n:Nat) -> Vec(a,n)

Arrows associate right, so A -> B -> C means A -> (B -> C). A named binder before an arrow is in scope in the result, making the function dependent.

Product and sum types

Int * Bool
String + Int
(n:Nat) * Vec(a,n)

* forms a product and binds more tightly than +; both bind more tightly than ->. In a type declaration body the same symbols separate constructors and their fields, so read that context according to the declaration grammar.

Quantification

forall a. a -> a
exists (a:Type). { value:a, display:a -> String }

forall introduces an implicit Pi binder. exists hides a Sigma witness. Both bind more loosely than arrows and products.

Effect types

Eff {} Int
Eff { console:Console } Unit
Eff { state:State(s), console:Console | e } a

Read the row between braces as required effect installations and the final argument as the produced value. | e is an open row tail. Eff {} a is observationally pure and may normally be written simply a.

A reading procedure

For:

forall a. List(a) -> Eff { console:Console | e } Maybe(a)

read outward:

  1. for any inferred type a;
  2. accept a List(a);
  3. perform at least the labeled Console effect plus row e;
  4. produce Maybe(a).

Parentheses are preferable to cleverness when a type mixes dependency, effects, and several operators.

Types are checked expressions

A type constructor occupies a universe appropriate to what it constructs. Type-level computation must terminate when checking requires normalization. Runtime values do not become types merely because terms and types share syntax; universe and phase rules maintain the boundary.

Common mistakes

Read arrows from the outside and remember they associate right. Do not interpret * in a type expression as constructor-field punctuation, or erase an open effect-row tail when copying a higher-order type.

Recap

Find the loosest-binding form, then work inward. Application is tight, products bind before sums, arrows are right-associative, and quantifiers enclose the whole type that follows.

Normative details: Language Reference §4.