748f87636a
checkpoint failing test after fixing tests checkpoint checkpoint checkpoint re-work asd checkpoint checkpoint checkpoint mix proj checkpoint mix first parser impl checkpoint fix tests re-org parser checkpoint strings fix multiline strings tuples checkpoint maps checkpoint checkpoint checkpoint checkpoint fix weird eof expression parse error checkpoint before typing checkpoint checpoint checkpoint checkpoint checkpoint ids in primitive types checkpoint checkpoint fix tests initial annotation checkpoint checkpoint checkpoint union subtyping conventions refactor - split typer typing tuples checkpoint test refactor checkpoint test refactor parsing atoms checkpoint atoms wip lists checkpoint typing lists checkopint checkpoint wip fixing correct list typing map discussion checkpoint map basic typing fix tests checkpoint checkpoint checkpoint checkpoint fix condition typing fix literal keys in map types checkpoint union types checkpoint union type checkpoint row types discussion & bidirectional typecheck checkpoint basic lambdas checkpoint lambdas typing application wip function application checkpoint checkpoint checkpoint cduce checkpoint checkpoint checkpoint checkpoint checkpoint checkpoint checkpoint
100 lines
8.4 KiB
Plaintext
100 lines
8.4 KiB
Plaintext
|
|
|
|
The core idea is to replace the current map-based type representations with a system centered around **canonicalized type descriptors (`Tilly.Type.Descr`)**, where each descriptor internally uses **Binary Decision Diagrams (BDDs)** to represent sets of values for different kinds of types (integers, atoms, pairs, etc.).
|
|
|
|
Here's a plan for adaptation:
|
|
|
|
** overarching concerns:
|
|
|
|
- lets use bare maps instead of structs. Structs are closed, and I want to keep the option of adding new fields later by the user of the compiler
|
|
|
|
**I. Foundational BDD and Type Descriptor Infrastructure (New Modules)**
|
|
|
|
This phase focuses on building the core components described in `set_types.md`. These will mostly be new modules.
|
|
|
|
1. **`Tilly.BDD.Node` (New):**
|
|
* Define the Elixir tagged tuples for BDD nodes: `false`, `true`, `{:leaf, leaf_value_id}`, `{:split, element_id, p_child_id, i_child_id, n_child_id}`.
|
|
* include smart constructors
|
|
2. **`Tilly.BDD.Store` (New):**
|
|
* Implement the hash-consing mechanism for BDD nodes.
|
|
* This store will be part of the compiler `ctx` map.
|
|
* Key function: `get_or_intern_node(typing_ctx, logical_structure_tuple) :: {new_typing_ctx, node_id}`.
|
|
3. **`Tilly.BDD.ElementProtocol` and `Tilly.BDD.LeafProtocol` (New):**
|
|
* Define these protocols. Implementations will be provided for basic elements (e.g., atoms, integers for splitting) and basic leaves (e.g., booleans for simple set membership).
|
|
4. **`Tilly.BDD.Ops` (New):**
|
|
* Implement core BDD operations: `union_bdds`, `intersection_bdds`, `negation_bdd`, `difference_bdd`.
|
|
* These functions will take BDD node IDs and the `typing_ctx`, returning a new BDD node ID.
|
|
* Implement smart constructors for `Split` and `Leaf` nodes that use the `Tilly.BDD.Store` and apply simplification rules.
|
|
5. **`Tilly.Type.Descr` (New):**
|
|
* Define the Elixir struct. It will hold IDs of canonical BDDs for each basic kind (e.g., `:atoms_bdd_id`, `:integers_bdd_id`, `:pairs_bdd_id`, etc., mirroring CDuce's `descr` fields).
|
|
6. **`Tilly.Type.Store` (New or Replaces `Til.Typer.Interner` logic for types):**
|
|
* Manages the interning of `Tilly.Type.Descr` structs. A `Descr` is canonical if its constituent BDD IDs are canonical and the combination is unique.
|
|
* This store will also be part of the `typing_ctx`.
|
|
7. **`Tilly.Type.Ops` (New):**
|
|
* Implement `union_types(descr1_id, descr2_id, typing_ctx)`, `intersection_types`, `negation_type`. These operate on `Descr` IDs by performing field-wise BDD operations using `Tilly.BDD.Ops`, then interning the resulting `Descr`.
|
|
|
|
**II. Adapting Existing Typer Modules**
|
|
|
|
This phase involves refactoring existing modules to use the new infrastructure. The `typing_ctx` will need to be threaded through all relevant type-checking functions.
|
|
|
|
1. **`Til.Typer.Types` (Major Refactor):**
|
|
* Functions like `get_primitive_type(:integer)` will now use the new infrastructure to construct/retrieve an interned `Tilly.Type.Descr` ID for the integer type (e.g., a `Descr` where `integers_bdd_id` points to a "true" BDD for integers, and others are "false").
|
|
* The concept of predefined type *maps* will be replaced by predefined canonical `Descr` IDs.
|
|
2. **`Til.Typer.Interner` (Major Refactor/Integration with `Tilly.Type.Store` and `Tilly.BDD.Store`):**
|
|
* Its role in interning type *maps* will be replaced. The new stores will handle BDD node and `Descr` interning.
|
|
* `populate_known_types` will pre-populate the `typing_ctx` with canonical `Descr` IDs for base types like `any`, `integer`, `atom`, `nothing`.
|
|
3. **`Til.Typer` and `Til.Typer.ExpressionTyper` (Significant Refactor):**
|
|
* `infer_type_for_node_ast` (in `ExpressionTyper` or similar):
|
|
* For literals (e.g., `123`, `:foo`), it will construct the corresponding `Descr` ID (e.g., an integer `Descr` with a BDD representing only `123`).
|
|
* For operations that combine types (e.g., if an `if` expression's branches have types A and B, the result is `A | B`), it will use `Tilly.Type.Ops.union_types`.
|
|
* `resolve_type_specifier_node`:
|
|
* For basic type names (`Integer`, `Atom`), it will fetch their canonical `Descr` IDs.
|
|
* For type expressions like `(or TypeA TypeB)`, it will recursively resolve `TypeA` and `TypeB` to `Descr` IDs, then use `Tilly.Type.Ops.union_types`. Similarly for `(and ...)` and `(not ...)`.
|
|
* The `type_id` field in AST nodes will now store the ID of an interned `Tilly.Type.Descr`.
|
|
4. **`Til.Typer.SubtypeChecker` (Complete Rewrite):**
|
|
* `is_subtype?(descr_a_id, descr_b_id, typing_ctx)` will be implemented as:
|
|
1. `descr_not_b_id = Tilly.Type.Ops.negation_type(descr_b_id, typing_ctx)`.
|
|
2. `intersection_id = Tilly.Type.Ops.intersection_types(descr_a_id, descr_not_b_id, typing_ctx)`.
|
|
3. `is_empty_type(intersection_id, typing_ctx)`.
|
|
* `is_empty_type(descr_id, typing_ctx)` checks if all BDDs within the `Descr` are the canonical `False` BDD.
|
|
|
|
**III. Handling Specific Type Kinds from `project.md`**
|
|
|
|
The existing type kinds in `project.md` need to be mapped to the new `Descr` model:
|
|
|
|
* **Primitive Types:** `%{type_kind: :primitive, name: :integer}` becomes a canonical `Descr` ID where `integers_bdd_id` is "all integers" and other BDDs are empty.
|
|
* **Literal Types:** `%{type_kind: :literal, value: 42}` becomes a `Descr` ID where `integers_bdd_id` represents only `42`.
|
|
* **Union/Intersection/Negation Types:** These are no longer explicit `type_kind`s. They are results of operations in `Tilly.Type.Ops` combining other `Descr` objects.
|
|
* **Function, List, Tuple, Map Types:**
|
|
* These will be represented by `Descr` objects where the corresponding BDD (e.g., `functions_bdd_id`, `pairs_bdd_id` for lists/tuples, `records_bdd_id` for maps) is non-empty.
|
|
* The structure of these BDDs will be more complex, as outlined in CDuce (e.g., BDDs whose leaves are other BDDs, or BDDs splitting on type variables/labels). This is a more advanced step.
|
|
* Initially, `list_type(element_descr_id)` might create a `Descr` where `pairs_bdd_id` points to a BDD representing pairs whose first element matches `element_descr_id` and second is recursively a list or nil.
|
|
* The detailed map type representation from `project.md` (`known_elements`, `index_signature`) will need to be encoded into the structure of the `records_bdd_id`. This will be a complex part, drawing heavily from how CDuce handles record types with BDDs.
|
|
|
|
**IV. Parser (`lib/til/parser.ex`)**
|
|
|
|
* No immediate changes are required for the AST structure itself.
|
|
* If new syntax for type operations (e.g., `(or Int Atom)`) is desired directly in source code (as opposed to only being used by `resolve_type_specifier_node`), the parser will need to be updated to produce AST nodes that `resolve_type_specifier_node` can interpret.
|
|
|
|
**V. Documentation (`project.md`)**
|
|
|
|
* The "Type Representation" sections will need a complete overhaul to describe the new `Tilly.Type.Descr` and BDD-based system.
|
|
|
|
**Suggested Phased Approach:**
|
|
|
|
1. **Phase 0: Core BDD Infrastructure:** Implement `Tilly.BDD.{Node, Store, Ops, Protocols}`. Focus on BDDs for simple sets first (e.g., sets of atoms, integers).
|
|
2. **Phase 1: `Tilly.Type.Descr` and Basic Types:** Implement `Tilly.Type.Descr`, `Tilly.Type.Store`, and `Tilly.Type.Ops`. Implement construction of `Descr` IDs for primitives (`any`, `nothing`, `integer`, `atom`) and literals.
|
|
3. **Phase 2: Typer Integration for Primitives:** Refactor `Til.Typer.Types`, `Til.Typer.Interner`, and parts of `Til.Typer.ExpressionTyper` to use the new system for primitive and literal types. Update `resolve_type_specifier_node` for basic type names and simple `(or)`, `(and)`, `(not)` forms.
|
|
4. **Phase 3: Subtyping:** Implement the new `Til.Typer.SubtypeChecker`.
|
|
5. **Phase 4: Constructed Types (Iterative):**
|
|
* Start with pairs/tuples, then lists. Design their BDD representations within `Tilly.Type.Descr`.
|
|
* Tackle records/maps. This will be challenging and require careful mapping of `project.md`'s map features to CDuce-style record BDDs.
|
|
* Address function types.
|
|
6. **Phase 5: Advanced Features:** Polymorphism (type variables in BDDs), refinement types.
|
|
|
|
This is a substantial refactoring. The key is to build the BDD foundation correctly, as everything else will depend on it. The `typing_ctx` will become a critical piece of data passed throughout the type system.
|
|
|
|
> Tokens: 77k sent, 2.3k received. Cost: $0.12 message, $0.15 session.
|
|
|
|
#### /edit
|