Types of functions

All expressions in Kind have a type, describing what type of thing it computes. For example, Bool.true has type Bool, just like Notb Bool.true also has type Bool.

Functions like Notb, before they receive arguments, also have a type, just like Bool.true or Bool.false. Their types are called Function Types, and are denoted with arrows.

Notb, for example, would be denoted as Bool -> Bool, which can be read as "a function that takes a Bool as input and returns a value of type Bool". Similarly, the type of the Andb function is Bool -> Bool -> Bool, meaning "a function that takes two arguments of type Bool and returns a value of type Bool".