Repository navigation
TScert: print TypeScript for verification under experimental -bs-emit-ts - #9211
Draft
cristianoc wants to merge 8 commits into
Draft
cristianoc wants to merge 8 commits into
cristianoc wants to merge 8 commits into
Conversation
Why:
A feasibility study for checking ReScript output with TScert, which reads
TypeScript whose top-level functions annotate their parameters and
result. The flag writes `.res.ts` (`.mts` for `.mjs`) in place of the
JavaScript output, annotates each top-level function from the typed tree,
and puts the module's type declarations at the top through genType's
translation. The annotations are keyed by `Ident.t` (name and stamp), so
one reaches the output only when the J IR prints the identifier the
typed tree bound; `RESCRIPT_EMIT_TS_DEBUG=1` reports, per printed
top-level function, whether its stamp and its parameters' stamps are the
typed tree's.
JS modified (top-level functions under -bs-emit-ts):
Example:
type point = {x: int, y: int, label: string}
let moveX = (p: point, dx: int) => {...p, x: p.x + dx}
Before (js):
function moveX(p, dx) {
return {
x: p.x + dx | 0,
y: p.y,
label: p.label
};
}
After (js): Rec.res.ts
export type point = {
readonly x: number;
readonly y: number;
readonly label: string
};
function moveX(p: point, dx: number): point {
return {
x: p.x + dx | 0,
y: p.y,
label: p.label
};
}
Review: Do the stamps survive to the printer? For every binding
`let f = (…) => …` at the top level or in a nested module, uncurried,
inlined into its callers, private or exported, the printed function and each
of its parameters carry the typed tree's stamp. A function the optimizer
synthesizes, such as `let partial = curried(1)`, has fresh parameters and
is printed unannotated.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Cristiano Calcagno <cristianoc@users.noreply.github.com>
…t-ts
Why:
TScert's source fragment admits `export function f(…)` and refuses the
trailing export list `export { f, … }`. Under -bs-emit-ts a top-level
function exported under its own name is printed with `export` in front
and leaves the list; other exports, such as a module record or an alias,
stay in it. The printer is assumed to print a top-level function under
its source name.
JS modified (exports under -bs-emit-ts):
Example:
let add = (a: int, b: int) => a + b
Before (js):
function add(a: number, b: number): number {
return a + b | 0;
}
export {
add,
}
After (js):
export function add(a: number, b: number): number {
return a + b | 0;
}
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Cristiano Calcagno <cristianoc@users.noreply.github.com>
Why:
A polymorphic function printed its type variables without declaring
them, which tsc rejects, and each parameter's variables were named on
their own, so distinct variables shared the name T1. Optional labelled
arguments printed as mandatory `undefined | T` parameters.
JS modified (-bs-emit-ts type parameters):
Example:
let id = x => x
let second = (_x: 'a, y: 'b): 'b => y
Before (js):
export function id(x: T1): T1 {
return x;
}
export function second(_x: T1, y: T1): T1 {
return y;
}
After (js):
export function id<T1>(x: T1): T1 {
return x;
}
export function second<a, b>(_x: a, y: b): b {
return y;
}
JS modified (-bs-emit-ts optional labelled arguments):
Example:
let scale = (x: int, ~by=2) => x * by
let offset = (~from=0, x: int) => x - from
Before (js):
export function scale(x: number, byOpt: (undefined | number)): number {
…
export function offset(fromOpt: (undefined | number), x: number): number {
After (js):
export function scale(x: number, byOpt?: number): number {
…
export function offset(fromOpt: (undefined | number), x: number): number {
Review: Why does `fromOpt` keep `undefined | number`? TypeScript requires
every parameter after an optional one to be optional, so `?` goes only on
the optional arguments after the last mandatory one; a ReScript call
passes `undefined` for an omitted argument in either position.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Cristiano Calcagno <ccrisccris@gmail.com>
The build test tests/build_tests/emit_ts compiles seven examples with -bs-emit-ts and type-checks the checked-in .res.ts output with tsc --strict against declarations for the runtime functions the output imports. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Signed-off-by: Cristiano Calcagno <ccrisccris@gmail.com>
Why:
`option<t>` printed `undefined | t`, but `Some(v)` is a marker object
`{BS_PRIVATE_NESTED_SOME_NONE: depth}` when `v` is `undefined` or a
marker, so the type was false for `option<option<int>>` and
`option<unit>`. At a type parameter it was false at a nested
instantiation, and the runtime declarations
`valFromOption<A>(x: A): A`, `getOr` and `map` were false there: at
`A` the marker type, `valFromOption(some(undefined))` returns
`undefined`. A verifier taking those declarations accepted programs
returning wrong values.
Representation modified (option under -bs-emit-ts):
Before (representation):
option<int> ↦ undefined | number
option<option<int>> ↦ undefined | (undefined | number)
option<'a> ↦ undefined | a
After (representation):
option<int> ↦ undefined | number
option<option<int>> ↦ undefined | (undefined | number) | { readonly BS_PRIVATE_NESTED_SOME_NONE: number }
option<'a> ↦ undefined | a, with a extends string | number | boolean | bigint
option<'a> in a type declaration ↦ undefined | a | { readonly BS_PRIVATE_NESTED_SOME_NONE: number }
rule: the marker arm is printed where Typeopt.type_cannot_contain_undefined fails for the payload, the test that selects Psome over Psome_not_nest
JS modified (-bs-emit-ts type parameters):
Example:
let getOr = (o, d) =>
switch o {
| Some(v) => v
| None => d
}
Before (js):
export function getOr<T1>(o: (undefined | T1), d: T1): T1 {
After (js):
export function getOr<T1 extends string | number | boolean | bigint>(o: (undefined | T1), d: T1): T1 {
JS modified (-bs-emit-ts nested options):
Example:
type box<'a> = {v: option<'a>}
let keep = (o: option<option<int>>) => o
Before (js):
export type box<a> = { readonly v: (undefined | a) };
export function keep(o: (undefined | (undefined | number))): (undefined | (undefined | number)) {
After (js):
export type box<a> = { readonly v: (undefined | (
a
| { readonly BS_PRIVATE_NESTED_SOME_NONE: number })) };
export function keep(o: (undefined | (
(undefined | number)
| { readonly BS_PRIVATE_NESTED_SOME_NONE: number }))): …
Review: Why bound a type parameter by the primitives, and not by every
type without the marker key? `some(x)` and `valFromOption(x)` return `x`
exactly when `x` is not `undefined` and its key
`BS_PRIVATE_NESTED_SOME_NONE` reads `undefined`. A primitive owns no
keys and its untampered prototypes hold none. A TypeScript record type
admits values owning further keys, and a weak type
`{ BS_PRIVATE_NESTED_SOME_NONE?: undefined }` rejects every record that
does not state that field, so no wider bound is both true and usable.
Review: What does the bound refuse? A call of such a function at a
non-primitive instantiation, `getOr` of an `option<point>` say, fails
tsc. A nested match such as `Some(Some(n))` fails tsc too: the marker
arm erases the depth, so no true declaration of `valFromOption` returns
the payload type there.
The runtime declarations in runtime-dts state the same bound, each line
audited against Primitive_option.res and Stdlib_Option.res, and
Stdlib_Array.reduce's callback receives the index and the array that
Array.prototype.reduce passes. The Nest example shows the marker arm and
the bound.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Cristiano Calcagno <ccrisccris@gmail.com>
…rrows
Why:
The marker arm reached only options genType translated from a type
expression as `option<t>`. A type declaration's manifest, translated
from its core type, and an optional argument of a function type, whose
option genType rebuilds, still printed `undefined | t` for a payload
that can hold a marker. An optional argument of a function type in a
type declaration also lost its option: the core type of `~x: int=?` is
its payload `int`, which genType read as the whole argument.
JS modified (-bs-emit-ts type declarations):
Example:
type opt<'a> = option<'a>
type callback = (~x: option<int>=?) => int
type cb2 = (~x: int=?) => int
Before (js):
export type opt<a> = (undefined | a);
export type callback = (x:(undefined | number)) => number;
export type cb2 = (x:number) => number;
After (js):
export type opt<a> = (undefined | (
a
| { readonly BS_PRIVATE_NESTED_SOME_NONE: number }));
export type callback = (x:(undefined | (
(undefined | number)
| { readonly BS_PRIVATE_NESTED_SOME_NONE: number }))) => number;
export type cb2 = (x:(undefined | number)) => number;
Review: Does this change genType's own output? Only where a type
declaration has an optional argument in a function type, which genType
printed without its `undefined`; the marker arm is off outside
-bs-emit-ts, and the gentype tests' outputs are unchanged.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Cristiano Calcagno <ccrisccris@gmail.com>
Why:
The printer drops a lone `return;`, so such a function prints an empty
body. TypeScript requires a `return` in a function whose declared result
type is other than `undefined`, `void` or `any`, and rejects the empty
body with TS2355.
JS modified (-bs-emit-ts body that is only return;):
Example:
let none = (): option<int> => None
Before (js):
export function none(): (undefined | number) {
}
After (js):
export function none(): (undefined | number) {
return;
}
Review: Does JavaScript output change? No: the statement is kept only
under -bs-emit-ts.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Cristiano Calcagno <ccrisccris@gmail.com>
… unwrapping The emit_ts test writes what tsc --strict reports for the generated TypeScript to a checked-in tsc.txt, so an example the printed types refuse is checked in with its diagnostics. NestMatch unwraps nested options: a nested match and the generic getOr at 'a = option<int>, which the primitive bound on Primitive_option refuses. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Signed-off-by: Cristiano Calcagno <ccrisccris@gmail.com>
ChangelogNo changelog entry. Semantic Diff8 commits · Full page Print TypeScript for a module under the experimental -bs-emit-ts flag571a0cc · cristianoc + Claude · Nov 04, 2026, 01:34 UTC
JS modified (top-level functions under -bs-emit-ts) type point = {x: int, y: int, label: string}
let moveX = (p: point, dx: int) => {...p, x: p.x + dx}
-function moveX(p, dx) {
+export type point = {
+ readonly x: number;
+ readonly y: number;
+ readonly label: string
+};
+
+function moveX(p: point, dx: number): point {
return {
x: p.x + dx | 0,
y: p.y,
label: p.label
};
}Review
Print an exported top-level function as export function under -bs-emit-ts8ec2de4 · cristianoc + Claude · Nov 04, 2026, 01:36 UTC
JS modified (exports under -bs-emit-ts) let add = (a: int, b: int) => a + b
-function add(a: number, b: number): number {
+export function add(a: number, b: number): number {
return a + b | 0;
}
-
-export {
- add,
-}Print type parameters and optional parameters under -bs-emit-ts2a07f4e · cristianoc + Claude · Nov 04, 2026, 02:50 UTC
JS modified (-bs-emit-ts type parameters) let id = x => x
let second = (_x: 'a, y: 'b): 'b => y
-export function id(x: T1): T1 {
+export function id<T1>(x: T1): T1 {
return x;
}
-export function second(_x: T1, y: T1): T1 {
+export function second<a, b>(_x: a, y: b): b {
return y;
}JS modified (-bs-emit-ts optional labelled arguments) let scale = (x: int, ~by=2) => x * by
let offset = (~from=0, x: int) => x - from
-export function scale(x: number, byOpt: (undefined | number)): number {
+export function scale(x: number, byOpt?: number): number {
…
export function offset(fromOpt: (undefined | number), x: number): number {Review
Check in the -bs-emit-ts examples and their TypeScript outputed4458a · cristianoc + Claude · Nov 04, 2026, 02:54 UTC The build test tests/build_tests/emit_ts compiles seven examples with -bs-emit-ts and type-checks the checked-in .res.ts output with tsc --strict against declarations for the runtime functions the output imports. Print option types true of the nested-option encoding under -bs-emit-tsbeb6284 · cristianoc + Claude · Nov 04, 2026, 04:32 UTC
Representation modified (option under -bs-emit-ts)
option<int> ↦ undefined | number
-option<option<int>> ↦ undefined | (undefined | number)
-option<'a> ↦ undefined | a
+option<option<int>> ↦ undefined | (undefined | number) | { readonly BS_PRIVATE_NESTED_SOME_NONE: number }
+option<'a> ↦ undefined | a, with a extends string | number | boolean | bigint
+option<'a> in a type declaration ↦ undefined | a | { readonly BS_PRIVATE_NESTED_SOME_NONE: number }
+rule: the marker arm is printed where Typeopt.type_cannot_contain_undefined fails for the payload, the test that selects Psome over Psome_not_nestJS modified (-bs-emit-ts type parameters) let getOr = (o, d) =>
switch o {
| Some(v) => v
| None => d
}
-export function getOr<T1>(o: (undefined | T1), d: T1): T1 {
+export function getOr<T1 extends string | number | boolean | bigint>(o: (undefined | T1), d: T1): T1 {JS modified (-bs-emit-ts nested options) type box<'a> = {v: option<'a>}
let keep = (o: option<option<int>>) => o
-export type box<a> = { readonly v: (undefined | a) };
-export function keep(o: (undefined | (undefined | number))): (undefined | (undefined | number)) {
+export type box<a> = { readonly v: (undefined | (
+ a
+ | { readonly BS_PRIVATE_NESTED_SOME_NONE: number })) };
+export function keep(o: (undefined | (
+ (undefined | number)
+ | { readonly BS_PRIVATE_NESTED_SOME_NONE: number }))): …The runtime declarations in runtime-dts state the same bound, each line audited against Primitive_option.res and Stdlib_Option.res, and Stdlib_Array.reduce's callback receives the index and the array that Array.prototype.reduce passes. The Nest example shows the marker arm and the bound. Review
Print the marker arm of option in aliases and optional arguments of arrowsccb1f14 · cristianoc + Claude · Nov 04, 2026, 04:39 UTC
JS modified (-bs-emit-ts type declarations) type opt<'a> = option<'a>
type callback = (~x: option<int>=?) => int
type cb2 = (~x: int=?) => int
-export type opt<a> = (undefined | a);
-export type callback = (x:(undefined | number)) => number;
-export type cb2 = (x:number) => number;
+export type opt<a> = (undefined | (
+ a
+ | { readonly BS_PRIVATE_NESTED_SOME_NONE: number }));
+export type callback = (x:(undefined | (
+ (undefined | number)
+ | { readonly BS_PRIVATE_NESTED_SOME_NONE: number }))) => number;
+export type cb2 = (x:(undefined | number)) => number;Review
Print a function body that is only return; under -bs-emit-tsb0a9c17 · cristianoc + Claude · Nov 04, 2026, 05:12 UTC
JS modified (-bs-emit-ts body that is only return;) let none = (): option<int> => None
export function none(): (undefined | number) {
+ return;
}Review
Record tsc's diagnostics for the emit_ts examples, with nested-option unwrapping8a1bb7e · cristianoc + Claude · Nov 04, 2026, 05:12 UTC The emit_ts test writes what tsc --strict reports for the generated TypeScript to a checked-in tsc.txt, so an example the printed types refuse is checked in with its diagnostics. NestMatch unwraps nested options: a nested match and the generic getOr at 'a = option<int>, which the primitive bound on Primitive_option refuses. |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## master #9211 +/- ##
==========================================
+ Coverage 81.73% 81.76% +0.02%
==========================================
Files 458 459 +1
Lines 65292 65480 +188
==========================================
+ Hits 53367 53539 +172
- Misses 11925 11941 +16
🚀 New features to boost your workflow:
|
rescript
@rescript/belt
@rescript/darwin-arm64
@rescript/linux-arm64
@rescript/linux-x64
@rescript/runtime
@rescript/win32-x64
commit: |
|
Developer playground preview: https://rescript-lang.github.io/rescript/dev-playground/?version=pr-9211 |
This branch has not been deployed
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.
Under the experimental
-bs-emit-tsflag, the compiler writes a module as TypeScript (.res.ts, or.mtsfor an.mjssuffix) in place of JavaScript. The goal is ReScript programs whose generated code is verified by TScert, a checker for TypeScript that accepts a function only with a proof that it is type-safe.What is printed
export function f(a: T): R. Types come from genType's translation: records become readonly object types, variants tagged unions. Locals stay unannotated.second<a, b>(_x: a, y: b): b.byOpt?: number. An earlier one printsfromOpt: undefined | number, because TypeScript requires every parameter after an optional one to be optional.export function.return;keeps the statement, which TypeScript requires when the result type is other thanundefined,voidorany.The option type
undefined | Tdescribesoption<T>exactly only whenTis neverundefined. The runtime representsSome(None)as a marker object{BS_PRIVATE_NESTED_SOME_NONE: 0}, one level deeper per nesting. The backend prints:option<int>,option<string>,option<record>undefined | Toption<option<int>>,option<unit>, aliasesundefined | T | Markeroption<'a>undefined | a, witha extends string | number | boolean | bigintOn a primitive,
Primitive_option.someandvalFromOptionreturn their argument, so the bound makes the runtime's declarations true. On an object that owns the marker key they do not:valFromOption(some({BS_PRIVATE_NESTED_SOME_NONE: 5, other: 1}))returns{BS_PRIVATE_NESTED_SOME_NONE: 5}. The bound is a limit, and some correct programs are refused: a generic function overoption<'a>used at a nested option, such asOption.getOrondict<option<int>>, and a nested matchSome(Some(n)).NestMatch.resrecords both.Tests
tests/build_tests/emit_tscompiles nine example modules with-bs-emit-tsand checks in their.res.tsoutput andtsc.txt, whattsc --strictreports for them against declarations of the runtime functions they import (runtime-dts/).tsc.txtholds four errors, all inNestMatch.res.ts, at the primitive bound.make testpasses.TScert
TScert is not released yet, so its results here are reported runs that a reviewer cannot reproduce. At TScert
12634735(2026-11-04), eight of the nine modules verify: Arith, Rec, Shape, Opt, Arr, Gen, OptArg and Nest. NestMatch is refused at the primitive bound.What a verification means: for inputs of the declared types, the function does not get stuck and does not return a value outside its result type. TScert takes imports at their declared types, so each verification assumes the hand-written declarations in
runtime-dts/are true of the runtime.Open
export {…}.Checklist
changes/README.md), or no release notes are needed and a maintainer should applychangelog:skip.CONTRIBUTING.md).git commit -s).🤖 Generated with Claude Code