elipl/set_types.md

Tilly Set-Theoretic Type System: Design and CDuce Reference

Objective:

Implement a CDuce-style set-theoretic type system in Elixir for the Tilly compiler. This document outlines the core principles adapted from CDuce and the planned Elixir implementation strategy.

Okay, let's lay out a revised and extensive implementation plan for adapting Tilly to a set-theoretic type system.

Overarching Concern:

• Bare Maps for Extensibility: We will prioritize using bare Elixir maps for representations like Type Descriptors (Descr) instead of structs. This approach maintains flexibility for future extensions, allowing new fields to be added without altering struct definitions. BDD node structures themselves will be represented by simple Elixir terms (atoms or tuples).

I. Foundational BDD and Type Descriptor Infrastructure (New Modules)

This phase focuses on building the core components for the set-theoretic type system. These will primarily be new modules. The typing_ctx map will be a central piece of data, passed through most functions in this layer, containing the necessary stores and configurations.

1. Tilly.BDD.Node (Conceptual Definition & Basic Helpers):

   • Node Structures: We define the canonical Elixir terms representing BDD nodes:
     • true: The atom representing the universal set BDD.
     • false: The atom representing the empty set BDD.
     • {:leaf, leaf_value_id}: Represents a leaf node. leaf_value_id can be any term, its interpretation depends on the ops_module (e.g., a boolean for simple sets, or another BDD node ID for nested structures).
     • {:split, element_id, positive_child_id, ignore_child_id, negative_child_id}: Represents an internal decision node.
       • element_id: The value being split upon.
       • positive_child_id, ignore_child_id, negative_child_id: IDs of other BDD nodes in the store.
   • Smart Constructors (Low-Level): This module might contain very basic helper functions for creating these structural tuples if needed, but the primary "smart" construction (with simplification and interning) will occur in Tilly.BDD.Ops and use Tilly.BDD.get_or_intern_node.
   • Purpose: To establish the fundamental building blocks of BDDs.

2. Tilly.BDD (BDD Store Management):

   • BDD Store (typing_ctx.bdd_store): This will be a map within the typing_ctx responsible for hash-consing BDD nodes. It will contain:
     • nodes_by_structure: A map where keys are {logical_structure_tuple, ops_module_atom} and values are unique_node_id (integer). The ops_module_atom is crucial for canonicalization, ensuring structurally identical nodes intended for different operational semantics are distinct.
     • structures_by_id: A map where keys are unique_node_id and values are %{structure: logical_structure_tuple, ops_module: ops_module_atom}. This allows retrieval of both the node's structure and its associated operations module.
     • next_node_id: An integer for generating new unique node IDs.
   • Key Function: get_or_intern_node(typing_ctx, logical_structure_tuple, ops_module_atom):
     • Takes the current typing_ctx, the node's structural representation (e.g., {:split, ...}), and the atom identifying its operations module (e.g., :integer_bool_bdd_ops).
     • Checks typing_ctx.bdd_store.nodes_by_structure for an existing node.
     • If not found, creates a new unique_node_id, updates both nodes_by_structure and structures_by_id, and increments next_node_id.
     • Returns {new_typing_ctx, node_id}.
   • Helper Functions:
     • get_node_data(typing_ctx, node_id): Returns %{structure: ..., ops_module: ...}.
     • is_false_node?(node_id, typing_ctx), is_true_node?(node_id, typing_ctx).
     • Functions to extract parts of a node structure if needed (e.g., get_element_from_split_node_id(typing_ctx, node_id)).

3. BDD Operations Modules (e.g., Tilly.BDD.IntegerBoolOps, Tilly.BDD.AtomSetOps, Tilly.BDD.RecursivePairOps):

   • Purpose: These modules provide the specific logic for how BDD elements are compared/hashed and how leaf values are combined/negated for a particular kind of BDD. They are the "plugins" for the generic BDD algorithms.
   • Interface Convention (Informal or via Elixir behaviour): Each module will implement a consistent set of functions:
     • compare_elements(elem1, elem2): Returns :lt, :eq, or :gt.
     • equal_element?(elem1, elem2): Returns boolean.
     • hash_element(elem): Returns an integer.
     • empty_leaf(): Returns the leaf value for emptiness.
     • any_leaf(): Returns the leaf value for universality.
     • is_empty_leaf?(leaf_val): Returns boolean.
     • union_leaves(leaf1, leaf2, typing_ctx): Combines leaves for union. May need typing_ctx for recursive BDD operations if leaves are BDD IDs.
     • intersection_leaves(leaf1, leaf2, typing_ctx): Combines for intersection.
     • negation_leaf(leaf, typing_ctx): Negates a leaf.
   • Example (Tilly.BDD.IntegerBoolOps):
     • compare_elements/2: Uses standard integer comparison.
     • empty_leaf/0: Returns false.
     • union_leaves/3: fn l1, l2, _ctx -> l1 or l2 end.

4. Tilly.BDD.Ops (Generic BDD Algorithms):

   • Core Operations: Implements union_bdds(node1_id, node2_id, typing_ctx), intersection_bdds/3, negation_bdd/2, difference_bdd/3.
     • These functions take BDD node IDs and the typing_ctx.
     • They fetch node data (structure and ops_module) using Tilly.BDD.get_node_data/2.
     • They use apply(ops_module, :function_name, args) to invoke element/leaf operations from the appropriate ops_module.
     • They return a node_id for the resulting BDD.
   • Smart Constructors (Algebraic): Implements functions like leaf(leaf_value, ops_module, typing_ctx) and split(element, p_id, i_id, n_id, ops_module, typing_ctx).
     • These are the CDuce-style smart constructors that apply simplification rules (e.g., if p_id == n_id in split, simplify to p_id ++ i_id).
     • After simplification, they call Tilly.BDD.get_or_intern_node/3 to get/create the canonical node ID.
     • Example split/6:

       def split(x, p_id, i_id, n_id, ops_module, ctx) do
         # Apply simplification rules based on CDuce bdd.ml, e.g.:
         # if i_id represents True for ops_module, return True node_id.
         # if p_id == n_id, result is union_bdds(p_id, i_id, ctx_with_ops_module).
         # ... other rules ...
         # If no simplification, create logical_structure:
         logical_structure = {:split, x, p_id, i_id, n_id}
         Tilly.BDD.get_or_intern_node(ctx, logical_structure, ops_module)
       end
       

5. Tilly.Type (Type Descriptor Definition):

   • Descr Map Structure: Defines the structure of a Type Descriptor map. This map holds IDs of canonical BDDs for each basic kind of type. Example:

     %{
       atoms_bdd_id: node_id,    # BDD for specific atoms (elements: atoms, leaves: booleans)
       integers_bdd_id: node_id, # BDD for specific integers (elements: integers, leaves: booleans)
       strings_bdd_id: node_id,  # BDD for specific strings
       tuples_bdd_id: node_id,    # BDD for pairs/tuples. Elements might be type vars or first component types; leaves might be BDD IDs for rest of tuple.
       maps_bdd_id: node_id,  # BDD for maps. Elements might be labels or key types; leaves might be BDD IDs for value types or record structures.
       functions_bdd_id: node_id,# BDD for functions.
       # ... other kinds as needed, e.g., for abstract types ...
       absent_marker_bdd_id: node_id # BDD representing if 'absent' or 'nil' is part of the type
     }
     

   • Helper Functions: May include functions like empty_descr(typing_ctx) which creates a Descr map where all *_bdd_id fields point to the false BDD node ID, and any_descr(typing_ctx) where they point to true BDDs (configured with appropriate ops_module for each field).

6. Tilly.Type.Store (Type Descriptor Interning):

   • Type Store (typing_ctx.type_store): A map within typing_ctx for interning Descr maps.
     • descrs_by_structure: Maps a canonical Descr map (where all BDD IDs are already canonical) to a unique_descr_id (integer).
     • structures_by_id: Maps unique_descr_id back to the canonical Descr map.
     • next_descr_id: For generating new unique Descr IDs.
   • Key Function: get_or_intern_descr(typing_ctx, descr_map):
     • Ensures all *_bdd_id values in descr_map are canonical.
     • Looks up descr_map in descrs_by_structure.
     • If not found, creates a new ID, updates stores, and increments next_descr_id.
     • Returns {new_typing_ctx, descr_id}.

7. Tilly.Type.Ops (Operations on Type Descriptors):

   • Set Operations: Implements union_types(typing_ctx, descr1_id, descr2_id), intersection_types/3, negation_type/2.
     • These operate on Descr IDs.
     • Example union_types/3:
       1. Fetch descr_map1 and descr_map2 from typing_ctx.type_store using their IDs.
       2. For each corresponding field (e.g., atoms_bdd_id):
          • Call Tilly.BDD.Ops.union_bdds(descr_map1.atoms_bdd_id, descr_map2.atoms_bdd_id, typing_ctx). The typing_ctx is passed along; the ops_module for these BDDs is retrieved from the bdd_store by union_bdds.
       3. Construct a result_descr_map using the new BDD IDs for each field.
       4. Intern this result_descr_map using Tilly.Type.Store.get_or_intern_descr(typing_ctx, result_descr_map) to get the final result_descr_id.
       5. Return {new_typing_ctx, result_descr_id}.
   • Construction Helpers: Functions to create specific types, e.g., create_integer_type(typing_ctx, integer_value) or create_atom_type(typing_ctx, atom_value). These would construct the appropriate Descr map (with a BDD representing only that literal) and intern it.

II. Adapting Existing Typer Modules

This phase involves refactoring existing modules to use the new BDD-based type infrastructure. The typing_ctx (initialized with empty stores) will be threaded through all relevant type-checking functions.

1. Til.Typer.Types (Major Refactor):

   • Functions like get_primitive_type(:integer) will now use Tilly.Type.Ops or dedicated constructors (e.g., Tilly.Type.integer_singleton(typing_ctx, value) or Tilly.Type.integer_any(typing_ctx)) to get/create an interned Descr ID.
     • For example, get_primitive_type(:integer) would return the Descr ID for the type "all integers". This Descr would have its integers_bdd_id pointing to a true BDD (interned with an ops_module like :integer_bool_bdd_ops), and other fields like atoms_bdd_id pointing to false BDDs.
   • The concept of predefined type maps (as Elixir maps with :type_kind) is replaced by predefined canonical Descr IDs, likely initialized once and stored or retrieved via helper functions.

2. Til.Typer.Interner (Major Refactor/Integration):

   • Its current role of interning Elixir map-based type representations is entirely replaced by Tilly.BDD.get_or_intern_node and Tilly.Type.Store.get_or_intern_descr.
   • populate_known_types will be responsible for initializing the typing_ctx by creating and interning the Descr IDs for fundamental base types (e.g., any, nothing, the general integer type, atom type). This involves creating the necessary BDDs (often just true or false BDDs for the respective fields in the Descr) with their appropriate ops_modules.

3. Til.Typer and Til.Typer.ExpressionTyper (Significant Refactor):

   • typing_ctx Threading: All type inference and checking functions will now take typing_ctx as an argument and return an updated typing_ctx along with their results.
   • infer_type_for_node_ast (or similar functions):
     • For literals (e.g., 123, :foo): Will call functions like Tilly.Type.Ops.create_integer_literal_type(typing_ctx, 123) which constructs a Descr map where integers_bdd_id points to a BDD representing only 123 (and other fields are empty BDDs), interns it, and returns the {new_ctx, descr_id}.
     • For operations that combine types (e.g., an if expression's branches have types descr_id_A and descr_id_B): Will use Tilly.Type.Ops.union_types(typing_ctx, descr_id_A, descr_id_B) to get the {new_ctx, result_descr_id}.
   • resolve_type_specifier_node:
     • For basic type names (Integer, Atom): Will fetch their canonical Descr IDs (e.g., from helper functions in Til.Typer.Types that retrieve pre-interned IDs).
     • For type expressions like (or TypeA TypeB): Will recursively call itself to get descr_id_A and descr_id_B, then use Tilly.Type.Ops.union_types(typing_ctx, descr_id_A, descr_id_B). Similarly for (and ...) and (not ...).
   • The type_id field in AST nodes will now store the Descr ID (an integer) obtained from Tilly.Type.Store.

4. Til.Typer.SubtypeChecker (Complete Rewrite):

   • is_subtype?(typing_ctx, descr_a_id, descr_b_id):
     1. {typing_ctx, descr_not_b_id} = Tilly.Type.Ops.negation_type(typing_ctx, descr_b_id).
     2. {typing_ctx, intersection_id} = Tilly.Type.Ops.intersection_types(typing_ctx, descr_a_id, descr_not_b_id).
     3. Tilly.Type.Ops.is_empty_type?(typing_ctx, intersection_id).
   • Tilly.Type.Ops.is_empty_type?(typing_ctx, descr_id):
     1. Fetches descr_map from typing_ctx.type_store.
     2. Checks if all *_bdd_id fields in descr_map point to the canonical false BDD node ID (by calling Tilly.BDD.is_false_node?/2 for each).

III. Handling Specific Type Kinds from project.md

The existing type kinds in project.md will be mapped to specific configurations of Descr maps and their constituent BDDs.

• Primitive Types: %{type_kind: :primitive, name: :integer} becomes a canonical Descr ID. For "all integers", its integers_bdd_id points to a true BDD (interned with ops_module: :integer_bool_bdd_ops), and other fields (like atoms_bdd_id) point to false BDDs.
• Literal Types: %{type_kind: :literal, value: 42} becomes a Descr ID. Its integers_bdd_id points to a BDD representing only the value 42 (e.g., a single Split node leading to a true leaf, or a more optimized representation if available), and other fields are false BDDs.
• Union/Intersection/Negation Types: These are no longer explicit type_kinds in the Descr map itself. They are the result of applying Tilly.Type.Ops.union_types, intersection_types, or negation_type to other Descr IDs. The resulting Descr ID represents the union/intersection/negation.
• Function, List, Tuple, Map Types:
  • These will be represented by Descr maps where the corresponding BDD field is non-empty and structured appropriately. For example, a list of integers would have a non-empty pairs_bdd_id.
  • The BDDs for these types will be more complex:
    • Lists/Tuples (pairs_bdd_id): The BDD might split on the type of the first element, with leaves being BDD IDs representing the type of the rest of the list/tuple. The ops_module for this BDD would handle element types and BDD ID leaves (e.g., :recursive_pair_ops).
    • Maps/Records (records_bdd_id): This BDD would split on record labels or key types. Leaves could be BDD IDs for value types or more complex record structures. This is a significant area requiring careful design inspired by CDuce's record BDDs. The project.md details on known_elements and index_signature will need to be encoded into the BDD structure and its ops_module.
    • Functions (functions_bdd_id): BDDs might split on argument types or arity, with leaves representing return types (possibly as BDD IDs).
  • This is an advanced stage. Initially, constructing these might involve specific helper functions in Tilly.Type.Ops (e.g., create_list_type(typing_ctx, element_descr_id)).

---