From 93ddb288029ae3f4a54c72d122bbd81040f37d16 Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Wed, 24 Jun 2026 15:53:52 +0200 Subject: [PATCH 01/11] docs: setup user manual --- assets/icon.svg | 117 ++++++++++++++++++++++++++++++++++++++++++++++ docs/manual.typ | 27 +++++++++++ docs/template.typ | 96 +++++++++++++++++++++++++++++++++++++ 3 files changed, 240 insertions(+) create mode 100644 assets/icon.svg create mode 100644 docs/manual.typ create mode 100644 docs/template.typ diff --git a/assets/icon.svg b/assets/icon.svg new file mode 100644 index 0000000..56c81fa --- /dev/null +++ b/assets/icon.svg @@ -0,0 +1,117 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/docs/manual.typ b/docs/manual.typ new file mode 100644 index 0000000..5919e48 --- /dev/null +++ b/docs/manual.typ @@ -0,0 +1,27 @@ +#import "template.typ": TODO, project + +#let midas-version = toml("../pyproject.toml").project.version +#let head-ref = read("../.git/HEAD").split(":").at(1).trim() +#let commit-hash = read("../.git/" + head-ref).slice(0, 8) + +#show: project.with( + title: [Midas User Manual], + author: "Louis Heredero", + version: midas-version, + hash: commit-hash, + icon-path: path("../assets/icon.svg"), +) + += Introduction + +#TODO + += Installation + +#TODO + += Quick Start + +This chapter will give you the keys to quickly start using Midas in your project. + +#TODO diff --git a/docs/template.typ b/docs/template.typ new file mode 100644 index 0000000..78589f0 --- /dev/null +++ b/docs/template.typ @@ -0,0 +1,96 @@ +#import "@preview/modpattern:0.2.0": modpattern + +#let TODO = block( + width: 6em, + height: 3em, + stroke: red, + fill: modpattern( + size: (10pt, 10pt), + line( + start: (0%, 0%), + end: (100%, 100%), + stroke: gray.transparentize(60%) + 2pt, + ), + ), + align( + center + horizon, + text(fill: red, size: 1.5em)[*TODO*], + ), +) + +#let _render-header(version, hash) = { + let last-heading = query(heading.where(level: 1).before(here())).last(default: none) + let next-heading = query(heading.where(level: 1).after(here())).first(default: none) + + let current-heading = if next-heading != none and next-heading.location().page() == here().page() { + next-heading + } else if last-heading != none { + last-heading + } else { none } + + let chapter = if current-heading != none { + let body = current-heading.body + if current-heading.numbering != none { + let num = counter(heading).display(current-heading.numbering, at: current-heading.location()) + body = [#num #body] + } + body + } else [] + + grid( + columns: (1fr, auto, 1fr), + align: (left, center, right), + document.title, [v#version - #hash], chapter, + ) +} + +#let project( + title: none, + author: none, + version: "0.0.1", + hash: "abcdefgh", + icon-path: none, + doc, +) = { + assert(title != none, message: "Please provide a title") + + set document( + title: title, + author: author, + ) + set text( + font: "Source Sans 3", + ) + + show std.title: set text(size: 1.5em) + + show heading.where(level: 1): it => { + pagebreak() + it + } + + set page( + header: context if counter(page).get().first() != 1 { _render-header(version, hash) }, + footer: context if counter(page).get().first() != 1 and page.numbering != none { + align(center, counter(page).display(page.numbering, both: true)) + }, + numbering: "1 / 1", + ) + + // Title page + align(center)[ + #std.title() + + v#version - #hash + + #if icon-path != none { + v(1cm) + image(icon-path) + } + ] + + outline() + show heading.where(level: 1): set heading(numbering: "I.") + + doc +} From bd47d33355476da67a594a286dd4e384c475a27d Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Fri, 26 Jun 2026 17:52:54 +0200 Subject: [PATCH 02/11] feat(manual): complete introduction and quick start --- docs/manual.typ | 160 +++++++++++++++++++++++++++++++++++++++++++++- docs/template.typ | 2 +- 2 files changed, 159 insertions(+), 3 deletions(-) diff --git a/docs/manual.typ b/docs/manual.typ index 5919e48..0f8fa09 100644 --- a/docs/manual.typ +++ b/docs/manual.typ @@ -1,3 +1,5 @@ +#import "@preview/codly:1.3.0": codly, codly-init +#import "@preview/codly-languages:0.1.10": codly-languages #import "template.typ": TODO, project #let midas-version = toml("../pyproject.toml").project.version @@ -12,16 +14,170 @@ icon-path: path("../assets/icon.svg"), ) +#show: codly-init +#codly(languages: codly-languages) + = Introduction -#TODO +Python is a very popular programming language, especially in data sciences. +However, it has been designed for simplicity, distancing itself from typed languages such as Java or C to embrace dynamic typing. +What this means is that in Python, type checks are deferred to runtime when operations are concretely executed. + +For developers, it might seem like a great way of simplifying the language and making it very flexible, but it does come with a cost. +Indeed, type errors are very easy to make in Python. While passing an integer where a string is expected might not be an issue in some cases, these are the sort of thing that can cause crashes or incorrect results without a clear diagnostic to help the user fix it. + +Fortunately, developers using IDEs or properly configured text editors can benefit from external type checkers such as MyPy which will perform static type analysis of their Python code. Some can also be configured to be very strict, forcing the user to make the whole code typable statically, thus avoiding any runtime type errors. + +This is not the end of the problem though. Some parts of a program, especially in data related fields, may not be available at "compile-time". For example, a dataset can be loaded from an external file, or data can be fetched from an API, with no guarantees of having the expected format when analysing the code statically. + +In turn, that can cause a range of loud and silent errors at runtime. A malformed number will probably crash the program when trying to convert it, but a NaN in a series of value might just produce wrong results without any exception. Combine this with often long-running data-processing pipelines and this is how developers can waste hours of precious computation time. + +Midas is a type system which can be used on top of Python to provide better type checking capabilities and gradual typing. +It aims at providing optional but strict type annotations and casting operations which can produce runtime assertions. It also allows the user to define dependent types with value constraints that are translated into runtime checks. = Installation -#TODO +Midas comes as a very light Python package that you can install on your system in a few simple steps. + +== Requirements + +Here below are the requirements for installing Midas. All Python dependencies will be installed by `uv` in the installation process described in @install-steps. + +- Python 3.11+ +- `uv` + +== Steps + +1. Clone the repository + ```bash + git clone https://git.kb28.ch/HEL/midas.git + ``` +2. Navigate inside the directory + ```bash + cd midas + ``` +3. Install Midas as a tool in your local user space + ```bash + uv tool install . + ``` + +And that's it ! You can now use Midas commands anywhere, like this: +```bash +midas --help +``` = Quick Start This chapter will give you the keys to quickly start using Midas in your project. +== Defining custom types + +To begin with, you might want to define some custom types for your project, to avoid handling anonymous float values everywhere. To do so, create a `*.midas` file in your project, and write some definitions for your types. See @midas-ref for more information on syntax and features. + +@qs-midas shows a simple example of what it might look like. + +#codly(header: [types.midas]) + +#figure( + ```midas + type Meter = float + extend Meter { + def __add__: fn(Meter, /) -> Meter + def __sub__: fn(Meter, /) -> Meter + } + + type Coordinate = object + extend Coordinate { + prop x: Meter + prop y: Meter + } + ```, + caption: [Example Midas type definitions], +) + +You can check for any syntax error using the following command: +```bash +midas validate types.midas +``` + +When you are happy with your definitions, you can generate Python stubs to use in your source code. This allows other type checkers like MyPy to recognize your custom types and avoid reporting them as undefined. It can also help catch some type errors in your IDE. +```bash +midas stubs types.midas -o stubs.pyi +``` + +This command will generate a file as shown in @qs-stubs, providing stub classes to represent the type lattice including methods and properties. + +#codly(header: [stubs.pyi]) + +#figure( + ```pyi + from __future__ import annotations + + class Meter(float): + def __add__(self, _0: Meter, /) -> Meter: ... + def __sub__(self, _0: Meter, /) -> Meter: ... + + class Coordinate(object): + x: Meter + y: Meter + ```, + caption: [Generated stubs], +) + +== Using Midas in Python + +You can now write your Python program as you would normally. You can import your custom types from the generated stubs file and use them in type annotations. + +You can also import the `cast` and `unsafe_cast` functions from `midas.typing` to explictly cast a value to a specific type (see @cast for more information). + +An example Python script is shown in @qs-python, demonstrating how you can use custom types in type annotations. Notice the comments describing errors that will be caught by the type checker in @qs-type-checking. + +#codly(header: [script.py]) + +#figure( + ```python + from lib import load_coordinate + from midas.typing import cast + from stubs import Coordinate, Meter + + p1 = cast(Coordinate, load_coordinate(0)) + p2 = cast(Coordinate, load_coordinate(1)) + + diff_x = p2.x - p1.x + diff_y = p2.y - p1.y + + dist = diff_x + diff_y + + p2.x += cast(Meter, 1) + p2.y = True # invalid, wrong type + p2.z = 3 # invalid, no property 'z' on Coordinate + p2.x.a = 3 # invalid, no properties on Meter + ```, + caption: [Example Python script], +) + +== Type checking + +Now that you have defined some types and written a script, you can run the type checker with the following command. You can also skip this step and directly run the compilation command in @qs-compilation. + +```bash +midas check -t types.midas script.py +``` + +== Compiling + +The final step is to compile your code. This step will produce a runnable Python script, including runtime assertions generated by `cast` expressions. + +```bash +midas compile -t types.midas script.py +python3 build/midas/script.py +``` + + + += Midas Language Reference + +== Casts + #TODO + diff --git a/docs/template.typ b/docs/template.typ index 78589f0..1861b5f 100644 --- a/docs/template.typ +++ b/docs/template.typ @@ -90,7 +90,7 @@ ] outline() - show heading.where(level: 1): set heading(numbering: "I.") + show heading: set heading(numbering: "I.1.") doc } From 386018b9569efa1d62b24144bc814e2e62151bb7 Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Sun, 28 Jun 2026 12:36:02 +0200 Subject: [PATCH 03/11] feat(manual): add sublime syntax for Midas --- docs/midas.sublime-syntax | 176 ++++++++++++++++++++++++++++++++++++++ docs/template.typ | 2 + 2 files changed, 178 insertions(+) create mode 100644 docs/midas.sublime-syntax diff --git a/docs/midas.sublime-syntax b/docs/midas.sublime-syntax new file mode 100644 index 0000000..66db18e --- /dev/null +++ b/docs/midas.sublime-syntax @@ -0,0 +1,176 @@ +%YAML 1.2 +--- +name: Midas +file_extensions: + - midas +scope: source.midas + +variables: + identifier: "[a-zA-Z_][a-zA-Z0-9_]*" + +contexts: + main: + - include: comments + - include: keywords + - include: types + + comments: + - match: "//" + scope: punctuation.definition.comment.midas + push: + - meta_scope: comment.line.midas + - match: $ + pop: true + - match: /\* + scope: punctuation.definition.comment.midas + push: + - meta_scope: comment.block.midas + - match: \*/ + pop: true + + keywords: + - match: \btype\b + scope: keyword.declaration.midas + push: type-stmt + - match: \bextend\b + scope: keyword.declaration.midas + push: extend-stmt + - match: \bpredicate\b + scope: keyword.declaration.midas + push: predicate-stmt + + type-stmt: + - include: comments + - match: "{{identifier}}" + scope: entity.name.type + - match: \[ + push: type-params + - match: "=" + scope: keyword.operator.equal.midas + push: type-expr + - match: $ + pop: true + + type-expr: + - include: comments + - match: \b(fn)\s*(\() + captures: + 1: keyword.other.midas + 2: punctuation.section.group.begin + push: fn-params + - match: \b(where)\b + scope: keyword.other.midas + set: constraint + - match: "{{identifier}}" + scope: entity.name.type + - match: $ + pop: 2 + + fn-params: + - match: "({{identifier}})(:)" + captures: + 1: variable.parameter.midas + 2: punctuation.separator.annotation.midas + push: + - include: type-expr + - match: \? + scope: keyword.operator.qmark.midas + - match: "(?=,)" + scope: punctuation.separator.midas + pop: true + - match: '(?=\))' + pop: true + - include: type-expr + - match: '\)' + set: + - match: "->" + scope: keyword.operator.arrow.midas + set: type-expr + + constraint: + - include: comments + - match: $ + pop: 2 + + - match: \d+(\.\d+)? + scope: constant.numeric.midas + + - match: \b(true|false|none)\b + scope: constant.language.midas + + - match: (<=|>=|<|>|==|!=|&) + scope: keyword.operator + + - match: _ + scope: variable.language.midas + + - match: '{{identifier}}(?=\s*\()' + scope: variable.function.midas + + - match: "{{identifier}}" + scope: variable.other.readwrite.midas + + type-params: + - include: comments + - match: "<:" + scope: keyword.operator.subtype.midas + - match: "[a-zA-Z][a-zA-Z_0-9]*" + scope: entity.name.type + - match: "]" + pop: true + + extend-stmt: + - include: comments + - match: "{{identifier}}" + scope: entity.name.type + - match: \[ + push: type-params + - match: \{ + scope: punctuation.section.block.begin + push: extend-body + + extend-body: + - include: comments + - include: member-stmt + - match: \} + scope: punctuation.section.block.end + pop: 2 + + member-stmt: + - match: \b(prop|def)\b + scope: keyword.other.midas + push: + - match: "{{identifier}}" + scope: variable.other.member + - match: ":" + push: type-expr + - match: $ + pop: true + + predicate-stmt: + - include: comments + - match: "{{identifier}}" + scope: entity.name.function.midas + - match: '\(' + push: predicate-params + - match: "=" + scope: keyword.operator.equal.midas + set: constraint + - match: $ + pop: true + + predicate-params: + - match: "({{identifier}})(:)" + captures: + 1: variable.parameter.midas + 2: punctuation.separator.annotation.midas + push: + - include: type-expr + - match: "(?=,)" + scope: punctuation.separator.midas + pop: true + - match: '(?=\))' + pop: true + + - match: '\)' + pop: true diff --git a/docs/template.typ b/docs/template.typ index 1861b5f..c4c1386 100644 --- a/docs/template.typ +++ b/docs/template.typ @@ -77,6 +77,8 @@ numbering: "1 / 1", ) + set raw(syntaxes: path("midas.sublime-syntax")) + // Title page align(center)[ #std.title() From f9f3ade6c7bba66360f17e6bc06bed3a18176b3c Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Sun, 28 Jun 2026 12:37:44 +0200 Subject: [PATCH 04/11] feat(manual): document type statement --- docs/manual.typ | 139 ++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 136 insertions(+), 3 deletions(-) diff --git a/docs/manual.typ b/docs/manual.typ index 0f8fa09..db21278 100644 --- a/docs/manual.typ +++ b/docs/manual.typ @@ -1,6 +1,7 @@ #import "@preview/codly:1.3.0": codly, codly-init #import "@preview/codly-languages:0.1.10": codly-languages #import "template.typ": TODO, project +#import "@preview/gentle-clues:1.3.1" as gc #let midas-version = toml("../pyproject.toml").project.version #let head-ref = read("../.git/HEAD").split(":").at(1).trim() @@ -15,7 +16,22 @@ ) #show: codly-init -#codly(languages: codly-languages) +#codly( + languages: codly-languages + + ( + midas: ( + name: "Midas", + color: rgb("#eedd47"), + icon: box( + image( + "../assets/icon.svg", + height: 130%, + fit: "contain", + ), + ), + ), + ), +) = Introduction @@ -173,11 +189,128 @@ midas compile -t types.midas script.py python3 build/midas/script.py ``` - - = Midas Language Reference +In this chapter, you will find a complete reference for the Midas definition language. + +A `*.midas` file contains a number of statements, which can be: +- *`type`* statements (see @type-stmt): to define a new type +- *`extend`* statements (see @extend-stmt): to define member of a type +- *`predicate`* statements (see @predicate-stmt): to define named predicates that can be used in constraint types + +== Type Statement + +A *`type`* statement lets you define a new type. It requires a unique name and base type. + +The simplest form of a *`type`* statement is: +```midas +type MyType = float +``` + +This statement defines a new type called `MyType` which is a subtype of `float`. `MyType` is a `float` but a `float` is not necessarily `MyType`. + +=== Function types + +A function type is written in a similar notation to Python function definitions: +```midas +type Repeater = fn(text: str, count: int) -> str +``` + +Midas supports positional-only, keyword-only and mixed arguments (using the `/` and `*` separators). You may omit the name of positional-only arguments. The return type is required. + +Optional parameters can be indicated by adding a question mark (`?`) after their type: +```midas +type Repeater = fn(text: str, count: int, *, sep: str?) -> str +``` + +#gc.warning[ + Sink arguments (`*args`, `**kwargs`) are not currently supported. +] + +=== Generic types + +For more complex types, you might want to use type parameters. For example, to define a container, we might write: +```midas +type Container[T] = object +``` + +To better refine a generic type, you can also bound type parameters using the following syntax: +```midas +type Container[T <: float] = object +``` + +This can be read as "`Container` is a generic type which takes one type parameter `T` that must be a subtype of `float`". + +You can use a generic type, i.e. instantiate it, by using a similar syntax with concrete type as arguments: + +```midas +type MyContainer = Container[MyType] +``` + +Generic types can also take multiple parameters, which are then separated by commas: +```midas +type ZipCodeRegistry = dict[int, str] +``` + +The _body_ of a generic type, i.e. the right-hand side of the definition, can contain or even be equal to any number of its parameters.#footnote[The latter is not something that is expressible in standard Python, yet it brings a semantic distinction on top of structurally equivalent values.] For example, the following is a valid type statement: +```midas +type Price[T <: Currency] = T where _ > 0 +``` + +=== Constraint types + +A useful feature provided by Midas is the possibility to combine types with custom value constraints. For example, you might want to define a type for positive amounts of money: +```midas +type Money = float +type Income = Money where _ >= 0 +``` + +Constraints can be combined with any type using the `where` keyword, followed by a predicate expression (see @predicate-stmt). + +== Extend Statement + +Type statements allow you to define new types, kind of like type aliases. However, a type might have properties or methods of its own. These might override those of the parent type or be brand new members. + +This is where the `extend` statement comes into play. It allows defining members on a given type. Members can either be properties (`prop`) or methods (`def`). The only difference between the two is that methods must be functions and can be overloaded. + +Here is a simple example showing how to define a property and a method on a custom type: +```midas +type MyType = float +extend MyType { + prop norm: float + def double: fn() -> MyType +} +``` + +An `extend` statement can appear anywhere after the type it extends has been defined. +You may want to overide Python's dunder methods to implement type checking for some basic operators, like `__add__` for the `+` operator. + +```midas +type Money = float +extend Money { + def __add__(Money, /) -> Money + def __mul__(float, /) -> Money +} +``` + +When extending generic type, you must specify the whole type, including its parameter(s): +```midas +type Container[T <: float] = object +extend Container[T <: float] { + prop content: T + def set_content: fn(content: T) -> None +} +``` + +== Predicate Statement + +#TODO + == Casts #TODO += Supported Python Syntax + +#TODO + From 4c39504750196b9aaa10f4d08d6bfaa8370c974a Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Sun, 28 Jun 2026 14:12:41 +0200 Subject: [PATCH 05/11] feat(manual): document predicate and constraints --- docs/manual.typ | 59 ++++++++++++++++++++++++++++++++++++++++++----- docs/template.typ | 25 +++++++++++++++++++- 2 files changed, 77 insertions(+), 7 deletions(-) diff --git a/docs/manual.typ b/docs/manual.typ index db21278..7bb2931 100644 --- a/docs/manual.typ +++ b/docs/manual.typ @@ -265,7 +265,9 @@ type Money = float type Income = Money where _ >= 0 ``` -Constraints can be combined with any type using the `where` keyword, followed by a predicate expression (see @predicate-stmt). +Constraints can be combined with any type using the `where` keyword, followed by a constraint expression (see @constraint-expr). + +#pagebreak() == Extend Statement @@ -302,15 +304,60 @@ extend Container[T <: float] { } ``` +#pagebreak() + == Predicate Statement +A *`predicate`* statement lets you define a named constraint expression, like a function, which can then be used in other constraint expressions (either in other predicate statements or in constraint types). See @constraint-expr for more information about the syntax of constraint expressions. + +The left-hand side of a predicate statement is written as a function signature, without a return type. The right-hand side is a constraint expression. For example: +```midas +predicate is_positive(v: float) = v >= 0 +``` + +The left-hand side can also be curried to allow partial application. For example: +```midas +predicate in_range(mn: float, mx: float)(v: float) = mn <= v & v <= mx +predicate is_ratio = in_range(0.0, 1.0) +``` + +Notice that the second predicate statement doesn't take any parameters. This is simply a partial application of another predicate, kind of like an alias. You can use it in other expressions to finalize the call: +```midas +type Efficiency = float where is_ratio(_) +``` + +Of course you can also directly call `in_range`: +```midas +type Efficiency = float where in_range(0.0, 1.0)(_) +``` + +When compiled, named predicates are translated to Python functions which are used in runtime assertions. Only predicates that are referenced are compiled. + +#pagebreak() +== Constraint Expressions + +*Constraint expressions* are Python-like expressions which can appear in *`predicate`* statements or in constraint types. + +They can contain comparisons, simple computations, logical operations and must evaluate to a boolean value. + +Context is quite restricted inside these expressions. You can only reference some builtin functions, such as type constructors (`float(...)`, `str(...)`, etc.), parameters of predicate statements, and named predicates. In constraint type, the special variable `_` can be used to reference the value targeted by the type. For example: + +#codly() +#figure( + ```midas + predicate not_nan(v: float) = v != float("nan") + type RealFloat = float where not_nan(_) + ```, + caption: [Example constraint expressions], +) + +In the predicate statement (@ex-constraint-expr:1), we reference the parameter `v` and the builtin `float` function. +In the constraint type definition (@ex-constraint-expr:2), we then reference the named predicate `not_nan`, passing the value targeted by the type itself ( `_` ) + += Supported Python Syntax + #TODO == Casts #TODO - -= Supported Python Syntax - -#TODO - diff --git a/docs/template.typ b/docs/template.typ index c4c1386..ae0ad8b 100644 --- a/docs/template.typ +++ b/docs/template.typ @@ -44,6 +44,10 @@ ) } +#let _unshift-prefix(prefix, content) = context { + pad(left: -measure(prefix).width, prefix + content) +} + #let project( title: none, author: none, @@ -64,9 +68,28 @@ show std.title: set text(size: 1.5em) + // Adapted from https://github.com/hei-templates/hei-synd-thesis/blob/7d2b941197babae0bf3afd4e5914754e09a64001/lib/template-thesis.typ#L242-L261 show heading.where(level: 1): it => { pagebreak() - it + + set text(size: 1.5em) + set block(above: 1.2em, below: 1.2em) + if it.numbering != none { + let num = numbering(it.numbering, ..counter(heading).at(it.location())) + let prefix = num + h(1em) + _unshift-prefix(prefix, it.body) + } else { + it + } + } + + show heading.where(level: 2): it => { + if it.numbering != none { + let num = numbering(it.numbering, ..counter(heading).at(it.location())) + _unshift-prefix(num + h(0.8em), it.body) + } else { + it + } } set page( From 4b2b0fe476990fe08b66db5f84c8db1c80596e39 Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Sun, 28 Jun 2026 21:41:39 +0200 Subject: [PATCH 06/11] feat(manual): document supported Python syntax --- docs/manual.typ | 272 +++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 269 insertions(+), 3 deletions(-) diff --git a/docs/manual.typ b/docs/manual.typ index 7bb2931..8745b27 100644 --- a/docs/manual.typ +++ b/docs/manual.typ @@ -1,4 +1,8 @@ -#import "@preview/codly:1.3.0": codly, codly-init +//#import "@preview/codly:1.3.0": codly, codly-init +// Fix unaligned highlights in v0.15.0 () +// See https://github.com/Dherse/codly/pull/132 +#import "@local/codly:1.3.1": codly, codly-init + #import "@preview/codly-languages:0.1.10": codly-languages #import "template.typ": TODO, project #import "@preview/gentle-clues:1.3.1" as gc @@ -144,7 +148,7 @@ This command will generate a file as shown in @qs-stubs, providing stub classes You can now write your Python program as you would normally. You can import your custom types from the generated stubs file and use them in type annotations. -You can also import the `cast` and `unsafe_cast` functions from `midas.typing` to explictly cast a value to a specific type (see @cast for more information). +You can also import the `cast` and `unsafe_cast` functions from `midas.typing` to explicitly cast a value to a specific type (see @cast for more information). An example Python script is shown in @qs-python, demonstrating how you can use custom types in type annotations. Notice the comments describing errors that will be caught by the type checker in @qs-type-checking. @@ -209,6 +213,23 @@ type MyType = float This statement defines a new type called `MyType` which is a subtype of `float`. `MyType` is a `float` but a `float` is not necessarily `MyType`. +=== Builtin / base types + +A number of base types are provided out of the box. They correspond to Python's builtin types: +- `object` +- `str` +- `float` +- `int` +- `bool` +- `list` +- `dict` +- `None` + +Some differences are to be noted however. +1. `bool` is not a subtype of `int` +2. `list` are homogeneous, i.e. all items must be of the same type +3. `dict` keys and values are homogeneous, i.e. all keys must be of the same type and all values must be of the same type (can be different from keys). + === Function types A function type is written in a similar notation to Python function definitions: @@ -356,8 +377,253 @@ In the constraint type definition (@ex-constraint-expr:2), we then reference the = Supported Python Syntax -#TODO +Midas integrates naturally in Python via type annotations. Through generated stubs, even other type checker can detect your custom types (see @cmd-stubs). + +It has been designed to leave the user free of typing any amount of their code but be strict about the parts that are annotated. By default, any untyped Python expression is assigned `UnknownType`. + +Any operation is permitted on `UnknownType` and will result in `UnknownType` values. + +The moment an expression can be typed, that be thanks to an annotation or a literal value, the type checker kicks in and will validate your statements. + +Because Python is very flexible language with many features, some expressions and statements might be more complex to properly type check, thus only a subset of the Python language is fully supported. This chapter lists all supported features of Python and how they affect type checking. + +Some examples are presented in the following sections in the form of code blocks. Highlights in the code blocks indicate the type assigned to each expression by the type checker. Some types may be omitted for readability. For example: + +#codly( + highlights: ( + ( + line: 1, + start: 5, + fill: green, + tag: [_int_], + ), + ( + line: 2, + start: 7, + end: 7, + fill: green, + tag: [_int_], + ), + ), +) + +```python +v = 3 +print(v) +``` + +== Literals + +Literal Python values are type checked using builtin types. Lists and dictionaries of literals are also typed liked literals. This does not include comprehension lists/dicts (```py [. for . in .]```), nor formatted strings (```py f"..."```). @supported-literals shows the list of supported literal values and their type. + +#let supported-literals = table( + columns: 2, + table.header[*Example value*][*Judged Type*], + ```py 42```, ```py int```, + ```py 3.14```, ```py float```, + ```py True```, ```py bool```, + ```py "Midas"```, ```py str```, + ```py None```, ```py None```, + ```py [1, 2, 3]```, ```py list[int]```, + ```py {1: "One", 2: "Two"}```, ```py dict[int, str]```, + ```py ("1", 1, True)```, ```py tuple[str, int, bool]```, +) + +#figure( + supported-literals, + caption: [Supported literal values and their judged types], +) + +== Assignments + +Variable assignments allow assigning a new value to a variable. For the type checker, this implies two things: +1. If the variable was not already declared in the current scope, it is declared at that point with the type of the right-hand side expression +2. If the variable was already declared, the type of the right-hand side expression is checked against the declared type of the variable. Only a subtype of the variable's type can be assigned to it + +Once a variable has been given a type, it cannot be changed in the same scope. + +The walrus operator (```py :=```) is not currently supported. + +A simple annotation declaration, without assigning a value, is enough to declare a variable. For example: +```python +var: float +``` + +Because unpacking is not supported, assigning to multiple values is also not handled by the type checker. + +== Arithmetic + +- All basic binary operators are supported, through dunder methods. +- All comparison operators except ```py in``` are supported. +- All unary operators are supported (`+`, `-`, `~`). +- All logical operators are supported (```py and```, ```py or```, ```py not```). + +== Ternary operator + +The ternary operator ```py . if . else .``` is supported. As for `if` statements (see @if-else), the test expression must be a boolean. Additionally, both branches must be of the same type. + +For example: +#codly( + highlights: ( + ( + line: 1, + start: 10, + end: 44, + tag: [_str_], + fill: blue, + ), + ( + line: 1, + start: 11, + end: 16, + tag: [_str_], + fill: green, + ), + ( + line: 1, + start: 39, + end: 43, + tag: [_str_], + fill: green, + ), + ( + line: 1, + start: 21, + end: 32, + tag: [_bool_], + fill: green, + ), + ), +) +```python +parity = ("even" if num % 2 == 0 else "odd") +``` + +== Control flow + +Some control flow features are supported. For the limited code of this project, not all constructs are supported. The following are those currently handled and typ checked by Midas. + +=== `if` / `elif` / `else` + +Conditional statements are checked relatively strictly by Midas. The test expression, i.e. what comes after the ```py if``` keyword, must be a boolean. While Python allows introducing and leaking new variables from inside an ```py if``` statement, Midas will strictly forbid leaks by restraining bindings to the scope they are defined in. For example, the following valid Python code will not compile with Midas: +```python +age = 22 +if age >= 18: + msg = "You're an adult" +else: + msg = "You're still a child" +print(msg) # -> unknown variable 'msg' +``` + +=== `for` loops + +Simple forms of `for` loops can be used, that is using a single variable and iterating over an object implementing the `__getitem__` method. Like above in @if-else, leaking variables from inside the loop is ignored. + +The `for`-`else` statements are not supported. `while` loops are also not not supported. + +== Functions + +You can define functions as usual and the type checker will do its best to type it. Apart from argument sinks (`*args`, `**kwargs`), all forms of parameter specifications are supported (positional-only, keyword-only, mixed, optional). + +As for the rest of your code, type annotations are optional, but recommended. If you omit the return type hint, the type checker will try to infer it from the function body and its return statements. If you did specify a return type, all return paths must return values that are subtypes of the type hint. + +#codly( + highlights: ( + ( + line: 2, + start: 12, + end: 16, + tag: [_float_], + fill: green, + ), + ( + line: 2, + start: 12, + tag: [_float_], + fill: blue, + ), + ( + line: 3, + start: 10, + end: 15, + tag: [_(value: float) -> float_], + fill: green, + ), + ( + line: 3, + start: 17, + end: 19, + tag: [_float_], + fill: green, + ), + ( + line: 3, + start: 10, + tag: [_float_], + fill: blue, + ), + ), +) +```python +def double(value: float) -> float: + return value * 2 +result = double(4.0) +``` + +Anonymous functions (```py lambda```) are not yet supported == Casts +#gc.info[ + The functions discussed in this section are provided by the `midas.typing` submodule. You can import them in your script like so: + ```python + from midas.typing import cast, unsafe_cast + ``` +] + +Sometimes, you may want to use a value whose type is not known to the type checker in a place where it expects a particular type. In that case, if you do know that the runtime type will correspond to what is expected, you can use a `cast` expression. + +Similar to the `cast` function from the `typing` package of Python's Standard Library, it allows telling the type checker that a value has a given type. While `typing`'s function doesn't have any runtime side-effect, Midas' will generate runtime assertions, ensuring that your statement is true when running the code. What cannot be checked statically is checked at runtime. + +In the following example, a runtime check would be generated to ensure that the value is indeed a `float` and that it satisfies the type's constraint (i.e. `>= 0`): + +#codly( + highlights: ( + ( + line: 1, + start: 35, + end: 47, + tag: [_UnknownType_], + fill: red, + ), + ( + line: 2, + start: 7, + end: 17, + tag: [_PositiveFloat_], + fill: green, + ), + ), +) +```python +typed_value = cast(PositiveFloat, unknown_value) +print(typed_value) +``` + +There may be some cases where the cost of checking a value at runtime is simply not worth the safety, for example when dealing with a big dataset. If do wish so, you can use `unsafe_cast` which will only tell the type checker the type of the value, without generating a runtime assertion. This maps to the default behavior of `typing`'s own `cast` function. + +If the value passed to `cast` or `unsafe_cast` is a literal (e.g. an integer, a string, a list of literals, etc.), the assertion is evaluated _at compile-time_ and no runtime assertion is generated. + += Commands + #TODO + +== Type Checking (`check`) +== Compiling (`compile`) +== Formatting (`format`) +== Highlighting (`highlight`) +== Dumping the AST (`parse`) +== Dumping the Registry (`dump-registry`) +== Generating Stubs (`stubs`) +== Showing Type Judgements (`types`) +== Validating Definitions (`validate`) From 759b416bf3efddcc90432fdb0f0b0d20dae10d7a Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Sun, 28 Jun 2026 22:20:15 +0200 Subject: [PATCH 07/11] feat(manual): wrap all code in figures --- docs/manual.typ | 288 ++++++++++++++++++++++++++++++------------------ 1 file changed, 178 insertions(+), 110 deletions(-) diff --git a/docs/manual.typ b/docs/manual.typ index 8745b27..82c3574 100644 --- a/docs/manual.typ +++ b/docs/manual.typ @@ -141,7 +141,7 @@ This command will generate a file as shown in @qs-stubs, providing stub classes x: Meter y: Meter ```, - caption: [Generated stubs], + caption: [Generated stubs from example definitions of @qs-midas], ) == Using Midas in Python @@ -207,86 +207,116 @@ A `*.midas` file contains a number of statements, which can be: A *`type`* statement lets you define a new type. It requires a unique name and base type. The simplest form of a *`type`* statement is: -```midas -type MyType = float -``` +#figure( + ```midas + type MyType = float + ```, + caption: [Simple `type` statement declaring a new type "`MyType`" as a subtype of `float`], +) This statement defines a new type called `MyType` which is a subtype of `float`. `MyType` is a `float` but a `float` is not necessarily `MyType`. === Builtin / base types -A number of base types are provided out of the box. They correspond to Python's builtin types: -- `object` -- `str` -- `float` -- `int` -- `bool` -- `list` -- `dict` -- `None` +A number of base types are provided out of the box, which can be used to derive other types. + +They correspond to Python's builtin types: +```py object```, +```py str```, +```py float```, +```py int```, +```py bool```, +```py list```, +```py dict```, +```py None```. Some differences are to be noted however. -1. `bool` is not a subtype of `int` -2. `list` are homogeneous, i.e. all items must be of the same type -3. `dict` keys and values are homogeneous, i.e. all keys must be of the same type and all values must be of the same type (can be different from keys). +1. ```py bool``` is not a subtype of ```py int``` +2. ```py list``` are homogeneous, i.e. all items must be of the same type +3. ```py dict``` keys and values are homogeneous, i.e. all keys must be of the same type and all values must be of the same type (can be different from keys). === Function types A function type is written in a similar notation to Python function definitions: -```midas -type Repeater = fn(text: str, count: int) -> str -``` +#figure( + ```midas + type Repeater = fn(text: str, count: int) -> str + ```, + caption: [Simple function type definition], +) Midas supports positional-only, keyword-only and mixed arguments (using the `/` and `*` separators). You may omit the name of positional-only arguments. The return type is required. Optional parameters can be indicated by adding a question mark (`?`) after their type: -```midas -type Repeater = fn(text: str, count: int, *, sep: str?) -> str -``` +#figure( + ```midas + type Repeater = fn(text: str, count: int, *, sep: str?) -> str + ```, + caption: [Function type definition with an optional keyword-only parameter], +) #gc.warning[ Sink arguments (`*args`, `**kwargs`) are not currently supported. ] +=== Constraint types + +A useful feature provided by Midas is the possibility to combine types with custom value constraints. For example, you might want to define a type for positive amounts of money: + +#figure( + ```midas + type Money = float + type Income = Money where _ >= 0 + ```, + caption: [Simple constraint type definition], +) + +Constraints can be combined with any type using the `where` keyword, followed by a constraint expression (see @constraint-expr). + === Generic types For more complex types, you might want to use type parameters. For example, to define a container, we might write: -```midas -type Container[T] = object -``` +#figure( + ```midas + type Container[T] = object + ```, + caption: [Simple generic container type definition], +) To better refine a generic type, you can also bound type parameters using the following syntax: -```midas -type Container[T <: float] = object -``` +#figure( + ```midas + type Container[T <: float] = object + ```, + caption: [Generic container type definition with a bound], +) This can be read as "`Container` is a generic type which takes one type parameter `T` that must be a subtype of `float`". You can use a generic type, i.e. instantiate it, by using a similar syntax with concrete type as arguments: -```midas -type MyContainer = Container[MyType] -``` +#figure( + ```midas + type MyContainer = Container[MyType] + ```, + caption: [Application of a generic type], +) Generic types can also take multiple parameters, which are then separated by commas: -```midas -type ZipCodeRegistry = dict[int, str] -``` +#figure( + ```midas + type ZipCodeRegistry = dict[int, str] + ```, + caption: [Application of a multi-parameter generic type], +) The _body_ of a generic type, i.e. the right-hand side of the definition, can contain or even be equal to any number of its parameters.#footnote[The latter is not something that is expressible in standard Python, yet it brings a semantic distinction on top of structurally equivalent values.] For example, the following is a valid type statement: -```midas -type Price[T <: Currency] = T where _ > 0 -``` - -=== Constraint types - -A useful feature provided by Midas is the possibility to combine types with custom value constraints. For example, you might want to define a type for positive amounts of money: -```midas -type Money = float -type Income = Money where _ >= 0 -``` - -Constraints can be combined with any type using the `where` keyword, followed by a constraint expression (see @constraint-expr). +#figure( + ```midas + type Price[T <: Currency] = T where _ > 0 + ```, + caption: [Type parameters in a generic type's body], +) #pagebreak() @@ -297,33 +327,42 @@ Type statements allow you to define new types, kind of like type aliases. Howeve This is where the `extend` statement comes into play. It allows defining members on a given type. Members can either be properties (`prop`) or methods (`def`). The only difference between the two is that methods must be functions and can be overloaded. Here is a simple example showing how to define a property and a method on a custom type: -```midas -type MyType = float -extend MyType { - prop norm: float - def double: fn() -> MyType -} -``` +#figure( + ```midas + type MyType = float + extend MyType { + prop norm: float + def double: fn() -> MyType + } + ```, + caption: [Simple `extend` statement defining a property and a method], +) An `extend` statement can appear anywhere after the type it extends has been defined. -You may want to overide Python's dunder methods to implement type checking for some basic operators, like `__add__` for the `+` operator. +You may want to override Python's dunder methods to implement type checking for some basic operators, like `__add__` for the `+` operator. -```midas -type Money = float -extend Money { - def __add__(Money, /) -> Money - def __mul__(float, /) -> Money -} -``` +#figure( + ```midas + type Money = float + extend Money { + def __add__(Money, /) -> Money + def __mul__(float, /) -> Money + } + ```, + caption: [Simple `extend` statement overriding some dunder methods], +) When extending generic type, you must specify the whole type, including its parameter(s): -```midas -type Container[T <: float] = object -extend Container[T <: float] { - prop content: T - def set_content: fn(content: T) -> None -} -``` +#figure( + ```midas + type Container[T <: float] = object + extend Container[T <: float] { + prop content: T + def set_content: fn(content: T) -> None + } + ```, + caption: [Generic `extend` statement using type parameters in the declared members], +) #pagebreak() @@ -332,25 +371,37 @@ extend Container[T <: float] { A *`predicate`* statement lets you define a named constraint expression, like a function, which can then be used in other constraint expressions (either in other predicate statements or in constraint types). See @constraint-expr for more information about the syntax of constraint expressions. The left-hand side of a predicate statement is written as a function signature, without a return type. The right-hand side is a constraint expression. For example: -```midas -predicate is_positive(v: float) = v >= 0 -``` +#figure( + ```midas + predicate is_positive(v: float) = v >= 0 + ```, + caption: [Simple `predicate` statement defining an `is_positive` predicate], +) The left-hand side can also be curried to allow partial application. For example: -```midas -predicate in_range(mn: float, mx: float)(v: float) = mn <= v & v <= mx -predicate is_ratio = in_range(0.0, 1.0) -``` +#figure( + ```midas + predicate in_range(mn: float, mx: float)(v: float) = mn <= v & v <= mx + predicate is_ratio = in_range(0.0, 1.0) + ```, + caption: [Curried `predicate` statement and partial application], +) Notice that the second predicate statement doesn't take any parameters. This is simply a partial application of another predicate, kind of like an alias. You can use it in other expressions to finalize the call: -```midas -type Efficiency = float where is_ratio(_) -``` +#figure( + ```midas + type Efficiency = float where is_ratio(_) + ```, + caption: [Constraint type definition using the partially applied predicate from @midas-predicate-partial], +) Of course you can also directly call `in_range`: -```midas -type Efficiency = float where in_range(0.0, 1.0)(_) -``` +#figure( + ```midas + type Efficiency = float where in_range(0.0, 1.0)(_) + ```, + caption: [Full call of curried predicate from @midas-predicate-partial], +) When compiled, named predicates are translated to Python functions which are used in runtime assertions. Only predicates that are referenced are compiled. @@ -363,7 +414,6 @@ They can contain comparisons, simple computations, logical operations and must e Context is quite restricted inside these expressions. You can only reference some builtin functions, such as type constructors (`float(...)`, `str(...)`, etc.), parameters of predicate statements, and named predicates. In constraint type, the special variable `_` can be used to reference the value targeted by the type. For example: -#codly() #figure( ```midas predicate not_nan(v: float) = v != float("nan") @@ -445,9 +495,12 @@ Once a variable has been given a type, it cannot be changed in the same scope. The walrus operator (```py :=```) is not currently supported. A simple annotation declaration, without assigning a value, is enough to declare a variable. For example: -```python -var: float -``` +#figure( + ```python + var: float + ```, + caption: [Bare Python variable annotation without assignment], +) Because unpacking is not supported, assigning to multiple values is also not handled by the type checker. @@ -495,9 +548,12 @@ For example: ), ), ) -```python -parity = ("even" if num % 2 == 0 else "odd") -``` +#figure( + ```python + parity = ("even" if num % 2 == 0 else "odd") + ```, + caption: [Typing of ternary operator], +) == Control flow @@ -505,15 +561,18 @@ Some control flow features are supported. For the limited code of this project, === `if` / `elif` / `else` -Conditional statements are checked relatively strictly by Midas. The test expression, i.e. what comes after the ```py if``` keyword, must be a boolean. While Python allows introducing and leaking new variables from inside an ```py if``` statement, Midas will strictly forbid leaks by restraining bindings to the scope they are defined in. For example, the following valid Python code will not compile with Midas: -```python -age = 22 -if age >= 18: - msg = "You're an adult" -else: - msg = "You're still a child" -print(msg) # -> unknown variable 'msg' -``` +Conditional statements are checked relatively strictly by Midas. The test expression, i.e. what comes after the ```py if``` keyword, must be a boolean. While Python allows introducing and leaking new variables from inside an ```py if``` statement, Midas will strictly forbid leaks by restraining bindings to the scope they are defined in. For example, the following Python code will not compile with Midas: +#figure( + ```python + age = 22 + if age >= 18: + msg = "You're an adult" + else: + msg = "You're still a child" + print(msg) # -> unknown variable 'msg' + ```, + caption: [`if`/`else` statement cannot leak variables], +) === `for` loops @@ -564,11 +623,14 @@ As for the rest of your code, type annotations are optional, but recommended. If ), ), ) -```python -def double(value: float) -> float: - return value * 2 -result = double(4.0) -``` +#figure( + ```python + def double(value: float) -> float: + return value * 2 + result = double(4.0) + ```, + caption: [Typing of function's body and call], +) Anonymous functions (```py lambda```) are not yet supported @@ -576,9 +638,12 @@ Anonymous functions (```py lambda```) are not yet supported #gc.info[ The functions discussed in this section are provided by the `midas.typing` submodule. You can import them in your script like so: - ```python - from midas.typing import cast, unsafe_cast - ``` + #figure( + ```python + from midas.typing import cast, unsafe_cast + ```, + caption: [Importing cast functions], + ) ] Sometimes, you may want to use a value whose type is not known to the type checker in a place where it expects a particular type. In that case, if you do know that the runtime type will correspond to what is expected, you can use a `cast` expression. @@ -605,10 +670,13 @@ In the following example, a runtime check would be generated to ensure that the ), ), ) -```python -typed_value = cast(PositiveFloat, unknown_value) -print(typed_value) -``` +#figure( + ```python + typed_value = cast(PositiveFloat, unknown_value) + print(typed_value) + ```, + caption: [Typing of `cast` expression], +) There may be some cases where the cost of checking a value at runtime is simply not worth the safety, for example when dealing with a big dataset. If do wish so, you can use `unsafe_cast` which will only tell the type checker the type of the value, without generating a runtime assertion. This maps to the default behavior of `typing`'s own `cast` function. From 31e696c938dd374819125103387e2fe02524a429 Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Sun, 28 Jun 2026 22:28:13 +0200 Subject: [PATCH 08/11] feat(manual): add listings outline and tweak template --- docs/template.typ | 112 +++++++++++++++++++++++++++------------------- 1 file changed, 67 insertions(+), 45 deletions(-) diff --git a/docs/template.typ b/docs/template.typ index ae0ad8b..1404092 100644 --- a/docs/template.typ +++ b/docs/template.typ @@ -66,56 +66,78 @@ font: "Source Sans 3", ) - show std.title: set text(size: 1.5em) - - // Adapted from https://github.com/hei-templates/hei-synd-thesis/blob/7d2b941197babae0bf3afd4e5914754e09a64001/lib/template-thesis.typ#L242-L261 - show heading.where(level: 1): it => { - pagebreak() - - set text(size: 1.5em) - set block(above: 1.2em, below: 1.2em) - if it.numbering != none { - let num = numbering(it.numbering, ..counter(heading).at(it.location())) - let prefix = num + h(1em) - _unshift-prefix(prefix, it.body) - } else { - it - } - } - - show heading.where(level: 2): it => { - if it.numbering != none { - let num = numbering(it.numbering, ..counter(heading).at(it.location())) - _unshift-prefix(num + h(0.8em), it.body) - } else { - it - } - } - - set page( - header: context if counter(page).get().first() != 1 { _render-header(version, hash) }, - footer: context if counter(page).get().first() != 1 and page.numbering != none { - align(center, counter(page).display(page.numbering, both: true)) - }, - numbering: "1 / 1", - ) - set raw(syntaxes: path("midas.sublime-syntax")) - // Title page - align(center)[ - #std.title() + let front-page() = { + align(center)[ + #{ + set text(size: 1.5em) + std.title() + } - v#version - #hash + v#version - #hash - #if icon-path != none { - v(1cm) - image(icon-path) + #if icon-path != none { + v(1cm) + image(icon-path) + } + ] + pagebreak() + } + + let outlines() = { + outline() + pagebreak() + outline( + title: [List of Listings], + target: figure.where(kind: raw), + ) + + outline( + title: [List of Tables], + target: figure.where(kind: table), + ) + } + + let main() = { + // Adapted from https://github.com/hei-templates/hei-synd-thesis/blob/7d2b941197babae0bf3afd4e5914754e09a64001/lib/template-thesis.typ#L242-L261 + show heading.where(level: 1): it => { + pagebreak() + + set text(size: 1.5em) + set block(above: 1.2em, below: 1.2em) + if it.numbering != none { + let num = numbering(it.numbering, ..counter(heading).at(it.location())) + let prefix = num + h(1em) + _unshift-prefix(prefix, it.body) + } else { + it + } } - ] - outline() - show heading: set heading(numbering: "I.1.") + show heading.where(level: 2): it => { + if it.numbering != none { + let num = numbering(it.numbering, ..counter(heading).at(it.location())) + _unshift-prefix(num + h(0.8em), it.body) + } else { + it + } + } - doc + set page( + header: context _render-header(version, hash), + footer: context if page.numbering != none { + align(center, counter(page).display(page.numbering, both: true)) + }, + numbering: "1 / 1", + ) + + show heading: set heading(numbering: "I.1.") + counter(page).update(1) + doc + } + + front-page() + outlines() + main() } From e28f324a85521001697c7b49b116e7c09cf122fe Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Sun, 28 Jun 2026 22:30:09 +0200 Subject: [PATCH 09/11] fix(manual): typos --- docs/manual.typ | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/manual.typ b/docs/manual.typ index 82c3574..0479434 100644 --- a/docs/manual.typ +++ b/docs/manual.typ @@ -46,9 +46,9 @@ What this means is that in Python, type checks are deferred to runtime when oper For developers, it might seem like a great way of simplifying the language and making it very flexible, but it does come with a cost. Indeed, type errors are very easy to make in Python. While passing an integer where a string is expected might not be an issue in some cases, these are the sort of thing that can cause crashes or incorrect results without a clear diagnostic to help the user fix it. -Fortunately, developers using IDEs or properly configured text editors can benefit from external type checkers such as MyPy which will perform static type analysis of their Python code. Some can also be configured to be very strict, forcing the user to make the whole code typable statically, thus avoiding any runtime type errors. +Fortunately, developers using IDEs or properly configured text editors can benefit from external type checkers such as MyPy which will perform static type analysis of their Python code. Some can also be configured to be very strict, forcing the user to make the whole code typeable statically, thus avoiding any runtime type errors. -This is not the end of the problem though. Some parts of a program, especially in data related fields, may not be available at "compile-time". For example, a dataset can be loaded from an external file, or data can be fetched from an API, with no guarantees of having the expected format when analysing the code statically. +This is not the end of the problem though. Some parts of a program, especially in data related fields, may not be available at "compile-time". For example, a dataset can be loaded from an external file, or data can be fetched from an API, with no guarantees of having the expected format when analyzing the code statically. In turn, that can cause a range of loud and silent errors at runtime. A malformed number will probably crash the program when trying to convert it, but a NaN in a series of value might just produce wrong results without any exception. Combine this with often long-running data-processing pipelines and this is how developers can waste hours of precious computation time. From e15607b763b4d3f15336a905f9c3d4ec0451a70c Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Tue, 30 Jun 2026 14:03:42 +0200 Subject: [PATCH 10/11] fix(manual): end syntax highlighting of extend body --- docs/midas.sublime-syntax | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/midas.sublime-syntax b/docs/midas.sublime-syntax index 66db18e..d6abba6 100644 --- a/docs/midas.sublime-syntax +++ b/docs/midas.sublime-syntax @@ -127,14 +127,14 @@ contexts: push: type-params - match: \{ scope: punctuation.section.block.begin - push: extend-body + set: extend-body extend-body: - include: comments - include: member-stmt - match: \} scope: punctuation.section.block.end - pop: 2 + pop: true member-stmt: - match: \b(prop|def)\b From 6a0401833c8c189d8236ba0881b26a5febb00924 Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Tue, 30 Jun 2026 14:10:32 +0200 Subject: [PATCH 11/11] feat(manual): add strings to midas syntax def --- docs/midas.sublime-syntax | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/docs/midas.sublime-syntax b/docs/midas.sublime-syntax index d6abba6..dec80f8 100644 --- a/docs/midas.sublime-syntax +++ b/docs/midas.sublime-syntax @@ -9,8 +9,10 @@ variables: identifier: "[a-zA-Z_][a-zA-Z0-9_]*" contexts: - main: + prototype: - include: comments + + main: - include: keywords - include: types @@ -28,6 +30,12 @@ contexts: - match: \*/ pop: true + string: + - meta_include_prototype: false + - meta_scope: string.quoted.double.c + - match: '"' + pop: true + keywords: - match: \btype\b scope: keyword.declaration.midas @@ -40,7 +48,6 @@ contexts: push: predicate-stmt type-stmt: - - include: comments - match: "{{identifier}}" scope: entity.name.type - match: \[ @@ -52,7 +59,6 @@ contexts: pop: true type-expr: - - include: comments - match: \b(fn)\s*(\() captures: 1: keyword.other.midas @@ -88,7 +94,6 @@ contexts: set: type-expr constraint: - - include: comments - match: $ pop: 2 @@ -98,6 +103,9 @@ contexts: - match: \b(true|false|none)\b scope: constant.language.midas + - match: '"' + push: string + - match: (<=|>=|<|>|==|!=|&) scope: keyword.operator @@ -111,7 +119,6 @@ contexts: scope: variable.other.readwrite.midas type-params: - - include: comments - match: "<:" scope: keyword.operator.subtype.midas - match: "[a-zA-Z][a-zA-Z_0-9]*" @@ -120,7 +127,6 @@ contexts: pop: true extend-stmt: - - include: comments - match: "{{identifier}}" scope: entity.name.type - match: \[ @@ -130,7 +136,6 @@ contexts: set: extend-body extend-body: - - include: comments - include: member-stmt - match: \} scope: punctuation.section.block.end @@ -148,7 +153,6 @@ contexts: pop: true predicate-stmt: - - include: comments - match: "{{identifier}}" scope: entity.name.function.midas - match: '\('