One unannotated add, answering 5 to the integers and 3.75 to the floats

The boundary and the operators, which are the two halves of dyn being a type
rather than a word the checker tolerates.

Typed to dyn is implicit and dyn to typed is not, and the asymmetry is the
design: boxing loses nothing and can happen wherever a dyn is wanted, while
unboxing can fail at run time on a value the compiler cannot inspect, so it
happens only where somebody wrote a type. Both go through expect, because
expect is already the one place a wanted type meets a produced one, and every
annotating site already calls it.

Literals take their width from the dyn, not from the default. (defvar x dyn 5)
holds an i64 five: the ABI carries one integer width, so the defaulting question
never arises, and the literal is built at i64 rather than boxed after defaulting
to i32 -- which also means 3000000000 is a dyn integer.

An operator with one dyn operand is the runtime's. binary has already checked
the second operand against the first, so a mixed pair arrives with the typed
side boxed and the fold only has to call flan_dyn_add instead of adding. The
comparisons answer bool and not a dyn holding one, because a comparison is
almost always the test of an if; a program that wants it as a value boxes it
again for free at that boundary. = and != never trap -- two values of unrelated
types are unequal, not an error -- and the orderings do.

Types.equal had no Dyn case, so dyn was equal to nothing including itself.

print hands the whole value to the runtime rather than walking it: every other
arm of the structural printer exists because a Flan value carries no header and
only the compiler knows what it is, and a dyn is the exact reverse.

The compiler carries the dyn runtime the way it already carries flan_rt.c, with
the header pasted in front of the stub so there is one self-contained
translation unit and one contract.
This commit is contained in:
Joseph Ferano 2026-09-19 05:55:48 +07:00
parent 3e68089cde
commit c8091bdbf9
9 changed files with 301 additions and 6 deletions

View File

@ -848,7 +848,8 @@ let executable ?(opts = default) ?(csrcs = []) ?(lflags = []) ?(pnames = [])
cache key via [compile_c]'s [opt]/[tflags] digest see [cflags]. *)
let objs =
cc ~warn:runtime_warnings Runtime_src.source "flan_rt.c"
:: [ cc ~warn:runtime_warnings Runtime_src.dev_source "flan_dev.c" ]
:: cc ~warn:runtime_warnings Runtime_src.dev_source "flan_dev.c"
:: [ cc ~warn:runtime_warnings Runtime_src.dyn_source "flan_dyn.c" ]
(* wasi-libc's entry point, which is not [main]. See [wasm_main_source].
Not the browser's: emscripten's start code calls [main] under that name,
so the .ll's @main is already the entry point and the shim would be a
@ -1102,7 +1103,8 @@ let macro_module ?(opts = default) ?(csrcs = []) ?(lflags = []) ~macros
let cc ?(warn = []) src name = compile_c ~opts ~tflags ~warn ~src ~name () in
let objs =
cc ~warn:runtime_warnings Runtime_src.source "flan_rt.c"
:: [ cc ~warn:runtime_warnings Runtime_src.dev_source "flan_dev.c" ]
:: cc ~warn:runtime_warnings Runtime_src.dev_source "flan_dev.c"
:: [ cc ~warn:runtime_warnings Runtime_src.dyn_source "flan_dyn.c" ]
@ (match p.Tast.cshim with
| [] -> []
| parts ->

View File

@ -1364,10 +1364,131 @@ let type_id name =
let restart_sig tys =
"(" ^ String.concat " " (List.map Types.to_string tys) ^ ")"
(* ── The dyn boundary ───────────────────────────────────────────────────
Typed to dyn is implicit and dyn to typed is not. That asymmetry is the
whole of the design and it is worth saying why it is not arbitrary.
Boxing loses nothing: the value goes in and the runtime records what it was.
It can happen anywhere a dyn is wanted without a reader being surprised,
because nothing about the program's meaning turns on it. Unboxing can fail,
at run time, on a value the compiler cannot inspect -- so it happens only
where somebody *wrote a type*: a typed parameter, a typed binding, a typed
field. Those are the places a reader already understands as a claim about
what a value is, and a claim that can be wrong is exactly what a trap is
for. Nowhere else does the compiler decide a dyn is an i64 on its own.
Both directions go through [expect], because [expect] is already the one
place a wanted type meets a produced one. Every site that annotates -- and
only those sites -- calls it with [~want].
Milestone 1 boxes the scalars and refuses everything else by name. A typed
container crossing into dyn is the interesting refusal: [(Vec i64)] has a
representation the dyn runtime does not know how to walk, and heterogeneity
at milestone 1 is served by the runtime's own vector behind
[flan_dyn_vec_new] instead. That is a "not yet" and says so. *)
let dyn_i64 = Types.Int Types.I64
let dyn_f64 = Types.Float Types.F64
(* Widening to the one width the ABI carries. runtime/flan_dyn.h boxes integers
as [i64] and floats as [f64] and offers no other width, which is the
language's "dyn integers are i64" written where it is enforced. The cast is
explicit in the tree rather than left to the backend: a [Cast] is what the
language's own conversions emit, and a widening one loses nothing. *)
let widen loc (want : Types.t) (e : Tast.expr) =
if Types.equal want e.Tast.ty then e
else mk loc want (Tast.Prim (Tast.Cast want, [ e ]))
let unboxable t =
match t with
| Types.Int Types.I64 | Types.Float Types.F64 | Types.Bool -> true
| _ -> false
(* The sentence a refusal at this boundary gives. It names the type and says
which direction failed, because "expected dyn, found (Vec i64)" would read
as a type error the programmer could fix by writing something else, and
there is nothing else to write -- the feature is not there yet. *)
let no_dyn_yet loc ~into t extra =
Loc.failk "check/dyn-not-yet" loc
"%s does not cross into %s yet%s"
(Types.to_string t) (if into then "dyn" else "a written type") extra
let box loc (e : Tast.expr) : Tast.expr =
let dyn sym args = rt loc Types.Dyn sym args in
match e.Tast.ty with
| Types.Dyn -> e
| Types.Int _ -> dyn "flan_dyn_from_i64" [ widen loc dyn_i64 e ]
| Types.Float _ -> dyn "flan_dyn_from_f64" [ widen loc dyn_f64 e ]
(* The ABI takes an [int32_t], because a C signature that says [_Bool] is a
width argument nobody wants to have. *)
| Types.Bool -> dyn "flan_dyn_from_bool" [ widen loc (Types.Int Types.I32) e ]
(* A string is ptr+len and arrives as two arguments, the way every other
(ptr, len) entry point in the runtime takes one. The runtime copies: the
bytes may be a literal or a slice of a buffer the program goes on to
write. *)
| Types.String -> dyn "flan_dyn_from_bytes" [ e ]
(* Unit does not box. A value of the zero-sized type carries nothing for a
dyn word to hold, and [nil] -- which is what an [if] with no else answers
in dyn context -- is a different thing with a different constructor. The
two get confused if unit is allowed to become one. *)
| Types.Unit ->
Loc.failk "check/dyn-unit" loc
"() does not box into dyn — a value of the zero-sized type carries \
nothing a dyn could hold. The absent dyn value is nil, which is what an \
if with no else branch answers here"
| Types.Never -> e
| Types.Vec _ | Types.Map _ | Types.Slice _ | Types.Array _ ->
no_dyn_yet loc ~into:true e.Tast.ty
". The dyn container at this milestone is the runtime's own, from \
(vec-new dyn); a typed container has a representation the dyn runtime \
cannot walk"
| Types.Named _ | Types.Enum _ | Types.Option _ | Types.Ptr _
| Types.Alloc | Types.Fn _ | Types.Var _ ->
no_dyn_yet loc ~into:true e.Tast.ty ""
let unbox loc (want : Types.t) (e : Tast.expr) : Tast.expr =
let need sym ty = rt loc ty sym [ e ] in
match want with
| Types.Int Types.I64 -> need "flan_dyn_need_i64" dyn_i64
| Types.Float Types.F64 -> need "flan_dyn_need_f64" dyn_f64
| Types.Bool ->
(* The ABI answers an [int32_t]; [bool] is an [i1]. The narrowing is the
language's own cast and cannot fail the runtime already decided the
value was a bool, so what comes back is 0 or 1. *)
widen loc Types.Bool (need "flan_dyn_need_bool" (Types.Int Types.I32))
(* Every other width is refused rather than served by a need_i64 and a
truncation. This language has no implicit narrowing anywhere, and putting
one at the boundary where a value's type was *already* uncertain is the
worst place in the program to start: the annotation would read as a check
and would be a silent discard of the high bits. The ABI grows a per-width
entry point when there is a reason to; until then the spelling that works
is an i64 and an explicit conversion after it. *)
| Types.Int _ | Types.Float _ ->
no_dyn_yet loc ~into:false want
(Printf.sprintf
" — the dyn runtime carries integers as i64 and floats as f64, so \
take it as %s and convert"
(if Types.is_numeric want && (match want with Types.Float _ -> true | _ -> false)
then "f64" else "i64"))
| _ -> no_dyn_yet loc ~into:false want ""
let expect loc ~want (got : Tast.expr) =
match want with
| None -> got
| Some w ->
(* The boundary, and the only implicit conversion in the language. It runs
before [fits] rather than instead of it: what comes back is an ordinary
expression of the wanted type, and if the coercion did not produce one
the usual message is still the one that reports it. *)
let got =
match w, got.Tast.ty with
| Types.Dyn, Types.Dyn -> got
| Types.Dyn, _ -> box loc got
| _, Types.Dyn when Types.fits ~expected:w ~actual:Types.Dyn -> got
| _, Types.Dyn -> unbox loc w got
| _ -> got
in
if Types.fits ~expected:w ~actual:got.Tast.ty then got
else
fail loc "expected %s, found %s" (Types.to_string w)
@ -1698,6 +1819,12 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
match e.Ast.e with
| Ast.Int n -> int_literal loc ~want n
| Ast.Byte b -> int_literal loc ~want ~default:Types.U8 (Int64.of_int b)
(* The float literal's own dyn case, for the reason the integer's has one:
the ABI carries one width and the literal is built at it. f64 is already
what an unconstrained float literal defaults to, so this only has to stop
the "expected dyn, found the float literal" arm below from firing. *)
| Ast.Float x when want = Some Types.Dyn ->
box loc (mk loc dyn_f64 (Tast.Float (x, Types.F64)))
| Ast.Float x ->
let k =
match want with
@ -1932,6 +2059,16 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
and int_literal loc ~want ?(default = Types.I32) n =
match want with
| Some (Types.Int k) -> mk loc (Types.Int k) (Tast.Int (in_range loc k n, k))
(* A literal in dyn position takes i64 and not the i32 an unconstrained one
defaults to. This is where "dyn integers are i64" stops being a statement
about the ABI and becomes one about the language: [(defvar x dyn 5)] holds
an i64 five, and the defaulting question a wider set of boxes would raise
never arises because there is only the one box. Handled here rather than
left to [expect] so the literal is *built* at the right width the range
check below is the one that matters, and 3000000000 is a dyn integer even
though it is not an i32. *)
| Some Types.Dyn ->
box loc (mk loc dyn_i64 (Tast.Int (in_range loc Types.I64 n, Types.I64)))
(* An untyped integer constant is usable where a float is wanted, as in
Odin. A float literal is never usable where an integer is wanted. *)
| Some (Types.Float k) ->
@ -3221,6 +3358,14 @@ and fold_left_prim ctx ~want loc name p ok what args =
match args with x :: y :: rest -> x, y, rest | _ -> assert false
in
let a, b = binary ctx name loc ~want:(numeric_want want) [ x; y ] in
(* One dyn operand makes the whole fold dyn. [binary] has already checked the
second against the first, so a mixed pair arrives with the typed side
boxed [(+ x 1)] over a dyn [x] checked the literal at dyn and got an i64
five in a box. What is left is to fold with the runtime's operator instead
of the machine's. *)
if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then
dyn_fold ctx ~want loc name [ a; b ] rest
else begin
unconstrained ctx.env loc name ~needs:"numeric?" a.Tast.ty;
(* Past [unconstrained] a variable here is one the [where] clause admitted,
so the concrete predicate below has nothing to say about it it is
@ -3236,6 +3381,37 @@ and fold_left_prim ctx ~want loc name p ok what args =
rest
in
expect loc ~want acc
end
(* The dyn lowering of a fold: one call per operator application, left to
right, each taking and answering a dyn word. The typed side of a mixed pair
is boxed on the way in [box] is the identity on something already dyn, so
this needs no case analysis of its own. *)
and dyn_fold ctx ~want loc name first rest =
let sym =
match name with
| "+" -> "flan_dyn_add" | "-" -> "flan_dyn_sub"
| "*" -> "flan_dyn_mul" | "/" -> "flan_dyn_div"
| "%" -> "flan_dyn_rem"
| _ ->
(* Bitwise and shift operators land here if they ever admit a dyn
operand. They do not: the runtime carries no bitwise entry points,
and an integer operation on a value that might be a float is not
something to guess at. *)
no_dyn_yet loc ~into:false Types.Dyn
(Printf.sprintf " — %s has no dyn form" name)
in
let apply acc b = rt loc Types.Dyn sym [ acc; box loc b ] in
let acc =
match first with
| [ a; b ] -> apply (box loc a) b
| _ -> assert false
in
let acc =
List.fold_left (fun acc arg -> apply acc (check ctx ~want:Types.Dyn arg))
acc rest
in
expect loc ~want acc
(* ── Allocation failure, spec-memory.md ────────────────────────────────
No allocating operation returns an error and none can fail silently. When
@ -3520,10 +3696,14 @@ and named_call ctx ~want loc name args =
| "%" ->
arity loc name 2 args;
let a, b = binary ctx name loc ~want:(numeric_want want) args in
if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then
dyn_fold ctx ~want loc name [ a; b ] []
else begin
unconstrained ctx.env loc name ~needs:"numeric?" a.Tast.ty;
if not (Types.is_numeric a.Tast.ty || generic_ty a.Tast.ty) then
fail loc "%s takes numbers, found %s" name (Types.to_string a.Tast.ty);
prim Tast.Rem a.Tast.ty [ a; b ]
end
| "=" | "!=" | "<" | "<=" | ">" | ">=" ->
let p = match name with
| "=" -> Tast.Eq | "!=" -> Tast.Ne | "<" -> Tast.Lt
@ -3531,6 +3711,35 @@ and named_call ctx ~want loc name args =
in
arity loc name 2 args;
let a, b = binary ctx name loc ~want:None args in
(* A comparison with a dyn operand answers a *bool*, not a dyn, even though
the runtime's own entry point answers a dyn holding one. The reason is
where the result goes: a comparison is overwhelmingly the test of an
[if] or a [while], and those want an i1. So the need_bool is applied
here, once, and a program that really wants the comparison as a dyn
value boxes it again on the way into wherever it is going which [box]
does for free at that boundary.
[=] and [!=] are the pair that never traps: the runtime compares
structurally and answers false for values of unrelated types, because
two things being unalike is the answer to "are these equal", not an
error. The orderings do trap, and rightly there is no true answer to
whether a string is less than a vector. *)
if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then begin
let sym =
match name with
| "=" | "!=" -> "flan_dyn_eq"
| "<" -> "flan_dyn_lt" | "<=" -> "flan_dyn_le"
| ">" -> "flan_dyn_gt" | _ -> "flan_dyn_ge"
in
let cmp = unbox loc Types.Bool (rt loc Types.Dyn sym [ box loc a; box loc b ]) in
(* [!=] has no entry point of its own: there is one structural equality
and the negation is an [i1] flip the backend folds away. *)
let r =
if String.equal name "!=" then mk loc Types.Bool (Tast.Prim (Tast.Not, [ cmp ]))
else cmp
in
expect loc ~want r
end else begin
(* [=] and [!=] admit one type [<] does not: a handle, which is a pair of
numbers in one word and where "the same entity" is the question the
type exists to answer. Ordering handles would order a slot index, which
@ -3548,6 +3757,7 @@ and named_call ctx ~want loc name args =
"%s compares machine numbers; %s has no built-in comparison \
(plan.org, Types)" name (Types.to_string a.Tast.ty);
prim p Types.Bool [ a; b ]
end
| "not" ->
arity loc name 1 args;
prim Tast.Not Types.Bool [ check ctx ~want:Types.Bool (List.hd args) ]

View File

@ -4001,7 +4001,8 @@ let merged_executable ~opts ~csrcs ~lflags ~pnames (p : Tast.program) ~out ~ll =
let cc src name = compile_c ~opts ~tflags ~src ~name () in
let objs =
(cc Runtime_src.source "flan_rt.c"
:: [ cc Runtime_src.dev_source "flan_dev.c" ])
:: cc Runtime_src.dev_source "flan_dev.c"
:: [ cc Runtime_src.dyn_source "flan_dyn.c" ])
@ (match p.Tast.cshim with
| [] -> []
| parts ->

View File

@ -26,11 +26,19 @@
; so there is only ever one copy to edit. flan_dev.c goes into a dev build
; only — it is the run-time name lookup a REPL needs and a release build has
; no use for.
; [dyn_source] is runtime/flan_dyn_stub.c with runtime/flan_dyn.h pasted in
; front of it, because the generated module is one string and the stub includes
; the header by name. THE MERGE REPLACES THE STUB WITH runtime/flan_dyn.c and
; this rule keeps its shape — the header stays the contract both sides are
; diffed against, and concatenating it here is what makes the compiler carry a
; self-contained translation unit the way it already carries flan_rt.c.
(rule
(target runtime_src.ml)
(deps
%{workspace_root}/runtime/flan_rt.c
%{workspace_root}/runtime/flan_dev.c)
%{workspace_root}/runtime/flan_dev.c
%{workspace_root}/runtime/flan_dyn.h
%{workspace_root}/runtime/flan_dyn_stub.c)
(action
(with-stdout-to
runtime_src.ml
@ -39,4 +47,7 @@
(cat %{workspace_root}/runtime/flan_rt.c)
(echo "|c}\n\nlet dev_source = {c|\n")
(cat %{workspace_root}/runtime/flan_dev.c)
(echo "|c}\n\nlet dyn_source = {c|\n")
(cat %{workspace_root}/runtime/flan_dyn.h)
(cat %{workspace_root}/runtime/flan_dyn_stub.c)
(echo "|c}\n")))))

View File

@ -2833,6 +2833,36 @@ declare i64 @flan_alloc_fail_align()
declare i64 @flan_alloc_fail_id()
declare i64 @flan_alloc_budget(ptr)
declare void @flan_alloc_set_budget(ptr, i64)
; The dynamic runtime, runtime/flan_dyn.h. A flan_dyn is one machine word and
; is spelled i64 here because the typedef says uint64_t; nothing in this file
; ever looks inside one, so every operation on a dyn value is one of these.
declare i64 @flan_dyn_nil()
declare i64 @flan_dyn_from_i64(i64)
declare i64 @flan_dyn_from_f64(double)
declare i64 @flan_dyn_from_bool(i32)
declare i64 @flan_dyn_from_bytes(ptr, i64)
declare i64 @flan_dyn_vec_new()
declare i64 @flan_dyn_add(i64, i64)
declare i64 @flan_dyn_sub(i64, i64)
declare i64 @flan_dyn_mul(i64, i64)
declare i64 @flan_dyn_div(i64, i64)
declare i64 @flan_dyn_rem(i64, i64)
declare i64 @flan_dyn_lt(i64, i64)
declare i64 @flan_dyn_le(i64, i64)
declare i64 @flan_dyn_gt(i64, i64)
declare i64 @flan_dyn_ge(i64, i64)
declare i64 @flan_dyn_eq(i64, i64)
declare i64 @flan_dyn_len(i64)
declare i64 @flan_dyn_at(i64, i64)
declare void @flan_dyn_set_at(i64, i64, i64)
declare void @flan_dyn_push(i64, i64)
declare void @flan_dyn_print(i64)
declare i64 @flan_dyn_need_i64(i64)
declare double @flan_dyn_need_f64(i64)
declare i32 @flan_dyn_need_bool(i64)
declare void @flan_dyn_root_push(ptr)
declare void @flan_dyn_root_pop(i64)
declare void @flan_gc_init()
declare void @flan_dev_reg_enable()
declare void @flan_dev_reg_note_vec(ptr, i64, ptr, i64)
declare void @flan_dev_reg_note_map(ptr, i64, i64, ptr, i64)

View File

@ -352,5 +352,18 @@ let rec render c depth (e : Tast.expr) : Tast.expr list =
(Tast.While
(cond, lit " " :: render c (depth + 1) elem, [ step ]));
lit "]" ])) ]
(* The one type this walk does not walk. Every other arm is here because a
Flan value carries no header and only the compiler knows what it is; a
dyn value is the exact opposite the runtime knows and the compiler
does not so the printing belongs on the side that can see the tag, and
the walk hands the whole value over.
The cost is that it writes to stdout itself rather than through
[c.emit], so a dyn printed at the REPL arrives on the program's output
and not in the REPL's buffer. Fixing that means an emit-shaped dyn
printer in the runtime a second entry point taking the sink and it
is not milestone 1's. *)
| Types.Dyn ->
[ unit_ (Tast.Prim (Tast.Rt "flan_dyn_print", [ e ])) ]
| t ->
fail loc "no printer for %s" (Types.to_string t)

View File

@ -97,7 +97,11 @@ let rec equal a b =
match a, b with
| Int x, Int y -> x = y
| Float x, Float y -> x = y
| Bool, Bool | String, String | Unit, Unit | Never, Never -> true
(* [Dyn] is equal to itself and to nothing else. Two dyn values may hold
different things at run time, which is the point of the type and is not
this function's question: this is identity of *static* types, and there is
one dyn type the way there is one string type. *)
| Bool, Bool | String, String | Unit, Unit | Never, Never | Dyn, Dyn -> true
| Named x, Named y | Enum x, Enum y -> String.equal x y
| Slice x, Slice y -> equal x y
| Array (n, x), Array (m, y) -> Int64.equal n m && equal x y

View File

@ -25,7 +25,16 @@
#include <string.h>
#include <unistd.h>
#include "flan_dyn.h"
/* The compiler carries this file as one string with flan_dyn.h pasted in front
* of it (lib/dune), and in that form there is no header on disk to find. The
* probe keeps the file compilable both ways: standalone against the real
* header, and concatenated, where the declarations are already above. The
* header's own include guard makes the two agree. */
#if defined(__has_include)
# if __has_include("flan_dyn.h")
# include "flan_dyn.h"
# endif
#endif
/* flan_rt.c's own [rt_trap] is static, so this mirrors it rather than calling
* it: print the sentence, offer the name to the dev daemon's hook, and leave

View File

@ -0,0 +1,15 @@
;;;; An unannotated defn, called at two different types.
;;;;
;;;; [(defn add [x y] dyn (+ x y))] states no type for either parameter, so both
;;;; are dyn, and the + in the body is the dyn one: a call into the runtime that
;;;; decides on what the two words actually hold. The same function serves the
;;;; integer call and the float call, which is the whole of what the feature
;;;; buys and is not something the typed language could express at all.
(defn add [x y] dyn (+ x y))
(defn main [] ()
(print (add 2 3))
(print "\n")
(print (add 1.5 2.25))
(print "\n"))