fpp/docs/spec/Type-Checking.adoc

== Type Checking

In this section, we explain the rules used to assign types to
expressions. FPP is a statically typed language. That means the
following:

* Type checking of expressions occurs during
<<Analysis-and-Translation_Analysis,analysis>>.

* If the type checking phase detects a violation of any of these rules,
then translation halts with an error message and does not produce any
code.

Each type represents a collection of
<<Values,values>>.
The type checking rules exist to ensure that whenever an expression of
type stem:[T] is <<Evaluation_Evaluating-Expressions,evaluated>>,
the result is a value of type stem:[T].

=== Integer Literals

To type an
<<Expressions_Integer-Literals,integer
literal expression>>, the semantic analyzer does the following:

. Evaluate the expression to an unsigned integer value stem:[v].

. Assign the type <<Types_Internal-Types_Integer,_Integer_>> to the expression.

**Examples:**

[source,fpp]
----
constant a = 0 # Type is Integer
constant b = 1 # Type is Integer
constant c = 256 # Type is Integer
constant d = 65536 # Type is Integer
constant e = 0x100000000 # Type is Integer
----

=== Floating-Point Literals

The type of a
<<Expressions_Floating-Point-Literals,floating-point
literal expression>> is `F64`.

=== Boolean Literals

The type of a
<<Expressions_Boolean-Literals,boolean
literal expression>> is `bool`.

=== String Literals

The type of a
<<Expressions_String-Literals,string
literal expression>> is `string`.

=== Identifier Expressions

To type an <<Expressions_Identifier-Expressions,identifier
expression>> stem:[e], the semantic analyzer
<<Scoping-of-Names_Resolution-of-Identifiers,resolves the identifier to a
definition>> and uses the type given in the definition.

**Example:**

[source,fpp]
----
constant a = 42 # a is a constant with type Integer
constant b = a # The expression a refers to the constant a and has type Integer
----

=== Dot Expressions

To type a
<<Expressions_Dot-Expressions,dot
expression>> stem:[e] `.x`, the semantic analyzer does the following:

. If stem:[e]`.x` is a
<<Scoping-of-Names_Qualified-Identifiers,qualified identifier>> that represents
the use of a definition according to the
<<Scoping-of-Names_Resolution-of-Qualified-Identifiers,rules
for resolving qualified identifiers>>, and the use is a valid
<<Expressions_Dot-Expressions,dot
expression>>, then use the type given in the definition.

. Otherwise do the following:

.. Compute the type stem:[T] of stem:[e].

.. If stem:[T] is a <<Types_Struct-Types,struct type>>
or <<Types_Internal-Types_Anonymous-Struct-Types,anonymous struct type>>
with a member `x`, then use the type associated with `x`.

.. Otherwise throw an error.

*Example:*

[source,fpp]
----
module M {
  constant a = 0 # The constant M.a has type Integer
  constant b = {
    c = "string1"
    d = "string2"
  }
}
constant b = M.a # Expression M.a represents a use of the definition M.a.
                 # Its type is Integer.

constant c = M.b.c # Expression M.b.c uses M.b and selects member `c`.
                   # Its type is string.
----

=== Array Expressions

To type an
<<Expressions_Array-Expressions,array expression>>
`[` stem:[e_1] `,` stem:[...] `,` stem:[e_n] `]`,
the semantic analyzer does the following:

. For each stem:[i in [1,n]], compute the type stem:[T_i] of stem:[e_i].

. Compute the <<Type-Checking_Computing-a-Common-Type_Lists-of-Types,common type>>
stem:[T] of the list of types stem:[T_i].

. Assign the type _[_ stem:[n] _]_ stem:[T] to the expression.

*Examples:*

[source,fpp]
----
constant a = [ 1, 2, 3 ] # Type is [3] Integer
constant b = [ 1, 2, 3.0 ] # Type is [3] F64
----

=== Array Subscript Expressions

To type an
<<Expressions_Array-Subscript-Expressions,array subscript expression>>
stem:[e_1] `[` stem:[e_2] `]`, the semantic analyzer does the following:

. Compute the type stem:[T_1] of stem:[e_1].

. Check that stem:[T_1] is an <<Types_Array-Types,array type>> or
<<Types_Internal-Types_Anonymous-Array-Types,anonymous array type>>
with element type stem:[T] and size stem:[n].

. Compute the type stem:[T_2] of stem:[e_2].

. Check that stem:[T_2] <<Type-Checking_Type-Conversion,may be converted to>>
_Integer_.

. Use stem:[T] as the type of the expression.

=== Struct Expressions

To type a
<<Expressions_Struct-Expressions,struct expression>>
`{` stem:[m_1] `=` stem:[e_1] `,` stem:[...] `,` stem:[m_n] `=` stem:[e_n] `}`,
the semantic analyzer does the following:

. Check that the member names stem:[m_i] are distinct.

. For each stem:[i in [1,n]], compute the type stem:[T_i] of stem:[e_i].

. Assign the type _{_ stem:[m_1] _=_ stem:[T_1] _,_ stem:[...] _,_ stem:[m_n] _=_ stem:[T_n] _}_
to the expression.

*Examples:*

[source,fpp]
----
constant a = { x = 1, y = 2.0 } # Type is { x: Integer, y: F64 }
constant b = { x = 1, x = 2 } # Error
----


=== Unary Negation Expressions

To type a
<<Expressions_Arithmetic-Expressions,unary
negation expression>> `-` stem:[e], the semantic analyzer does the following:

. Compute the type stem:[T] of stem:[e].

. If stem:[T] is a <<Types_Internal-Types_Numeric-Types,numeric type>>, then use stem:[T].

. Otherwise if stem:[T] <<Type-Checking_Type-Conversion,may be converted to>>
_Integer_, then use _Integer_.

. Otherwise throw an error.

**Examples:**

[source,fpp]
----
constant a = -1.0 # Type is F64
constant b = -1 # Type is Integer
constant c = -c # Type is Integer
constant d = -0xFFFFFFFF # Type is Integer
enum E { X = 1 }
constant e = -E.X # Type is Integer
constant f = -true # Error
----

=== Binary Arithmetic Expressions

To type a
<<Expressions_Arithmetic-Expressions,binary
arithmetic expression>> stem:[e_1] _op_ stem:[e_2], the semantic analyzer does
the following:

. Compute the common type stem:[T] of stem:[e_1] and stem:[e_2].

. If stem:[T] is a <<Types_Internal-Types_Numeric-Types,numeric type>>, then use stem:[T].

. Otherwise if stem:[T] <<Type-Checking_Type-Conversion,may be converted to>>
_Integer_, then use _Integer_.

. Otherwise throw an error.

**Examples:**

[source,fpp]
----
constant a = 1 + 2 # Type is Integer
constant b = 3 + 4 # Type is Integer
constant c = -0xFFFFFFFF # Type is Integer
enum E { X = 1, Y = 2 }
constant d = X + Y # Type is Integer
constant e = true + "abcd" # Error
----

=== Parenthesis Expressions

To type a
<<Expressions_Parenthesis-Expressions,parenthesis
expression>> `(` stem:[e] `)`, the semantic analyzer does the following:

. Compute the type stem:[T] of stem:[e].

. Use stem:[T] as the type of the expression.

**Examples:**

[source,fpp]
----
constant a = (1.0 + 2) # Type is F64
constant b = (3 + 4) # Type is Integer
constant c = (true) # Type is bool
constant d = ("abcd") # Type is string
constant e = ([ 1, 2, 3]) # Type is [3] Integer
----

=== Identical Types

We say that types stem:[T_1] and stem:[T_2] are *identical* if one
of the following holds:

. stem:[T_1] and stem:[T_2] are
<<Types_Internal-Types_Numeric-Types,numeric types>>
with the same name, e.g., `U32` or _Integer_.
In each case of a numeric type, the name of the type uniquely identifies
the type.

. stem:[T_1] and stem:[T_2]
are both
<<Types_The-Boolean-Type,the Boolean type>>.

. stem:[T_1] and stem:[T_2]
are both  the same
<<Types_String-Types,string type>>.

. Each of stem:[T_1] and stem:[T_2]
is an
<<Types_Abstract-Types,abstract type>>,
<<Types_Alias-Types,alias type>>,
<<Types_Array-Types,array type>>,
<<Types_Enum-Types,enum type>>, or
<<Types_Struct-Types,struct type>>,
and both types refer to the same definition.

=== Type Conversion

We say that a type stem:[T_1] *may be converted to* another type stem:[T_2] if
every <<Values,value>> represented by type stem:[T_1] can be
<<Evaluation_Type-Conversion,converted>> into a value of type stem:[T_2].

Here are the rules for type conversion:

. stem:[T_1] may be converted to stem:[T_2] if stem:[T_1] and stem:[T_2]
are <<Type-Checking_Identical-Types,identical types>>.

. If either stem:[T_1] or stem:[T_2] or both is an
<<Types_Alias-Types,alias type>>, then stem:[T_1]
may be converted to stem:[T_2] if the <<Types_Underlying-Types,underlying
type>> of stem:[T_1] may be converted to
the <<Types_Underlying-Types,underlying type>> of stem:[T_2].

. Any <<Types_String-Types,string type>> may be converted
to any other string type.

. Any <<Types_Internal-Types_Numeric-Types,numeric
type>> may be converted to any other numeric type.

. An <<Types_Enum-Types,enum type>> may be converted to a
<<Types_Internal-Types_Numeric-Types,numeric type>>.

. If stem:[T_1] or stem:[T_2] or both are
<<Types_Array-Types,array types>>, then
stem:[T_1] may be converted to stem:[T_2] if the conversion
is allowed after replacing the array type or types with
structurally equivalent
<<Types_Internal-Types_Anonymous-Array-Types,anonymous array types>>.

. An anonymous array type stem:[T_1 =] _[_ stem:[n] _]_ stem:[T'_1]
may be converted to the anonymous array type
stem:[T_2 =] _[_ stem:[m] _]_ stem:[T'_2]
if stem:[n = m] and stem:[T'_1] may be converted to stem:[T'_2].

. A <<Types_Internal-Types_Numeric-Types,numeric type>>,
  <<Types_The-Boolean-Type,Boolean type>>, <<Types_Enum-Types,enum type>>, or
<<Types_String-Types,string type>> stem:[T_1] may be converted to an anonymous
array type stem:[T_2] if stem:[T_1] may be converted to the member type of
stem:[T_2].

. If stem:[T_1] or stem:[T_2] or both are
<<Types_Struct-Types,struct types>>, then
stem:[T_1] may be converted to stem:[T_2] if the conversion
is allowed after replacing the struct type or types with
structurally equivalent
<<Types_Internal-Types_Anonymous-Struct-Types,anonymous struct types>>.
For purposes of structural equivalence, the member sizes of
struct types are ignored.
For example, the struct type `S` defined by `struct S { x: [3] U32 }`
is structurally equivalent to the anonymous struct type
`{ x: U32 }`.

. An anonymous struct type
stem:[T =]_{_ stem:[m_1] _:_ stem:[T_1] _,_
stem:[...] _,_ stem:[m_1] _:_ stem:[T_n] _}_ may be converted to
the anonymous struct type stem:[T'] if for each stem:[i in [1,n\]],

.. stem:[m_i] _:_ stem:[T'_i] is a member of stem:[T']; and

.. stem:[T_i] may be converted to stem:[T'_i].

. A <<Types_Internal-Types_Numeric-Types,numeric type>> type, <<Types_The-Boolean-Type,Boolean
type>>,
<<Types_Enum-Types,enum type>>, or <<Types_String-Types,string type>> stem:[T]
may be converted to an
<<Types_Internal-Types_Anonymous-Struct-Types,anonymous struct type>> stem:[T'] if
for each member stem:[m_i] `:` stem:[T_i] of stem:[T'],
stem:[T] may be converted to stem:[T_i].

. Type convertibility is transitive: if stem:[T_1] may be converted to
stem:[T_2]
and stem:[T_2] may be converted to stem:[T_3], then stem:[T_1]
may be converted to stem:[T_3].

=== Computing a Common Type

==== Pairs of Types

Here are the rules for resolving two types stem:[T_1] and stem:[T_2]
(e.g., the
types of two subexpressions) to a common type stem:[T] (e.g., the type of
the whole expression):

. If stem:[T_1] and stem:[T_2] are
<<Type-Checking_Identical-Types,identical types>>, then let
stem:[T] be stem:[T_1].

. Otherwise if stem:[T_1] or stem:[T_2] or both are <<Types_Alias-Types,alias
types>>, then do the following:

.. Let stem:[L_1] be the <<Types_Alias-Lists,alias list>> of stem:[T_1].

.. Let stem:[L_2] be the <<Types_Alias-Lists,alias list>> of stem:[T_2].

.. If there is no type in stem:[L_1] that is
<<Type-Checking_Identical-Types,identical>>
to a type in stem:[L_2], then replace each each alias type with its
<<Types_Underlying-Types,underlying type>> and reapply these rules.

.. Otherwise let stem:[T] be the first type in stem:[L_2] that is identical
to a type in stem:[L_1].

+
Note that the algorithm is symmetric in stem:[L_1] and stem:[L_2], i.e.,
reversing stem:[L_1] and stem stem:[L_2] in the last two items would
produce the same result.

. Otherwise if stem:[T_1] and stem:[T_2] are both
<<Types_Internal-Types_Numeric-Types,numeric types>>, then do the following:

.. If stem:[T_1] and stem:[T_2] are both floating-point types, then use `F64`.

.. Otherwise use <<Types_Internal-Types_Integer,_Integer_>>.

. Otherwise if stem:[T_1] and stem:[T_2] are both
<<Types_String-Types,string types>>, then use `string`.

. Otherwise if stem:[T_1] or stem:[T_2] or both are enum types, then replace
the enum type or types with the representation type specified in the enum definitions and
and reapply these rules.

. Otherwise if stem:[T_1] or stem:[T_2] or both are array types,
then replace the array type or types with structurally equivalent
anonymous array types and reapply these rules.

. Otherwise if stem:[T_1] and stem:[T_2] are anonymous array types with the same size stem:[n]
and with member types stem:[T'_1] and stem:[T'_2], then apply these rules to resolve
stem:[T'_1] and stem:[T'_2] to stem:[T'] and let stem:[T] be _[_ stem:[n] _]_ stem:[T'].

. Otherwise if one of stem:[T_1] and stem:[T_2] is a type stem:[T'] that is
convertible to an anonymous array type
and the other
one is an anonymous array type _[_ stem:[n] _]_ stem:[T''], then apply these
rules to resolve
stem:[T'] and stem:[T''] to a common type stem:[T''']. Let stem:[T] be
the
array type _[_ stem:[n] _]_ stem:[T'''].

. Otherwise if stem:[T_1] or stem:[T_2] or both are struct types,
then replace the struct type or types with structurally equivalent
anonymous struct types and reapply these rules.

. Otherwise if stem:[T_1] and stem:[T_2] are both anonymous struct types, then use
the anonymous struct type stem:[T] with the following members:

.. For each member stem:[m_1] _:_ stem:[T'_1] of stem:[T_1],
if stem:[T_2] has a member stem:[m_1] _:_ stem:[T'_2], then apply these rules
to convert stem:[T'_1] and stem:[T'_2] to a common type stem:[T'] and
use stem:[m_1] _:_ stem:[T']. Otherwise use stem:[m_1] _:_ stem:[T'_1].

.. For each member stem:[m_2] _:_ stem:[T'_2] of stem:[T_2] such
that stem:[T_1] has no member named stem:[m_2],
use stem:[m_2] _:_ stem:[T'_2].

. Otherwise if one of stem:[T_1] and stem:[T_2] is a type stem:[T'] that is
convertible to an anonymous struct type and the other
one is an anonymous struct type stem:[S], then apply these rules to resolve
stem:[T'] and each of the struct member types to a common type.
Let stem:[T] be the struct type whose member names are the member names of
stem:[S] and
whose member types are the corresponding common types.

. Otherwise the attempted resolution is invalid. Throw an error.

==== Lists of Types

To compute a common type for a list of types
stem:[T_1, ... , T_n], do the following:

.  Check that stem:[n > 0]. If not, then throw an error.

. Let stem:[T'_1] be stem:[T_1].

.  For each stem:[i in [2,n]], compute the
<<Type-Options_Computing-a-Common-Type-Option,
common type option>> stem:[T'_i] of stem:[T'_(i-1)] and stem:[T_i].

.  Use stem:[T'_n] as the common type option of the list.