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.

ALT

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:

ALT

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:

ALT