← 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> B a foreign call; FFI is mandatory III
extern f : A -> <FFI "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

  • A wasm build cannot confine a file operation. Its host reads the path alone, so medaka build --target wasm refuses a call that writes a pattern grant such as "cfg/*" for a function that can reach a file operation, located at that call. 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.

  • 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.

  • 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.

  • 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