# Data types and type inference¶

Values in CertSAFE can come from a variety of **data types**, including
Boolean, integer, floating-point, and user-defined
enumeration types. To help catch
mistakes, CertSAFE performs static type checking and issues errors if
components are connected in an ill-typed way. For example, it is not
permitted to feed the output of an AND gate into a multiplication
component, because multiplication requires a numeric type and Boolean
values are not considered numeric.

Much of the time, it is not necessary to annotate data types explicitly
in your model. CertSAFE performs **type inference** that can fill in
most types automatically. An example will illustrate this process.

This diagram only has one type annotation: the input Y has been constrained to the type Int16 (16-bit signed two’s-complement integer). Yet, CertSAFE can infer the types of all the wires in the diagram fully.

- From the fact that AND gates have Boolean-typed inputs and outputs, CertSAFE can deduce that Z, O, and the output of the comparator all have type Bool.
- The explicit annotation forces Y to have type Int16.
- The type of X is not directly constrained by any component connected to it, since comparators can work on different types of values (they are polymorphic Using reasoning similar to this, CertSAFE can deduce the data types for almost all networks in a diagram with a minimum of explicit annotations. The same processes is also applied for stitches.

## How type inference works¶

Most of the time, it is not necessary to think about how CertSAFE performs its type inference. However when designing your models or debugging problems, it can be helpful to know a bit about CertSAFE’s type system.

CertSAFE uses a variant of the Hindley-Milner type
system.
In this system, the type of a wire can either be a **type constant**
(Bool, Float64, an enum type...) or a **type variable** (represented in
CertSAFE as Greek letters α, β, γ...). During type inference, all of the
types in a diagram start out as unconstrained type variables. CertSAFE
then uses the information in the diagram to progressively restrict the
possible types that each network could have. If two constraints conflict
with each other, CertSAFE generates a type error.

The simplest sort of constraint occurs when a network is directly connected to a component pin that must have a particular type. This is the case with the wires connected to the AND gate in the example above. The adjacent networks all have to have type Bool because that is the only type allowed for those pins.

When using polymorphic
components, different pins of a component that share the same type
variable must be instantiated (substituted The final variety of
constraint is called a **type class**. A type class constraint restricts
a type variable to be instantiated only with data types that support
certain operations. Suppose we tried to change the type annotation on Y
in the example above to be Bool instead of Int16. CertSAFE will generate
an error message saying that “The type ‘Bool’ does not provide an
instance for the type class ‘Ordered’.” Here, “Ordered” is the name of a
type class consisting of types that support “less than” / “greater than”
comparisons. The Bool types does not support these operations in
CertSAFE, so a type error is produced. (For the complete list of type
classes and which data types implement them, see the data
types reference article. When type inference
is completed, the inferred data types are used to construct a **type
signature** for the diagram that will determine how it interacts with
other diagrams and stitches it is placed in. Any remaining type
variables and type classes are generalized to become part of the type
signature. See the polymorphism
article for more details.

## When type inference fails¶

There are a few rare circumstances where CertSAFE cannot infer a data type from the information given in a diagram or stitch. This example illustrates one such case:

What is the data type of the variable named “Counter” in the diagram above? It could be any numeric type, and there is no way for CertSAFE to know which type the diagram author had in mind. Not only that, but, depending on the data type, the “Result” output of the diagram will have different values. If the type is Int8, the counter will overflow after 127 frames to -128 and “Result” will become true. If the type is UInt8, on the other hand, the counter will overflow from 255 to 0 and “Result” will never be true. And if the type is Float32, the counter will run for a long time before eventually saturating at 2^24 without ever overflowing.

Rather than trying to guess what the author had in mind, CertSAFE will
generate an **ambiguous type** error on the diagram: “This diagram
contains a type variable which cannot be fixed to a single type by any
instantiation of the diagram.” The solution to this error is to specify
a type explicitly using a Type Annotation primitive: