Repository navigation
A complete type system for HQL - #4
Merged
Merged
Conversation
The example lists open tasks by priority and architecture decisions by date. A metadata leaf is Option<Data>, which is not Orderable, so each sort key is read with a typed match; a partial record type over card metadata replaces that match in issue 0027, now on the todo column.
Twenty-three proposed programs under examples/mighty-types/, three workspace modules under its lib/ root, issue 0028 with the milestones, and the corpus harness skipping module roots and accepting a modules: header. The proposal gains the prelude.hql model: std/prelude.hql is the standard import list and an extension's prelude.hql is its constructor.
…lues A type statement with fields declares a record the program constructs by field name or position, reads with a dot, matches by type inside a union, and prints as the call that builds it. A bodiless type is a tag. The lattice is held per program: checking extends it and evaluation reads values against it. Function types reach eight parameters, and an integer literal may receive a call, 7.max(3). A named function passed to map now yields elements at the function's result type, which fixes sum over such a map.
value.f(args) calls f with the value as its first argument, resolved among the visible modules by the receiver's type; module.f(x) qualifies one. The prelude is the import list of std/prelude.hql. Two modules may declare one name, told apart at the call by the input, so string.contains and the core's contains coexist. str and fmt join the prelude, fmt with variadic arguments; a step name stands as a function value, map(str); Pair<A, B> is the element of zip, enumerate, entries and join; argument lists take a trailing comma. Fourteen more Mighty Types programs are valid-now.
… module ok(v) and err(e) build a result, ok(p) and err(p) match one and a match must cover both, map keeps a failure, and the result module in the prelude has is_ok, is_err, ok, err, unwrap_or, unwrap_or_else, map_err, and_then and or_else. Example 08 is valid-now.
trait declares a contract with Self for the implementing type and default bodies; impl Name for Type provides it once per trait and type, with the trait's defaults for what it leaves out. A receiver call reaches a trait's function implemented for the receiver's type or promised by a T : Trait bound, which is checked at every call. Arithmetic over a declared type resolves through Add, Sub, Mul, Div and Rem, equality through Eq, and a type implementing Ord is Orderable, its compare deciding <, sort, min and max. Dispatch is on the value's own type at run time. The binary runs its host on a large-stack thread and the evaluator keeps its heavy arms out of the expression frame, so recursion a few thousand calls deep holds. Examples 09 to 11 are valid-now.
…ceiver modules import a.b as c makes one module visible under a local name; a builtin module answers to its canonical path (io.net) and its one-word name, and a workspace module is an HQL file found by its position under a module root: hql.toml [modules] roots, --modules on the command line, or the corpus header. A module file declares functions, types, traits and implementations, may open with module for T to make its self functions receiver functions, and may import for itself. Imports sit at the head of a unit, two imports may not share a local name, and a module imports no cycle. Examples 18, 19 and 23 are valid-now.
…nd split Imported where it is used; a pattern that does not parse fails at the call. Example 20 is valid-now, which completes the Mighty Types corpus.
…ext is a String Adopts encode-decode-format.md as HQL-0024 part 7: every format narrows Format and none narrows String, format(x, F) and the shorthands give a String that keeps its format for presentation, formatted text asked for in another format is that String encoded again, and Lines and JsonLines frame records by line for source, tap and sink. std/format.hql declares the codec contracts Decoder<F, T> and Encoder<T, F>. HQL-0017 is superseded in that one rule; the cards, the book and the changelog say so.
External declarations, fn trim(self) : String with no body, are the contract of a module an extension implements; std/string.hql, seq.hql, math.hql, option.hql, result.hql and regex.hql declare theirs, and a test holds each to its extension function by function. io/init.hql is io/mod.hql. The type system, naming, extensions, std-lib, design status and presentation cards, the std README, the proposals index (HQL-0025 reserved for the execution context) and issue 0028 record what landed.
…'s general-purpose core Every program in the chapter runs under the book harness, two of them from the Mighty Types module root; hql --modules <dir> before the command parses. The README describes formats as a category of their own and the records, unions, results, receiver calls, traits and modules the language now has.
… one value A .txt or .log path implies Lines; Text reads the whole document; lines and jsonlines encode one record per line; sink writes a single value as one document beside a stream of them. Two Mighty Types programs read a file as lines and write another whole with target, and append to a file's end with sink; the corpus harness runs a program that writes in a temporary copy of its example (io: sandbox), so a test run leaves the checkout as it was.
… binary formats sink keeps its Iterable input and target writes one value whole, as HQL-0021 has them; the records that said one would give way to the other are corrected. Example 15 holds the sorted union beside its texts at Data, as the upd commit left it. Issue 0029 takes binary formats and codecs provided outside the binary. The extensions card states that HQL declares a module's interface and the extension implements it.
…hat provide them Every builtin extension carries its descriptor's provides, the canonical modules it implements; once per process, before the first program, binding holds each external declaration of std/ to the operation of that name, its arity and its result constructor, and refuses every program on a mismatch, naming the module, the declaration and the extension. The extensions card documents the wiring with a worked example over a function, a type and a trait; part 9 records the first stage as done in part.
…ions std/core.hql declares the built-in types' native implementations as bodyless impl headers, binding pairs each header with a native body, and one implementation per trait and type holds across std, imports and the program. A standard module's .hql declaration is its functions' signature. The prelude gains the string functions from issue 0031, replace splits into replace_all and replace_first, and HQL-0026 with issue 0032 opens generic traits.
…erations Traits take type parameters (HQL-0027, issue 0032): trait Index<T>, impl<T> Index<T> for Ring<T>, a bound naming a generic trait, and xs[i] over a declared type as its xs.at(i); the codec contracts are the traits Decoder<T> and Encoder<T>. The generic traits corpus shows each. A name declared more than once in a std/ module is one operation with several signatures, and a call takes the first its input and arguments fit. S : Seq<T> holds the input at its own type, F<_> : Iterable<_> rebuilds its constructor as F<U>, and Type<U> takes a type name. The core's collection operations, map and filter over an Option and map over a Result, seq's reverse, distinct, take_while, drop_while, min_by, max_by, with, without, intersection and difference, and math's abs, pow and sign take their signatures from their declarations; the Input, Prefix, Reorder, Image, Number and Fold output rules and the Ordering argument kind are gone. Issue 0033 tracks what is still written in Rust. HQL-0028 drafts import units, the program module and declaration visibility.
…ented, issue 0030 closed - Data trees convert to program-declared records by shape (is, of_type, match arms) - fmt keeps a native signature until a variadic-over-any parameter exists - type aliases for three signatures clippy flags as too complex
…ly parameters; format and fmt declared in HQL - '/' and '*' markers in external declarations; shadowed overloads refused at binding - steps lifted over absence evaluate to absence - collect(for=) refused by its declaration; Output::Finite removed - M<_, _> constructor parameters; narrowing filter declared via Is<U> - examples/overloads corpus; issue 0033 done
- constructors declared as fn beside their types and bound against the Rust table - fn E(..) : E beside type E; constructor forms overload by first parameter - Data(s, F) parses text by construction for Json, JsonLines, Yaml, Csv - generic variadics infer their type parameter from trailing arguments
…6 implemented - Kind::Slice; Range record and Slice trait with String, Seq and Data impls - a slice keeps the receiver's type; stream slices are lazy - String is indexed; negative positions count from the end - examples/slicing promoted, invalid cases added
…ntities - value.f() reaches only declarations with self; overloads agree on receivers - effectful fn marks external declarations; binding checks the Rust marking - binding allocates module and declaration identities; checked steps carry them - io and logging operations declared in std
…to give - source and tap typed from a binding's declared element type - live reads decode per document; mismatches name the field - HQL-0021 spec synced with std/io/mod.hql; accepted, implemented in part
…-0028 implemented - private before fn, type, trait, alias and binding; internal reserved - modules check against the standard prelude only and never see host bindings - cards and graph move to the program module - an imported receiver name two modules provide is an ambiguity
xs | fork { a = …, b = … } is a pipeline step: every branch is a pipeline
over the same input, evaluated once, and the step's value is the record of
the branch results, a closed record type named by its branches,
{a: A, b: B}. { a, b } = … binds the branches by name. Over a Stream each
branch is a stream in the upstream's order.
A tap of a file is a shared reading, opened on first use and read once, so every later traversal of the stream, the branches of a fork among them, replays it, as standard input and sockets already did. A pure branch of a bound fork that no later statement reads is not run; an effectful one is. A configured source bound once counts its elements against max_elements once.
fork { accepted = oks(), rejected = errs() } over a List, Seq and Stream
of results, each value on one side and each side in source order, and a
live file validated and forked read once. Results have no split of their
own.
errs() written with sink reads back with | Invalid in a later run, and a repair from e.value runs through another validate and fork. Message<T> is not a type yet: HQL-0033 states that provenance sits in an envelope beside Invalid, or as extra fields on the open record, until it is.
The predicate partition, a pair of the values a predicate accepts and rejects, is removed: those are two branches of a fork with complementary filters. partition(by = f) over a Seq or a Stream keeps the input's type and every value, is declared with the partition shape so the planner opens a stage at it, and on the local backend passes the values on in order. HQL-0037 is accepted.
a | merge(b) interleaves two streams, one value from each in turn, a | zip(b) pairs them by position and a | concat(b) produces one and then the other, each a lazy traversal that reads its inputs a portion at a time. merge keeps its map form and is resolved by argument type, or by the expected function type where it is named as a value; over a List, Seq, Set or Table it is a type error naming concat or union, and f = merge alone is an ambiguous reference.
A planned step names its topology, fan-out for fork and tee and fan-in for merge, zip, concat and the joins, and a fan-out lists its branches, each by name with its own steps, as the stages that read its input. hql plan prints both and its JSON adds topology and branches. merge and concat written as steps are step nodes.
HQL-0033's section on retry states the form first: xs | retry(operation, attempts = n, when = …) is elementwise over a collection or a stream, and invokes the operation for each value again while it fails with an error when accepts, up to attempts invocations; the last failure stands as an ordinary err, and no time passes between invocations. retry takes the operation, never a finished Result.
HQL-0032's runtime failure policies, stream validation, dead-letter handling and validation result, and its open questions on them, are marked superseded by HQL-0033 where they conflict: each policy is a pipeline over Result<T, Invalid>. Issue 0043 records its stream policies as closed by E1 to E5. HQL-0033 is accepted and implemented, every item of its test plan covered. Issue 0045 moves to doing.
…5 V2 HQL-0034's placeholders are stated, then built. std/validators.hql is the standard library's first module written in HQL: a program imports it by name, and it is loaded as a workspace module is, before the module roots. It declares Email, for text, and NonEmpty, implemented for text and for lists. A validator for several types is one impl per type and is named in a rule; a field declared with one is refused. A field declared f: V reports the violation Contract.f with the text f: V. HQL-0034 is accepted and implemented.
HQL-0035 states the form first: a configured source maps its fields under [sources.<id>.fields.<field>] with name or a dotted path, type, position, read, write and absent, and keys its kind's extension owns in a subtable named by the kind. The configuration loads each into a FieldMapping whose unwritten properties are left to the format, and refuses a malformed one with the vault.
HQL-0035 states the resolver first. src/boundary.rs merges a format's defaults, a source's configuration and an invocation's override by field-level recursive override, each effective property keeping the layer it came from, and reports every boundary error at once as a structured diagnostic: an undeclared or unmapped field, a shared or missing external field, and an external type with no decoder. The format tables give each kind's default external type and absent representations.
source("id") and tap("id") read where a Seq of a declared record is
expected go through the source's boundary: each field reads its external
field, a nested JSON path included, and a SQLite source selects only the
columns the boundary reads. A CSV header and a table's columns are checked
against the boundary before any element decodes, and a configured element
type is checked against it when the program is checked.
HQL-0035 states the rules first. A field's absent lists the external representations of no value: csv an empty cell or a missing column, json, json_lines and yaml a missing key or null, sqlite NULL, unless the boundary says otherwise per field. An optional field holding one is absent; an unlisted null is refused, and unlisted empty text is read as text; a required field holding one is missing.
… 0045 B5 HQL-0035 states the policy first. A Decimal field is a JSON and YAML string by default and reads the string's digits; a number there reads with its digits too. A representation that may not keep a value, a Decimal as a JSON number, a CSV float or a SQLite REAL or NUMERIC, is a boundary error unless the field writes lossy = true. Closes issue 0042's open item.
HQL-0035's sections on configured targets and write modes replace the
placeholder. xs | target("id") writes a Table<R> or a sequence of a
declared record through the source's boundary, to CSV, JSON, JSON Lines,
YAML or SQLite: the fields it writes under their external names, in
position order, each in its external type. The source's mode, create,
append or replace, says what a write does with what the target holds.
Binding allows one native signature to hold to several declarations where
one argument is a choice, as target(endpoint) and target(id) are. Closes
issue 0044's SQLite item.
HQL-0035 states the policy first. A source's strictness decides what a read does with an external field no HQL field reads, and never the HQL type's openness: compatible, the default, passes it to the type; open does not read it; warn does not read it and reports it once per read; strict refuses it. A table's unread columns are judged before any row.
…ue 0045 B8 HQL-0035 states the command first. hql boundary <file> <id> [--as T] prints a configured source's effective boundary for a type the file declares: its kind, strictness and write mode, and per field its external field, both types, position, read and write, and what reads as absent, each with the layer it comes from; --envelope json writes the same. A boundary that does not resolve prints every boundary error and exits 1. Issue 0045 is done.
…ue 0046 std/ is the builtin package: prelude.hql, the package's global space, and one folder per module with its declarations in mod.hql. Each module imports every module whose types or traits it writes, core included, and library::closure refuses an environment where a module writes a name it neither declares nor imports, imports a module listed after it or its own child, or where two modules declare one name; the listed order is the import graph's, so the graph is acyclic. Closing the modules exposed three cycles, each resolved by moving the shared type down: the collection types and their constructors and Format move to core, Card, HmdCard and MdCard to doc. An import of a standard module the runtime implements resolves, validators is checked without the package's prelude, and each module checks over its own import cone. Issue 0046 carries the trace log.
… HQL-0026, issue 0047 Cardinality has one name, size, with count(xs) its kept alias. A String declares size(self), its number of code points, and length is withdrawn; a String's positions are its code points. Decided, not yet implemented: issue 0047 carries the work.
…ages status HQL-0038 gathers how a function is declared, HQL-0039 the three kinds of trait and the validator positions, and HQL-0040 proposes io.fs: paths, folders, globs and entries. doc/status/packages.hmd audits the packages the binary carries: their extensions, modules and declarations.
std/ moves to lib/std/ with its history. lib/ holds the builtin packages, one folder each, their contracts bundled with the binary and their extensions compiled into it; std is the standard package among them. The binary embeds lib/std/, the checker locates a written module there, and the tests walk and check it. Every ADR, issue, card, model, status document, example and comment names lib/std/ where it named std/, and relative links reach it. Diagnostics keep naming a module as std/core, its package and name; released CHANGELOG entries keep their paths.
…0049, 0050 - Module files declare `module a.b` or `module a.b for T`; a misnamed module is refused (issue 0050). - Issue 0049: one extension per package, folding descriptors into `std` and `search`. - A String is always UTF-8 whatever encoding its text was read from; other external encodings are converted at the codec, and invalid bytes are a decoding error (values model, HQL-0024 formats and codecs).
…arch/; HQL-0038, issues 0048, 0051
A function body written `{ … }` without `=` is bindings followed by a final
expression, the function's value (HQL-0038, implemented). A block that yields
stays iterating. Trait and impl functions take a value block. The declared
result reaches the final expression through the bindings, as an expected type
now reaches every `match` arm. Refused at parse: yield with a final
expression, only bindings, `for` in a value block, an expression before the
last line. Cases under examples/functions/.
`lib/search/` holds contracts for the `lexical` and `semantic` modules of the
`search` package, loaded after std's modules; issue 0048 is done. Draft
HQL-0041: time, statistics, digests and encodings, randomness, environment.
…tive Data number equality - zip of a stream and a list, in either order, is a Seq traversed one position at a time; std declares the two mixed overloads. - A Decimal's significand is at most 512 bits and its scale at most 154. Out of range: a literal is a syntax error, to_decimal is none, arithmetic and round are a numeric overflow, checked before any digits are expanded. HQL-0031 updated. - Data Int and Float leaves compare through the same Decimal value as the Decimal comparisons do, so equality is transitive.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
HQL becomes a statically typed language end to end: a type system, a module system with a standard library declared in HQL, and typed data in and out.
ResultandOption,Decimal, structural types and contractslib/, withstddeclared in HQLfn, with an expression body or a block bodyDetails are in each proposal under
doc/proposals/, the issues underdoc/issues/, andCHANGELOG.md.