Type Annotations and Coercions

DaeDaLus declarations and expressions may be annotated with explicit types, which is useful when type inference fails to infer the type of something, or to improve the readability of the specification.

Annotating an Expression

Use e : t to specify that expression e should have type t. For example:

def i_am_a_byte = 1 : uint 8

Note that without the type annotation on the expression 1 the resulting declaration would be polymorphic because literals are overloaded and may be used at many different types.

Annotating the Result of a Declaration

To specify the result type of a declaration use : t after the name (or the parameters, if any) of the declaration like this:

def also_byte : uint 8 = 1

def returns_byte x : uint 8 = x

Annotating a Parameter

Parameters of declarations may also be annotated with a type:

def Example (P : uint 8) = P

The previous example specifies that parameter P is a parser that will construct a uint 8 semantic value.

Naming Unknown Types

Occasionally it is useful to name a type without specifying it explicitly. For example:

def f (x : maybe ?a) = 1 : ?a

The type annotation maybe ?a specifies that the input should be of type maybe ?a for some type ?a that we can refer to using the name ?a, as we do in the body.

Warning

The notation ?x is used for two unrelated features: in types it refers to some unknown type, as in the previous example; in parsers and value declarations it refers to Implicit Parameters.

Coercions

Coercions provide a way to change a semantic value into the corresponding value of a different type. The general form is e as T, which converts the value of expression e into type T. For example, the following code will parse a byte and pad the resulting value out to a 32-bit unsigned integer.

block
  let i = UInt8
  ^ i as uint 32

The base form e as T statically checks that the resulting type has enough bits to losslessly represent the original value. There are two other forms, as! and as? that can be used when this does not hold true statically:

• e as! T is guaranteed to succeed, but may lose information. In the case that the original value fits into the target type, the behaviour coincides with the lossless version of as. Otherwise, behaviour is implementation dependent, but will attempt to do something reasonable.

• e as? T performs a run-time check that the coercion will not lose information. If this holds, behaviour is identical to the lossless version of as. Otherwise, the coercion fails and backtracks.

Note that e as T and e as! T are values, and e as? T is a parser. This is because e as? T can fail and backtrack, which is only meaningful in parser expressions.