# History Types¶

In order to improve the expressivity of Kind 2’s specification language,
the tool provides a built-in type constructor that allows users to
refer to an unbounded number of previous values of a stream.
Specifically, the unary type constructor `history(x)`

, that
takes a stream `x`

of arbitrary type `T`

as its single argument,
represents the set of all streams `z`

of values of type `T`

such that
at any time `t >= 0`

, there exists a `k`

in the interval `[0, t]`

such that
`z(t) = x(k)`

.

For instance, given a node with an input stream `x`

and an output
stream `y`

, both with the same type, the property the current value of stream y
equals the current value or a previous value of a stream x plus one
can’t be expressed in Lustre. However, using the type constructor
`history`

, one can easily express the property as
`exists (z: history(x)) y=z+1`

.

Notice that `history(x)`

denotes a refinement type,
suggesting its applicability wherever a type is expected in the model.
However, at present, the implementation restricts the use of the
type constructor `history`

to the type of a quantified variable.
We plan to lift this restriction in future versions of Kind 2.