Module

Tramaj.Types

Package: purescript-tramaj-purs
Repository: lucasdicioccio/purescript-tramaj-purs

v4-types resolution, normalisation, canonical identity, and the closure and constraint machinery output needs (roadmap-to-v4 Phases 9, 10, 13, 14). Kept as its own module, the way Tramaj.Analysis is kept apart from Tramaj.Eval: this is a static pass over parsed programs, evaluates nothing, and its only dependencies are Tramaj.Ast and Tramaj.Analysis.

Scope, precisely: v4-types §9 says resolution and identity are the whole of what a type-aware analysis does before evaluation, and §3 fixes the one property every implementation must agree on — two spellings of the same type must produce the same string, and two different types must never collide.

Type parameters (roadmap Phase 10). A Ref's arguments (v4-types §1) come from nowhere in the surface syntax at the reference site — $msg.types.Envelope carries no bracketed application. They come instead from how msg was imported (§2): resolveLibBinding now returns the import's own params alongside its key and program, and a TLibRef resolves its RRef's arguments by intersecting those params' %-marked entries with the target library's own typeParams — the set Tramaj.Analysis.typeParams already computes without resolving anything. Each supplied argument is itself resolved under the importing program's own substitution, which is what makes forwarding (%ctx.payload, still a hole) and supplying (%Json, a closed argument) both fall out of the same code path.

Canonical ids and the library segment. v4-types §3's grammar renders a Ref as library ":" name with library inserted directly, and its worked examples (message:Envelope) do exactly that. But a library key is an arbitrary staticString (see Tramaj.Parser), and §3 requires injectivity: two distinct types must never render to the same string. Inserting an arbitrary key raw is safe on one side, because a name is always a colon-free identifier (see Tramaj.Parser's typeField) — reconstructing library and name from library <> ":" <> name is therefore unambiguous however many colons library itself contains. The side that is not safe is the program being resolved itself: a declaration with no importing library at all (an ordinary type X = ... at the root) needs some token for "no library", and no plain word is safe for that — a library can legally be named "root", or even "", since staticString forbids only a literal " or a backtick.

The fix follows from that one forbidden character: renderLibrary wraps every real library key in a literal pair of quotes (safe, and injective, precisely because a key can never itself contain one), and reserves the bare, unquoted word root for "this program, not a library" — a token no quoted key can ever equal, because a quoted key always begins with ". This is a deliberate departure from §3's unquoted worked examples, which never exercise a program that is not itself an importable library; nothing in the grammar there rules quoting out, and nothing else in it is injective without it.

Kept in lockstep with ../tramaj-hs/src/Tramaj/Types.hs.

#ResolvedType Source

data ResolvedType

The normal form a TypeExpr resolves to (v4-types §3). Structurally the same six shapes as TypeExpr, but every reference is now a genuine (library, name) pair rather than a name that might not exist, record fields and union arms are sorted by name, a RRef carries its resolved type arguments (roadmap Phase 10) rather than none, and a RRef never carries its referent's expansion — only resolveTypeExpr ever looks a name up, and it looks up only whether the name exists, never what it means.

Nothing as a RRef library means "declared in the program being resolved, not reached through an import" — see the module header for why this needs a real Maybe here rather than folding straight to a string: the encoding decision belongs to canonicalId alone, so a ResolvedType can be compared with == before any string is ever built.

Constructors

RPrim String
RArray ResolvedType
RRecord (Array (Tuple String ResolvedType))
RUnion (Array (Tuple String (Maybe ResolvedType)))
RRef (Maybe String) String (Array (Tuple String ResolvedType))
RVar (Array String)

Instances

#ResolvedConstraintArg Source

data ResolvedConstraintArg

A resolved !type-constraint argument: a type, or one of the four scalar shapes §5 allows — the type-realm counterpart of the already-evaluated Value a v3 constraint's argument becomes.

Constructors

Instances

#TypeError Source

data TypeError

v4-types §10's analysis errors.

Constructors

Instances

Eq TypeError
Show TypeError

#resolveTypeExpr Source

resolveTypeExpr :: Map String Program -> Program -> TypeExpr -> Either TypeError ResolvedType

Resolves a TypeExpr written somewhere in prog's own statement chain against prog's own scope: its own declarations for a bare TName, and the libraries in libs, reached through prog's own direct import(...) bindings, for a TLibRef (v4-types §9's $lib.types.X rule). No library in libs is evaluated — this walks parsed programs only, exactly as Tramaj.Analysis's deep analyses do.

Structural shapes (TArray, TRecord, TUnion) recurse; TVar passes through unchanged, since prog's own declarations carry no substitution of their own — only a reference to a parameterised library's declaration, resolved from the referencing side, ever supplies one (see resolveWith below). A TName or TLibRef resolves to a RRef that carries no expansion of the declaration it names — v4-types §3's "stop at declaration boundaries" clause, which is what keeps resolving a self-recursive declaration's own body from looping: a TName occurring inside Tree's own definition, referring to Tree itself, is checked for existence and rendered as a reference, never expanded.

#canonicalId Source

canonicalId :: ResolvedType -> String

v4-types §3's grammar, rendered. Assumes its argument is already normalised the way resolveTypeExpr produces it — fields, arms and arguments sorted by name — since this function only renders the order it is given; it does not sort.

#programTypeDecls Source

programTypeDecls :: Program -> Map String TypeExpr

Just the type declarations at the top of a program's own statement chain (v4-types §1.1), as a lookup table. This is typeDecls plus unlets plus programRoot, named once because every entry point below needs it and because a caller resolving several declarations from the same program should not repeat the walk.

#requireClosed Source

requireClosed :: ResolvedType -> Either TypeError ResolvedType

v4-types §4: a type reaching the root — an annotation (roadmap Phase 11), the closure of a program's own output (Phase 13) — must be closed. Everything else may stay partial; only a caller at the root need ever call this.

#checkTypeParamCollisions Source

checkTypeParamCollisions :: Program -> Either TypeError Unit

v4-types §10's TypeParamCollision, surfaced as a proper TypeError from Tramaj.Analysis.typeParamCollisions' plain Data.Set.Set. Reports the first colliding key found, the way every other check here reports one concrete failure rather than the whole set.

#typeClosure Source

typeClosure :: Map String Program -> Program -> Array ResolvedType -> Either TypeError (Map String ResolvedType)

The transitive closure of every type referenced from roots (v4-types §8): a record's field types, a union's payloads, and theirs, cut by id so a cycle terminates. Each RRef found is expanded exactly once — its declaration's own body, resolved under the substitution its arguments supply — which is the one place in this module a declaration boundary is crossed, because the output table is precisely where a host needs the definition behind an id, not merely the id.

Keyed by canonical id rather than by (library, name): two applications of the same generic library at different arguments are two different entries, exactly as §3 says they are two different types.

#eraseTypes Source

eraseTypes :: Map String Program -> Program -> Either TypeError Program

Rewrites every TypeAnnotate in prog into the Let plus Emit §7 specifies, resolving and closing its type first (an annotation whose type is partial is PartialType, per §7's own note that this is what makes erasure safe). Everything else is rebuilt unchanged; a TypeDecl and a resolved TypeEmit are left in place rather than stripped, since both are already inert to Tramaj.Eval.evalExpr — only TypeAnnotate produces something the evaluator cannot already ignore on its own.

Run once, up front, by every one of Tramaj.Eval's entry points (including a library, the moment it loads) rather than baked into evaluation itself — this is what keeps Value free of a type constructor and the whole §1.5 NotConcrete table untouched: by the time Tramaj.Eval.evalExpr runs, there is no TypeAnnotate left for it to match, and the byte-identical-to-annotations-deleted invariant §8 asks for follows from erasure alone, nothing evaluation-specific.

#typeReferences Source

typeReferences :: Map String Program -> Program -> Either TypeError (Set String)

Every type this program's own statement chain refers to, normalised to its canonical id (v4-types §9: "which it refers to, normalised") — every declaration, annotation and type-constraint argument's own type, resolved. An unresolvable reference is reported rather than skipped (§9's closing rule), which is exactly what resolveTypeExpr already does by returning an Either.

#deepTypeReferences Source

deepTypeReferences :: Map String Program -> Program -> Either TypeError (Set String)

typeReferences, following every transitively imported library — the type-realm analogue of Tramaj.Analysis.deepContextHoles.

#typeConstraints Source

typeConstraints :: Map String Program -> Program -> Either TypeError (Array (Tuple String (Array ResolvedConstraintArg)))

Every !type-constraint this program's own statement chain collects (v4-types §5), each argument resolved, deduplicated by name and already-resolved arguments — the same "first position kept" rule v3 §4 uses for value constraints, applied here because instantiation (substitution through a supplied argument) can make two differently written constraints collide the same way two differently written value constraints can.

#deepTypeConstraints Source

deepTypeConstraints :: Map String Program -> Program -> Either TypeError (Array (Tuple String (Array ResolvedConstraintArg)))

typeConstraints, over-approximated by following every transitively imported library (roadmap Phase 12/14) — the type-constraint analogue of Tramaj.Analysis.deepConstraintKinds: a constraint written inside a library that this program imports is reported whether or not the program's own evaluation would ever force that library, since a !type-constraint is never evaluated in the first place and so has no notion of "reached" to restrict it by.

#programTypeRoots Source

programTypeRoots :: Map String Program -> Program -> Either TypeError (Array ResolvedType)

Every TypeExpr sitting in a type-bearing position of prog's own syntax — a declaration's body, an annotation's type, a type constraint's type-marked arguments, an import's %-marked param (v4-types §2, §5, §7, §9) — resolved. This is typeReferences before the last step that throws the structure away down to a set of ids; Tramaj.Eval needs the structure itself to build the "types" output table's closure (v4-types §8, roadmap Phase 13), and typeReferences needs only the ids.

Modules: Tramaj.Analysis; Tramaj.Analysis.Card; Tramaj.Ast; Tramaj.Eval; Tramaj.Node; Tramaj.Parser; Tramaj.Types