Types

This section covers how the type checker reasons about types, focusing on two concerns: well-formedness and equivalence.

The type checker needs to know two things about any type it encounters: whether the type is well-formed, and whether two types are the same. These two jobs are handled by two relations defined in 5.02-typing-type.watsup.

Type Elaboration: Type_ok

The Type_ok relation elaborates a surface-syntax type into its internal representation (typeIR).

relation Type_ok:
  typingContext |- type ~> typeIR
  hint(input %0 %1)

Read typingContext |- type ~> typeIR as: “under typingContext, the type type elaborates to the internal type typeIR.”

For base types, the rule is trivial: the surface type is already its own internal representation.

rule Type_ok/signed:   TC |- INT `< n `>    ~> INT `< n `>
rule Type_ok/unsigned: TC |- BIT `< n `>    ~> BIT `< n `>
rule Type_ok/boolType: TC |- BOOL          ~> BOOL
rule Type_ok/matchKindType: TC |- MATCH_KIND ~> MATCH_KIND

Named types require a lookup.

rule Type_ok/typeName:
  TC |- (_TID typeId) ~> typeIR
  -- if typeDefIR = $find_typeDef_t(TC, typeId)
  -- if typeIR = $typeIR_of_typeDefIR(typeDefIR)

When the checker sees a named type such as Header, it:

1. Looks up Header in the typing context TC via $find_typeDef_t, retrieving a typeDefIR.
2. Converts that typeDefIR to a typeIR with $typeIR_of_typeDefIR.

$typeIR_of_typeDefIR is a two-clause function defined in 5.00:

def $typeIR_of_typeDefIR(dataTypeIR)       = dataTypeIR
def $typeIR_of_typeDefIR(objectTypeDefIR)  = objectTypeDefIR

Both clauses are identity-like: a typeDefIR is either a dataTypeIR or an objectTypeDefIR, and both are subtypes of typeIR, so the conversion just changes the tag. The function exists to make the type explicit to the elaboration rule.

When a named type is resolved into its underlying type, not only do we know that it is a valid type, but the resolved information can be used somewhere else along the type checking process.

What typeIR looks like

Understanding elaboration requires knowing what the internal type universe looks like.

Base types need no further structure:

syntax baseTypeIR =
  | INT `< nat `>
  | BIT `< nat `>
  | BOOL
  | MATCH_KIND

Data types are user-defined and carry their full field list:

syntax structTypeIR = STRUCT typeId `{ fieldTypeIR* `}
syntax headerTypeIR = HEADER typeId `{ fieldTypeIR* `}

Structs and headers carry both a typeId (the name the programmer gave them) and the full field list fieldTypeIR*. The name matters for equality, as discussed in Type Equality below.

Object types represent instantiable components (parsers, controls, packages, externs, tables):

syntax parserObjectTypeIR  = PARSER  typeId `( parameterIR* `)
syntax controlObjectTypeIR = CONTROL typeId `( parameterIR* `)
syntax packageObjectTypeIR = PACKAGE typeId `( parameterIR* `)
syntax externObjectTypeIR  = EXTERN  typeId externMethodTypeDefEnv
syntax tableObjectTypeIR   = TABLE   typeId

Each carries its name and its parameter list (or method map, for externs).

Type Equality: Type_eq

Type_eq decides whether two internal types are the same.

relation Type_eq:
  typeIR ~~ typeIR
  hint(input %0 %1)

Read typeIR_a ~~ typeIR_b as: “typeIR_a and typeIR_b are equal types.”

Base types

rule Type_eq/baseTypeIR:
  baseTypeIR ~~ baseTypeIR

Two base types are equal if and only if they are syntactically identical. INT<8> is not equal to INT<16>, and BOOL is not equal to BIT<1>. Pattern matching handles this: the same variable baseTypeIR appears on both sides, so the rule only fires when the two sides are the same term.

Structs and headers

rule Type_eq/structTypeIR:
  (STRUCT typeId `{ _ `}) ~~ (STRUCT typeId `{ _ `})

rule Type_eq/headerTypeIR:
  (HEADER typeId `{ _ `}) ~~ (HEADER typeId `{ _ `})

Two struct/header types are equal when they share the same typeId. The field lists on both sides are wildcarded with _ and ignored entirely.

This is nominal equality, not structural equality. If two independent structs happen to have identical fields but different names, they are not considered equal by this relation. P4 treats struct and header types as distinct by name; the spec reflects this by comparing type names rather than structural content.

Externs

rule Type_eq/externObjectTypeIR:
  (EXTERN typeId _) ~~ (EXTERN typeId _)

Extern types are also compared by name only. As with structs, the global type environment guarantees that the same name always resolves to the same extern declaration.

Parsers, controls, and packages

rule Type_eq/parserObjectTypeIR:
  (PARSER _ `( parameterIR_a* `)) ~~ (PARSER _ `( parameterIR_b* `))
  -- (ParameterType_eq: parameterIR_a ~~ parameterIR_b)*

rule Type_eq/controlObjectTypeIR:
  (CONTROL _ `( parameterIR_a* `)) ~~ (CONTROL _ `( parameterIR_b* `))
  -- (ParameterType_eq: parameterIR_a ~~ parameterIR_b)*

rule Type_eq/packageObjectTypeIR:
  (PACKAGE _ `( parameterIR_a* `)) ~~ (PACKAGE _ `( parameterIR_b* `))
  -- (ParameterType_eq: parameterIR_a ~~ parameterIR_b)*

Parsers, controls, and packages are compared structurally: their names (the _) are ignored, and equality holds when the parameter lists are equal pairwise under ParameterType_eq.

This contrasts with how structs and headers are compared: a type name is a declaration, so two values have the same type only if they were declared under that exact name. Parsers and controls are different: a control type declaration describes an interface, and any control block that satisfies that interface is a valid implementation. The name of the implementing block is irrelevant; what matters is that its parameter list matches.

Consider:

// control type declaration (in nano_model.p4)
control filter(inout Header hdr, out bool accept);

// control block declaration (user-written)
control Filter(inout Header hdr, out bool pass) {
    apply { pass = true; }
}

// package instantiation
NanoSwitch(MyParser(), Filter()) main;

filter and Filter are two different names, yet Filter is a valid implementation of the filter interface because their parameter lists match. Structural comparison is what captures this.

Parameter equality

All three iterated premises above delegate to ParameterType_eq:

rule ParameterType_eq:
  (direction typeIR_a _) ~~ (direction typeIR_b _)
  -- Type_eq: typeIR_a ~~ typeIR_b

Two parameters are equal when they share the same direction and have equal types under Type_eq. The parameter name (the trailing _) is ignored.

Tables

rule Type_eq/tableObjectTypeIR:
  (TABLE typeId) ~~ (TABLE typeId)

Tables are compared by name only, consistent with structs and externs.

Exercise

Branch: exercise/3.2

Check out the exercise branch in the spec submodule:

git -C nano-p4/spec checkout exercise/3.2

Run the following test to observe the failure:

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.2.p4

The test program declares two variables with the same struct type and tries to assign one to the other. The checker should accept this, but it rejects it.

Find the bug/missing rule in 5.02-typing-type.watsup and fix it accordingly.

When you are done, restore the original branch:

git -C nano-p4/spec checkout main