Types | Soufflé • A Datalog Synthesis Tool for Static Analysis

Primitive Types

Soufflé provides two primitive types that form the foundation of every relation attribute definition.

Symbol type

The symbol type represents string values. Internally, symbols are stored in a global symbol table and referenced by ordinal numbers, making comparisons and joins efficient. Symbol literals are written in double quotes.

Number type

The number type represents signed 32-bit integer values. Numeric literals are written as standard integers and support arithmetic operations within rules.

Primitive type usage

When declaring a relation, each attribute is assigned a type. The following example declares a relation with two symbol attributes and one number attribute:

Relation	Attribute	Type
`my_rel`	first	`symbol`
`my_rel`	second	`symbol`
`my_rel`	third	`number`

Beyond Primitive Types

Soufflé supports richer type constructs that go beyond primitives, enabling more expressive and reusable type definitions.

Base Type

A base type defines a new named type that is semantically distinct from its underlying primitive. For example, declaring .type Person <: symbol creates a type Person that is a subtype of symbol. This allows the type checker to distinguish a Person from a plain symbol, preventing accidental mixing of semantically different values.

Union Types

Union types combine multiple base types into a single type that can hold any of the member values. They are declared with the | operator. For instance, .type Identifier = Person | Company defines Identifier as a type that accepts either a Person or a Company value. Union types are especially useful when a relation attribute needs to reference entities from different domains.

Domains

A domain type restricts the set of valid values using a companion relation. Values that appear in the domain's defining relation are considered valid members of the type. This provides a lightweight form of value-set constraint that is checked at runtime.

Sub-typing

Soufflé's type system supports a sub-typing hierarchy. A base type declared with <: is a subtype of its parent. Sub-types inherit the properties of their parent while remaining distinct for type-checking purposes. This hierarchy enables precise modelling of program entities in static analysis, such as distinguishing different categories of variables or heap objects.

← Back to Documentation

Soufflé's type system is a foundational component of its design, providing a static framework that enforces correctness at compile time. By requiring that every relation attribute be declared with a specific type, the tool catches inconsistencies early in the development process, before any analysis runs. This design choice reflects the broader philosophy of the language, which prioritizes safety and predictability in large-scale program analysis tasks. The static nature of types means that developers can reason about the structure of their data without runtime surprises, making Soufflé particularly well-suited for complex static analysis workflows where reliability is paramount. The type system thus serves as a first line of defense against logical errors.

The two primitive types—symbol and number—form the core of Soufflé's data model, each optimized for different kinds of analysis tasks. The symbol type handles string data through an efficient internal representation: all strings are stored in a global symbol table and referenced by ordinal numbers, which makes comparisons and joins extremely fast. This approach is especially valuable in program analysis, where large volumes of string data such as variable names, method signatures, and source file paths must be processed efficiently. Symbol literals are written in double quotes, making the syntax clear and unambiguous. The number type, meanwhile, provides signed integer arithmetic for quantities, indices, and other numeric data that commonly appear in analysis relations.

Beyond the primitive types, Soufflé supports user-defined types that allow developers to create more expressive and domain-specific data models. By defining subtypes of the primitive types, analysts can give semantic meaning to otherwise generic data, improving both readability and correctness. For example, a static analysis for Java taint tracking might define distinct types for source locations, taint tags, and method signatures, each backed by the symbol or number type but carrying their own semantic identity. The type checker then enforces that these types are not accidentally mixed, catching subtle bugs that could otherwise lead to incorrect analysis results. This layered approach to typing combines flexibility with strong compile-time guarantees.

The type system's design reflects Soufflé's broader goals of enabling rapid prototyping while supporting deep design space explorations in static analysis. By catching type errors early, the tool frees developers to focus on the logical structure of their Datalog programs rather than debugging runtime mismatches. This is especially important when using advanced features such as the Futamura projections and partial evaluation techniques that Soufflé supports, where the complexity of the compilation pipeline demands strong foundational guarantees. The static type system thus acts as a scaffolding that supports the construction of sophisticated, parallelized C++ analysis tools, ensuring that the generated code is not only fast but also correct from the ground up.