← Playground Medaka: Advanced Topics
☰

#Effects VII: Reference and Open Edges

This chapter is the lookup page for the topic: every spelling on one table, the diagnostics you are likely to meet and where they are explained, and the places where the system is known not to express something yet.

#Spellings

Written Meaning Chapter
f : A -> B pure function, the row is <> I
f : A -> <IO> B may perform any of the eleven host labels I
f : A -> <Stdout, Clock> B may perform exactly those labels I
v : <Stdout> Int a value whose computation performs Stdout I
v : <> Int a value computed purely (checked) I
v : Int a value; its row is inferred, not promised I
f : (a -> <e> b) -> <e> b performs whatever the callback performs II
f : … -> <Stdout | e> b Stdout, plus the callback's row II
f : … -> <e | e2> b the join of two independent rows II
effect Audit declare an atomic label III
export effect Audit declare and export one III
extern f : A -> <FFI "c"> B a foreign call; FFI is mandatory III
extern f : A -> <FFI "c/libm"> B a foreign call, naming the library III
effect Store Prefix a label whose parameter is a path or host IV
effect Var Set a label whose parameter is a set of names IV
effect Http Product (Host : Prefix, Method : Set) a label with axes IV
<Store> the whole domain IV
<Store "cfg/*"> a pattern: everything under cfg/ IV
<Store "cfg/app.toml"> an exact element: that path only IV
<Store "cfg/*", Store "data/*"> either subtree, never their common prefix IV
<Var {"HOME", "PATH"}> a set element IV
<Http Host="a.com/*" Method={"GET"}> a product element; an unwritten axis is its whole axis IV
(path : String) -> <Store path> B a named argument; the caller's path is the authority IV
(dir : String @Store) -> String @dir a named argument with its domain written; charges nothing IV
(dir : String @Store*) -> String @dir a pattern-ranging named argument; dir ++ x stays within dir IV
String @p a string known to lie within p IV
String @(a | b) a string within either authority IV
v : String @"cfg/*" a value within a written bound; a use carries the bound IV
(a <= d) => … a relation check prints on an unsigned binding IV
data H (p : Authority Store) = H (String @p) a type indexed by an authority V
data DataDir (d : Authority Store*) = DataDir (String @d) an index that ranges over patterns; a bare d in a signature takes that range V
H path / H p / H "cfg/*" / H * index forms: named argument, variable, literal, whole domain V
data Any = Any (p : Authority Store) (H p) an existential index V
extern data Socket (h : Authority Net) an opaque indexed type produced only by the runtime V
data Job (e : Effect) a = … a type indexed by a row VI
Job <> a / Job <Stdout> a a written index VI
Job (e | e2) a a joined index VI

#Commands

Command What it shows
medaka check file.mdk the inferred scheme, row included, of every top-level binding
medaka manifest file.mdk [--fn name] the entry's verified capability row as TOML
medaka check-policy file.mdk --fn name --allow L1,L2=param,… accept or reject against an allow list

#Diagnostics

The first words of each message, and where the rule behind it is explained.

Message begins Rule Chapter
Effectful value used where <…> is allowed, but it performs <…> a body, alias, stored value, or index exceeds its bound I, II, VI
Binding '…' performs <…>, but the row it must fit, <a>, is chosen by its caller a declared effect variable is rigid II
Binding '…' runs the effect row <a>, which its caller chooses a callback is applied under a pure arrow II
this statement's value (…) is silently discarded a non-Unit statement I
Unknown effect: … a label nobody declared III
Ambiguous effect label: … two modules' labels with one spelling in scope III
Foreign declaration '…' does not name the 'FFI' effect an extern without FFI III
Foreign declaration '…' redeclares a built-in runtime name with a NARROWER effect row a catalog name redeclared too narrowly III
Invalid effect parameter on <…> a written element the domain refuses: an empty element, or more than 16 members IV
Binding '…' reaches "…" where only … is admitted a body under a named authority reaches a value it did not derive from it IV
Binding '…' reaches … where its declared bound admits only … a returned value, constructor or existential exceeds a written bound IV, V
The qualifier names '…', but no binder domain, effect atom or index in this signature names '…' a qualifier with no domain IV
'…' needs "…" to lie within "…" here a use violates a relation the binding's inferred type carries IV
Authority index mismatch an authority index is invariant, and an index row must cover each atom its tail cannot take V, VI
`"…"` is an exact element of `…`'s domain, but it fills an `Authority …*` slot a written exact element where only a pattern goes V
'…' ranges over every authority of `…`, but it fills an `Authority …*` slot a binder without the * fills a pattern slot IV, V
`Authority …*` ranges over the patterns of `…`'s domain / `@…*` ranges over … a * on a Set label, or a Product whose first axis is a Set IV
A pattern-ranging authority index (an `Authority L*` slot) is equated with an index equality with an exact element V
Effect index mismatch an effect index is invariant VI
This pattern opens the existential authority '…' only a clause or arm can open one V
Constructor '…' of public type '…' carries its authority parameter '…' in no field a public export data constructor that proves nothing V
Type parameter … is used as an effect row … but its head does not declare it one (e : Effect) is missing VI

#Open edges

These are the places where the current compiler does not yet express something the design intends, where it is stricter than it needs to be, or where a guarantee stops short. Where an issue is filed, its number is the thing to search for.

  • File confinement checks a path, then uses it. The runtime resolves the path to check it, and the operating system resolves it again to open it. A symlink swapped inside the granted tree between the two can escape it. Closing this needs resolution beneath the granted directory (openat with O_NOFOLLOW, or openat2). #3585

  • The wasm host confines a file operation as native does, with three differences. A pattern grant such as "cfg/*" builds for medaka build --target wasm, and the host checks each path, compared as bytes, against the grant the call writes and against each declared bound it runs under. The whole domain and exact paths build, and so does a wrapper such as io.readLines or fs.*, which only passes on the grant its caller writes. The differences: the browser's in-memory file system has no symbolic links; the host measures paths against Linux's 4096-byte PATH_MAX, where a native build on macOS has 1024; and a path holding a NUL byte is an Err on wasm, where native reads it only up to the NUL. #3590

  • An opened existential or an instance head's index grants the whole domain. Neither has a caller to supply an authority. The declaration that reaches one is held to its declared row, which is the bound, rather than the value's index. #3591

  • Net authority is a string. A Net bound confines the strings a program passes. A host part such as a.com/../x, a percent-encoded byte, or a . segment is not normalized, and the socket externs receive no grant. #3592

  • There is no written syntax for a relation. A binding whose inferred type carries a context such as (a <= d) => (the relation the compiler kept, see chapter IV) must stay unsigned. #3566

  • A relation cannot be shared by a recursive group. Two mutually recursive functions over a captured handle are refused where one function would be accepted. #3482

  • check prints effect and type variables from one alphabet. The issue's title describes an older symptom, since fixed; the naming is what remains. #2583

#Further reading