Mim Language Reference

This page is the reference for Mim surface syntax.

Note

The Tutorial shows every construct defined here in one annotated file. That page is lit/docs/tutorial.mim rendered by mim --output-md, and the file asserts what it shows with refly, so the test suite keeps the tour honest. It is also the playground's landing example - open it there to run and edit the tour in the browser.

Notation

This document uses a lightweight EBNF-style notation. A terminal is shaded, a nonterminal is not, and the lexical terminals I, L, X_n, C, and S have a colour of their own. Clicking a nonterminal or a lexical terminal traces its occurrences across the page. The meta-symbols are:

x ::= y  // defines the nonterminal x as y
x | y    // either x or y
(x y)    // grouping
x*       // zero or more x
x+       // one or more x
x?       // an optional x
[a-c]    // character range from a to c
[a-cx-z] // combines several ranges

For example, x ("," x)* is a comma-separated list of one or more x.

Note

Ranges only occur in the rules of the lexical terminals.

Every comma-separated list additionally accepts a trailing ,, as in (e, e, e,). The rules below don't spell this out.

Lexical Structure

Mim source files are UTF-8 encoded and are lexed from left to right. The lexer uses maximal munch, so ambiguities are resolved by taking the longest matching token. For example, >>= is tokenized as >> followed by =.

Note

<- is therefore a single token: x <- 1 is an insert, and a comparison against a negative literal needs a space, as in x < -1.

Terminals

The grammar refers to primary terminals. Some tokens have a second spelling - an ASCII-only one or a Unicode variant - that denotes the very same lexical token; these are the secondary terminals.

Primary Terminals

( ) [ ] { }
‹ › « »
→ ← => ⊥ ⊤ * □ λ
= , ; . : @ $ # | ∪
+ - / % == != < <= > >= << >>
<eof>

• . is the separator of a path, e.g. affine.Idx or core.nat.rem.
• +, -, *, /, %, ==, !=, <, <=, >, >=, <<, and >> are infix operators.
• # is an infix operator after an expression and a prefix one everywhere else; see Singletons and Nominal Newtypes.

Secondary Terminals

Primary	Secondary
→	->
←	<-
λ	lm
⊥	bot
⊤	top
*	★

Keywords

Bool Cn Fn I1 I8 I16 I32 I64 Idx Level Nat Rule Type
anx as axm cn con end extern ff fn fun
i1 i8 i16 i32 i64 import inj lam let match mod mutual
nom norm plugin priv pub rec ret rule tt use when where with

The following names are predefined aliases:

Alias	Expansion
tt	1₂
ff	0₂
Bool	Idx i1
I1	Idx i1
I8	Idx i8
I16	Idx i16
I32	Idx i32
I64	Idx i64
i1	2
i8	0x100
i16	0x1'0000
i32	0x1'0000'0000
i64	0

Note

2⁶⁴ doesn't fit into a Nat, so i64 is 0, which Idx reads as 2⁶⁴.

Lexical Terminals

The following terminals are defined by lexical rules.

I      ::= id
        |  "`" op
L      ::= dec+
        |  "0" ("b" | "B") bin+
        |  "0" ("o" | "O") oct+
        |  "0" ("x" | "X") hex+
        |  dec+ eE sign? dec+
        |  dec+ "." dec* (eE sign? dec+)?
        |  dec* "." dec+ (eE sign? dec+)?
        |  "0" ("x" | "X") hex+ pP sign? dec+
        |  "0" ("x" | "X") hex+ "." hex* pP sign? dec+
        |  "0" ("x" | "X") hex* "." hex+ pP sign? dec+
X_n    ::= dec+ sub+
        |  dec+ "_" dec+
        |  (dec+ | "0" ("b" | "B") bin+ | "0" ("o" | "O") oct+ | "0" ("x" | "X") hex+) ("i" | "I") dec+
C      ::= "'" (ascii_char | esc) "'"
S      ::= "\"" (ascii_string_char | esc)* "\""

Here I is an identifier, L is a numeric literal, X_n is an index literal of type Idx n, C is a character literal, and S is a string literal. The third form of X_n spells a bit width from 1 to 64 instead of n itself, so 23I32 is 23:I32 and 0xFFI8 is 255:I8. A literal never carries a sign; -23 is the signed literal expression instead. ` escapes an infix operator into an ordinary identifier, e.g. `+ .

The shorthand symbols used above are:

bin    ::= [0-1]
oct    ::= [0-7]
dec    ::= [0-9]
sub    ::= [₀-₉]
hex    ::= [0-9a-fA-F]
eE     ::= "e" | "E"
pP     ::= "p" | "P"
sign   ::= "+" | "-"
id     ::= ("_" | [a-zA-Z]) ("_" | [0-9a-zA-Z])*
op     ::= "+" | "-" | "*" | "/" | "%"
        |  "==" | "!=" | "<" | "<=" | ">" | ">="
        |  "<<" | ">>"
esc    ::= "\'" | "\\" | "\"" | "\0" | "\a" | "\b"
        |  "\f" | "\n" | "\r" | "\t" | "\v"

ascii_char is any ASCII character except \ and ', ascii_string_char is any ASCII character except \ and ", and a non-ASCII payload character is an error.

Comments

Supported comments:

/* multi-line comment */
// single-line comment
/// doc-comment

• /* ... */ comments do not nest.
• doc-comments are forwarded to generated Markdown output. Each line starting with /// contributes its remainder, minus one leading space, directly to the Markdown output. All other source lines are emitted verbatim inside a fenced code block.

Grammar

Mim is defined by a context-free grammar. Its terminals are the lexical elements defined above. The start symbol is f for file.

The main nonterminals used below are:

Symbol	Meaning
f	file
d	declaration
p	pattern
t	telescope
e	expression

Files and Imports

f ::= d*

A file is a sequence of declarations. Each file forms a module of its own that an import binds under a name.

• import foo; resolves the module name foo through the search path.
• import "some/dir/foo.mim"; resolves the path relative to the importing file first, then through the search path.
• If the resolved file name has no extension, .mim is appended.
• plugin foo; first loads the plugin foo and then imports the module with the same name. Only plugin loads a shared object; import never does.
• plugin "some/dir/foo"; looks for libmim_foo in some/dir below each plugin search path and takes foo.mim from wherever that library was found.
• The bound name defaults to the file name without its extension and must be an identifier; as overrides it.
• import foo as *; splices foo's public members into the current scope like a following use foo; would - except that foo itself is never bound; the same goes for plugin foo as *;. Since no name is needed, this form also accepts a file name that isn't an identifier.
• An import is priv unless declared pub: import foo; binds foo privately, while pub import foo; re-exports it, and pub import foo as *; re-exports every spliced member.
• A file is parsed, bound, and emitted exactly once, no matter how many modules import it. Importing a file that is still being parsed is an error.
• An import is an ordinary declaration, so it may sit wherever declarations may - inside a mod, a where block, or a function body - and binds its name in exactly that scope.

Paths and Modules

path ::= I ("." I)*

A path resolves its first component lexically and then walks into that module. A module is either an imported file or a mod declaration.

• Every component of a path is an identifier; a keyword is not allowed, not even after a ..
• . never reads a field out of a value; use # for that.
• An anx declaration is an ordinary member of its enclosing module and is found by the same path resolution as any other member; see Annex for what additionally makes it an annex.

Declarations

Mim supports the following declaration families. Most of them may be prefixed with a visibility (priv or pub), extern, and anx. These modifiers may be written in any order; the productions below only spell out which of them a declaration accepts at all. Visibility is a Mim-only, purely lexical fact - it has no effect on backend linkage or compiler registration. extern and anx are each independent of visibility, but not of each other: extern anx on the same declaration is a static error. Either one nudges the default visibility to pub (instead of the usual priv default) unless priv/pub is given explicitly, so e.g. priv anx and priv extern are legal and meaningful.

d      ::= vis? import (I | S) ("as" (I | "*"))? ";"
        |  vis? "use"  path    ("as" (I | "*"))? ";"
        |  vis? "mod" I d* "end"
        |  vis? "anx"? "let" p "=" e
        |  vis? "anx" I "=" path
        |  vis? ("extern" | "anx")? lam I dom+ (":" e)? "=" e
        |  vis?  "extern"          lam I fwd+ (":" e)? ";"
        |  vis? "anx"? "rec" I "=" e
        |  vis? "anx"? "nom" I ndom* "=" e
        |  vis? ("extern" | "anx")? "mutual" d* "end"
        |  vis? "axm" axm
        |  vis? ("rule" | "norm") I p ":" e ("when" e)? "=>" e
 
import ::= "import" | "plugin"
vis    ::= "priv" | "pub"
lam    ::= "lam" | "con" | "fun"
dom    ::= (p | "{" plist? "}") ("@" e)?
ndom   ::= p | "{" plist? "}"
fwd    ::= (p | t | "{" tlist? "}") ("@" e)?
axm    ::= I ":" e tail
        |  (I ".")? "(" (tag ("," tag)*)? ")" ":" e tail
tag    ::= I ("=" I)*
tail   ::= ("," I)? ("," L ("," L)?)?

Note

A declaration may be followed by a ;, as all examples on this page do; stray semicolons between declarations are skipped.

• import and plugin bind a file as a module, or splice its public members into the current scope; see Files and Imports.
• use path as I introduces I as another name for the module path denotes; use path as * splices that module's public members into the current scope instead, and a plain use path is sugar for the latter.
• mod groups declarations under a name; its body also sees the enclosing scope. Neither extern nor anx apply to it.
• let introduces a binding pattern.
• anx I = path declares I as an alias for the annex denoted by path.
• lam, con, and fun declare lambdas, continuations, and returning continuations. The declared name is already in scope inside its own body, so such a declaration is recursive. A forward reference only resolves within a mutual block. The corresponding expression forms are anonymous and cannot refer to themselves.
• The @ of a dom introduces its partial-evaluation filter.
• rec declares a recursive type. Its body must be a sigma, a variant, or a function type, as those are built as a mutable and filled in afterwards, so that I is already in scope inside it; its universe level is inferred from the body. A recursive function is declared with lam/con/fun instead.
• nom declares a nominal newtype; like rec, it is in scope inside its own body, but its body may be any type.
• mutual ... end groups declarations that may refer to each other, as in Lean. Its members must be rec, nom, lam, con, or fun declarations. Modifiers on mutual apply to every member; a member's own priv/pub overrides the group's.
• axm declares an axiom. A tag list declares several axioms of the same type at once, and each = I adds another name for that tag. Prefixed with a name as in axm nat.(add, sub): ..., the tags become members of a module of that name.
• An axm's tail is the normalizer, the curry counter, and the trip count, in that order; a trip count requires a curry counter.
• rule and norm declare rewrite rules.
• norm is the normalizing variant of rule.

Modifiers

• anx marks a declaration as an annex. It doesn't apply to mod, since a module is pure AST grouping, not a single value. axm is implicitly anx and may not combine with extern.
• extern is currently only meaningful on a lam/con/fun declaration and makes it
  • with a body a root of the World that stays reachable through Cleanup. Backends emit it under its source name with external linkage, so other translation units can call it, whereas a non-extern function gets a mangled name and internal linkage.
  • without a body (just ;) a declaration for another translation unit. Contrary to its extern annotation, such a stub is not external in the IR sense and, if unused, is removed like any other unreachable Def.

Visibility

• priv restricts a declaration to its lexical scope: a path may not cross into it from outside its enclosing mod; it is the default visibility unless extern or anx nudges it to pub.
• pub lifts that restriction, so a path from outside the enclosing mod may reach the declaration.
• Visibility belongs to the binding, not to the declaration it names: an import/plugin/use that splices as * re-binds someone else's declarations under its own visibility, so only a pub splice re-exports them, no matter how public they were in their own module.

Patterns and Telescopes

A pattern decomposes a value; a telescope describes a type.

p     ::= I (":" e)?
       |  "(" plist? ")"
       |  p "as" I
 
t     ::= I (":" e)?
       |  "[" tlist? "]"
       |  t "as" I
       |  e
 
plist ::= (p | g) ("," (p | g))*
tlist ::= (t | g) ("," (t | g))*
g     ::= I+ ":" e

These are two different things, not two spellings of one thing.

• A pattern p destructs a value into names that a body uses, so it only appears where a body exists.
• A telescope t describes a type and names a component only so that later components or the codomain may depend on it.
• The two grammars are identical except that a telescope additionally admits a bare e. Hence the whole difference: an unnamed element is a binder in (...) and a type in [...]. (a, b, c) binds three components with inferred types; [A, B, C] describes three unnamed components of those types.
• A group g distributes one annotated type over several names, as in (a b c: Nat, d e: Bool) or [a b c: Nat, d e: Bool]. It is only ever an element of a plist/tlist, never a p/t of its own.
• Only a telescope may contain general expressions, which is what makes [T: *] → T and Cn [mem: mem.M 0, I32] legal.
• [...] never binds for a body: a declaration or λ/cn/fn with a body must spell its domain as a (...) pattern, and writes an unnamed component as _: T. A bodyless extern declaration accepts either, since nothing binds there anyway.

A telescope name is visible only to what stands to its right - later components, and the codomain after a →. Cn X abbreviates X → ⊥ and so has no codomain at all, which makes every name in Cn [x y: I32] erased: it is the very same type as Cn [I32, I32].

A telescope is not a form of its own but the finite end of one construct. [...] is a sigma, and a sigma whose components are all the same is an array: [Nat, Nat, Nat] and «3; Nat» denote one and the same type. The same compression applies once more to a nest of arrays: «2; «3; T»» and «2, 3; T» denote one and the same type, and an array carries all of its axes as one shape. # follows suit - t#i#j and t#(i, j) are the same Extract - so an index has exactly as many components as the shape it indexes into. The sole exception is a mutable sigma of one component. A sigma names a component so that later components may depend on it; an array names its index so that the element type may depend on that. «i: n; T i» is therefore the very same dependency, taken over an arity that need not be a literal.

The term level mirrors the type level: (...) is a tuple, ‹n; e› a pack, and a tuple of n equal elements is that pack - (0, 0, 0) and ‹3; 0› are the same value, while (23, 42, 66) stays a tuple. # extracts from all four alike. Hence [n: Nat, «n; T»] describes a function whose number of arguments is a runtime value - a telescope of its own could never spell that, since it fixes its length syntactically.

An alias pattern wraps another pattern and additionally binds the whole value:

let (a, b, c) as abc = (1, 2, 3);

This binds a, b, and c to the tuple elements and abc to the whole tuple.

let and ret allow rebinding of an existing name, which is especially useful for state-threading style code:

let (m, ptr) = mem.alloc (I32, 0) m;
let m        = mem.store (m, ptr, 23I32);
let (m, val) = mem.load (m, ptr);

Expressions

Kinds and Builtin Types

e     ::= "Level"
       |  "Type" e
       |  "*"
       |  "□"
       |  "Nat"
       |  "Idx"
       |  "Rule" e
       |  alias
 
alias ::= "Bool"
       |  "I1" | "I8" | "I16" | "I32" | "I64"
       |  "i1" | "i8" | "i16" | "i32" | "i64"

• Level is the type of universe levels.
• Type e is the type at level e.
• * abbreviates Type (0:Level).
• □ abbreviates Type (1:Level).
• Nat is the natural number type.
• Idx is the builtin of type Nat → *.
• Rule e is the type of rewrite rules over the meta type e.
• alias is one of the predefined aliases, so Bool abbreviates Idx i1 and I32 abbreviates Idx i32.

Literals and Basic Forms

e   ::= sign? L (":" e)?
     |  sign? X_n
     |  "ff"
     |  "tt"
     |  C
     |  S
     |  "⊥" (":" e)?
     |  "⊤" (":" e)?
     |  path
     |  d+ e

• A numeric, character, string, ⊥, or ⊤ literal may carry an explicit type ascription.
• A +/- sign is part of the literal expression, not of the literal token, and only a numeric literal accepts one. Because + and - are infix operators everywhere else, f -23 subtracts; pass a negative argument as f (-23).
• Without an explicit type, numeric literals default to Nat.
• Without an explicit type, ⊥ and ⊤ default to *.
• d+ e is a declaration expression: one or more declarations followed by a final expression e, which is the result. It is not delimited by any brackets; it simply starts with a declaration keyword such as let.

Functions and Continuations

e   ::= e "→" e
     |  t "→" e
     |  "{" tlist? "}" "→" e
     |  "Cn" t
     |  "Fn" t "→" e
     |  "λ" p+ (":" e)? "=" e
     |  "cn" p+ (":" e)? "=" e
     |  "fn" p+ (":" e)? "=" e
     |  e e
     |  e "@" e
     |  "ret" p "=" e "$" e ";" e

• e → e is the ordinary arrow type.
• t → e, Cn t, and Fn t → e are dependent function forms whose domain is described by a telescope.
• λ, cn, and fn are the expression forms corresponding to lam, con, and fun. They are anonymous, so they cannot call themselves; use a lam/con/fun declaration to recurse.
• Application is written by juxtaposition.
• {...} declares implicit domains: an application inserts a Hole for each, and e @ e passes one explicitly.
• e @ e passes an explicit implicit argument.
• ret p = callee $ arg; body binds the result of a continuation-style call and continues with body.

Products

e     ::= "[" tlist? "]"
       |  "(" (e ("," e)*)? ")"
       |  "«" shape ";" e "»"
       |  "‹" shape ";" e "›"
       |  e "#" e
       |  e "#" I
       |  e ("#" e)+ "←" e
 
shape ::= arity ("," arity)*
arity ::= e
       |  I ":" e

• [ ... ] is a sigma expression unless it is immediately followed by as or →, in which case it is parsed as the domain of a dependent function type.
• ( ... ) is a tuple expression.

  Note

  There are no parenthesized/grouping expressions in Mim. Instead, you use a 1-tuple. A 1-tuple always degrades to its sole element, giving the effect of a parenthesized expression.

• « ... ; ... » builds an array.
• ‹ ... ; ... › builds a pack. Without the ; both are a singleton instead.
• A shape lists one or more comma-separated dimensions, as in «i: m, j: n; body», and each dimension may optionally be named. All of them fuse into one array of shape (m, n), whose index binds every axis at once, so t#i#j and t#(i, j) are the same Extract - except through a mutable sigma of one component. The exception is a dimension whose extent depends on an earlier index, as in «i: n, j: s#i; body»: a shape lists extents, not functions of preceding indices, so such a nest stays one array per axis.
• e#e extracts a component by index, e#I by field name.
• tuple#index ← value yields a new aggregate with index replaced by value; it does not mutate tuple. A # on the left is mandatory: without a component to update there is nothing to insert into.
• ← updates the component at the whole #-path, so t#i#j#k ← v denotes the outer aggregate t. The path extends leftward through # and stops at the first expression that is not itself a #.
  • ( ... ) builds a tuple (see above), so it ends a path. Thus, (t#i)#j ← v denotes t#i instead.
  • A let ends a path the same way: let row = t#i; row#j ← v also denotes t#i.
  • ← binds weaker than application, so f t#i ← v is (f t#i) ← v - write f (t#i ← v).

Dependent Tuple Types

A sigma is a dependent tuple type as soon as one of its components mentions a name to its left:

let sigma = [n: Nat, «n; Nat»];

The components refer to that name through a var of the sigma itself, so such a sigma is a mutable: it is built empty and filled in afterwards. Where no component uses that var, the sigma is the structural one after all - [i: Nat, j: Nat] is the very same type as «2; Nat».

A rec declaration additionally puts the declared name in scope inside the body, which is the only way for a type to mention itself:

rec Node = [val: I32, next: mem.Ptr0 Node];

rec also keeps the sigma mutable unconditionally.

Note

"mutable" says how such a sigma is constructed, not that anything about it may be changed later. A mutable is not hash-consed, so every occurrence is a node of its own, but it is still checked structurally: a second declaration of the same layout is alpha-equivalent to the first, and the two are interchangeable.

A mutable sigma of exactly one component stays a genuine 1-tuple; only rec builds one, since a lone component has nothing to its left to depend on. Everywhere else a one-element aggregate degrades to its sole element - [T] and «1; T» are T, and (x) is x - which makes #0₁ a no-op. Here it is a real Extract, and that is the one exception to t#i#j ≡ t#(i, j): a fused index folds its size-1 axes away, while the #-chain keeps them.

rec One = [x: Nat];
lam f (t: «2; One»): Nat = t#1₂#0₁;    // a real Extract: reads `x` out of the 1-tuple
lam g (t: «2; One»): One = t#(1₂, 0₁); // the `0₁` axis folds away, so this is just `t#1₂`

← is unaffected: writing the component rebuilds the whole 1-tuple either way, so t#(1₂, 0₁) ← v and t#1₂#0₁ ← v do agree.

Unions

e   ::= e "∪" e
     |  e "inj" e
     |  "match" e "with" "|"? arm ("|" arm)*
arm ::= p "=>" e
     |  (I | L) p? "=>" e

• e ∪ e forms a union type.
• e inj e injects a value into a union type.
• match e with | p => e | ... eliminates a union value.

Variants

e   ::= "|" (I (":" e)? ("|" I (":" e)?)*)?

• | I₀: e₀ | ... | Iₙ₋₁: eₙ₋₁ forms a variant type: a sum whose cases are positional. A constructor without : e carries [], and a lone | is the empty variant.
• Unlike ∪, nothing is sorted, deduplicated, or flattened: | A | B | C has three cases where [] ∪ [] ∪ [] is just [], and | A: Nat | B: Nat keeps both.
• A variant is a type like any other and may be anonymous; rec makes it recursive, and a mutual block mutually recursive.
• Its last payload extends as far right as it can, and | never starts an application argument: write f (| A | B), and parenthesize a variant inside a match arm.
• T#I or T#n on a variant type T selects a case by constructor name or by index, counting from 0. That is a value for a [] payload, and a function from the payload into T otherwise.
• Like an application, # first fills the implicit domains of its left-hand side with holes, so for nom Opt {T: *} = | None | Some: T, Opt#Some 23 infers T.
• In a match on a variant, each arm names a constructor or gives its index, optionally followed by a pattern for its payload. | 1 (h, t) => e selects the same case as | Cons (h, t) => e, just as T#1 and T#Cons do. Every constructor needs an arm; a second arm for the same one is unreachable and warned about.
• Constructor names are looked up in the scrutinee's type, so any scrutinee works, not just an annotated variable. Variants are structural, so two of the same shape are the same type; where they put a name at different positions, it is ambiguous and needs an index. A name reaches only the type it was declared on, so an instance of a polymorphic variant such as V T carries none and its cases are selected by index.

rec List = | Nil | Cons: [Nat, List];
 
lam len (l: List): Nat =
    match l with
        | Nil         => 0
        | Cons (_, t) => core.nat.add (1, len t);
 
let xs = List#Cons (1, List#Nil);
let ys = List#1 (2, xs); // the same constructor, by index

Singletons

e   ::= "«" e "»"
     |  "‹" e "›"
     |  "#" e

• « e » is the singleton type whose sole inhabitant is e. It sits one level above e, so «23» is a type and «Nat» a kind; «Level» does not exist.
• ‹ e › introduces a value of that type and the prefix # eliminates it again, so #‹e› is e.
• # recovers the inhabitant from the type alone: #x is e for every x: «e».
• The ; is what tells an array or pack from a singleton - «n; T» is an array, «T» a singleton.
• Because # is also the Extract operator, it is a prefix only where an expression starts: f #x extracts rather than applies, so pass a singleton as f (#x).

Nominal Newtypes

A nom declaration is the one place where Mim is not structurally typed: two noms over the same underlying type are still distinct types.

• nom I = e declares I as a fresh type that wraps e; it is the declaration - not the shape of e - that tells two noms apart.
• If e is a sigma, a variant, or a function type, I is already in scope inside e, so such a nom may be recursive, and a mutual block makes a group of them mutually recursive.
• anx nom additionally makes I an annex.
• nom I ndom+ = e declares a type constructor; it is sugar for lam I ndom+ = nom I = e; I. Each instance is a nom of its own, and within e, I names the type constructor, so a recursive instance refers to itself as I ndom+.
• e inj I wraps a value of the underlying type into I, and the prefix # unwraps it again, so #(e inj I) is e. Like I#C, e inj I fills the implicit domains of a type constructor I with holes.
• The named constructors of a nom over a variant - I#C and a match arm | C x - and the field names of a nom over a sigma - x#f and x#f ← v - unwrap and, for an update, rewrap the nom by themselves; access by index still needs #.
• inj, #, and the named constructors and fields are as visible as the nom itself: a pub or anx nom is transparent, while a priv one confines them to the mod that declares it - or its file, outside of any mod. A nom declared within a body takes the visibility of the enclosing top-level declaration.
• The type crosses a module boundary like any other value, so pub let I = I; exports a priv nom as an abstract type: an importer may name it but has to go through whatever the declaring module exports to build or inspect a value of it.

nom Meter = I32;
nom Foot  = I32;
 
lam to_foot (m: Meter): Foot = #m inj Foot; // Meter and Foot do not unify
 
mod units
    nom Kelvin = Nat;
    pub let Kelvin = Kelvin;                   // abstract outside of `units`
    pub lam kelvin (n: Nat): Kelvin = n inj Kelvin;
end
 
nom List = | Nil | Cons: [I32, List];
 
nom Tree (T: *) = | Leaf | Node: [Tree T, T, Tree T]; // `Tree Nat` and `Tree Bool` are distinct `nom`s

Note

A --output-mim dump flattens a program into one file, so a wrapping that an inliner carried across a module boundary lands in a dump that no longer re-parses.

Infix Operators

e   ::= e "==" e
     |  e "!=" e
     |  e "<" e
     |  e "<=" e
     |  e ">" e
     |  e ">=" e
     |  e "<<" e
     |  e ">>" e
     |  e "+" e
     |  e "-" e
     |  e "*" e
     |  e "/" e
     |  e "%" e

• a op b is sugar for `op (a, b) , so a + b is `+ (a, b) .

• Mim doesn't give the operators a meaning of their own; whatever `op is bound to is what they mean:

  plugin core;
   
  let `+ = core.nat.add;
  let x = 2 + 3;
• * doubles as the multiplication operator, so f * is a multiplication and not an application of f to Type (0:Level); write f (*) for the latter.

Local Declaration Blocks

e   ::= e "where" d* "end"

where attaches a local declaration block to an already parsed expression. where blocks bind more weakly than the other infix expression forms.

Precedence

Parser and dumper share one ladder of precedence levels, listed here from strongest to weakest binding. Assoc is left-, right-, or non-associative; chaining a non-associative operator, as in a == b == c, is an error - parenthesize one side. Pi, Bot, and Err are pseudo levels: they name no syntax at all and only ever bound how far a nested expression may extend. A +/- sign is part of the literal rather than an operator and so has no level of its own.

#	Level	Assoc	Operators	Notes
1	Lit	-	L:e	The tightest level. Not an infix operator - the literal parser reads the ascription itself and bounds e here.
2	Extract	left	e#e, e#I
3	App	left	e e, e @ e	Application binds tighter than every operator. Also bounds the e in Type e and Rule e.
4	Prefix	-	#e	The only prefix level. Looser than application, so #f x is #(f x).
5	Shift	left	e << e, e >> e	Tighter than *, as in Lean and OCaml - not the C position.
6	Mul	left	e * e, e / e, e % e
7	Add	left	e + e, e - e
8	Rel	none	e < e, e <= e, e > e, e >= e
9	Eq	none	e == e, e != e
10	Pi	-	pseudo	Bounds the domain of a λ/Fn/t → e binder so it stops before the →. A Cn-style binder has no → and uses Bot instead.
11	Arrow	right	e → e	Also bounds the codomain after a →.
12	Union	left	e ∪ e
13	Inj	right	e inj e	Weaker than ∪, so x inj A ∪ B is x inj (A ∪ B).
14	Ins	right	e("#"e)+ ← e	Also bounds a declaration's : codom slot, which ends at = and so takes everything short of a where.
15	Where	left	e where d* end	The loosest surface operator.
16	Bot	-	pseudo	A complete expression; the default bound, and the only one a trailing where fits into.
17	Err	-	pseudo	Below everything; the parser's "no operator seen yet" sentinel.

Summary: Functions and Types

Mim uses different surface syntax for declarations, expressions, and types:

Declaration	Expression	Type
lam	λ / lm	→
con	cn	Cn
fun	fn	Fn

Declarations

The following declarations are equivalent:

lam f1 (T: *) ((x y: T), return: T → ⊥)@ff: ⊥ = return x;
con f2 (T: *) ((x y: T), return: Cn T)        = return x;
fun f3 (T: *)  (x y: T): T                    = return x;

A partial-evaluation filter defaults to tt, except on the last domain of a con, cn, fun, or fn, where it defaults to ff.

Expressions

The following expressions are equivalent. Because they are bound by let, they behave like the declarations above - except that f is not in scope inside the body, so they cannot recurse:

let f1 =  λ (T: *) ((x y: T), return: T → ⊥)@ff: ⊥ = return x;
let _  = lm (T: *) ((x y: T), return: T → ⊥)@ff: ⊥ = return x;
let f2 = cn (T: *) ((x y: T), return: Cn T)        = return x;
let f3 = fn (T: *)  (x y: T): T                    = return x;

Applications

The following applications of f are equivalent, where g is a continuation that consumes the result:

fun f (T: *)  (x y: T): T = return x;
 
fun test1 (): Nat =
    f Nat ((23, 42), cn res: Nat = return res);
 
fun test2 (): Nat =
    ret res = f Nat $ (23, 42);
    return res;

Function Types

The following types are equivalent and describe the type of f above:

let _ = [T: *] →    [[T, T], T → ⊥] → ⊥;
let _ = [T: *] → Cn [[T, T], Cn T];
let _ = [T: *] → Fn  [T, T] → T;

Scoping

Mim uses lexical scoping. Unless noted otherwise, all names live in the same scope. A file is bound in isolation: it never sees the scope of whoever imports it.

Underscore

The symbol _ is special: it never binds an entity. As a consequence, _ may appear repeatedly in the same scope without conflict, but any use of _ as a reference is a scoping error.

Annex

An anx declaration is an ordinary member of its enclosing module, found by the same path resolution as any other member. Its plugin-qualified name (plugin.tag or plugin.tag.sub, derived from mod nesting) is additionally registered in a global by-name table (mim::Annex) that tools such as compile.named and plugin bootstrap use to look an annex up directly by that name, independent of the surrounding modules.

Field Names of Sigmas

Named components of a sigma are available for extracts and inserts. A structural sigma keeps no names in the IR, so the frontend records them per shape: once [i: Nat, j: Nat] is declared, every «2; Nat» answers to i and j. A name that another sigma of the same shape puts at a different position is ambiguous there; select the component by index instead. A mutable sigma is a node of its own, so its names are never ambiguous.

Note

These names take precedence over ordinary lexical names. In the example below, i refers to the field name of S, not the let-bound variable:

let i = 1₂;
rec S = [i j: Nat];
lam f (x: S): Nat = x#i;

Use parentheses to force the variable interpretation:

let i = 1₂;
rec S = [i j: Nat];
lam f (x: S): Nat = x#(i);

The constructor names of a variant behave the same way after #, as in T#Red.

Normalizations

Mim nodes are hash-consed and normalized while they are built, so the left-hand sides below never reach the IR - mim --output-mim prints the right-hand side. Every argument is zonked first, so a resolved Hole normalizes like the term it stands for. A mutable node is built empty and filled in afterwards and is therefore never normalized; only its body is. While the World is frozen, a rule that would have to build a new node bails out instead.

Aggregates

• (e) -> e, [T] -> T - a one-element aggregate degrades to its element; the sole exception is a mutable sigma of one component
• (e, e, e) -> ‹3; e›, [T, T, T] -> «3; T» - uniform elements compress into a pack/array
• (t#0, t#1, t#2) -> t - η for tuples, provided t has the ascribed type
• ⊥:[T, U] -> (⊥:T, ⊥:U), ⊥:«n; T» -> ‹n; ⊥:T› - ⊥/⊤ are pushed into aggregates
• ‹i: 3; e› -> (e[i ↦ 0₃], e[i ↦ 1₃], e[i ↦ 2₃]) - only for a literal arity below --scalarize-threshold and a body that depends on i

Shapes

• «1; T» -> T - a literal size-1 axis folds out of a shape
• «2, 0, 3; T» -> «2; []» - a literal 0 extent empties everything below it
• «a; «b; T»» -> «a, b; T» - a nest of the same kind fuses into one shape, unless the inner extents depend on the outer index

Extract

• d#(i, 0₁, k) -> d#(i, k) - a literal size-1 axis folds out of an index, mirroring the shape rule
• d#i -> d if i: Idx 1 and d's type is not a mutable sigma of one component
• d#() -> d - an index that folded away entirely
• ‹i: n; e›#j -> [i ↦ j]e for a pack that is not expanded into a tuple (see Aggregates), (a, b, c)#1 -> b
• t#i#j -> t#(i, j) - the maximal-rank fused Extract is the normal form, as far as t's own shape reaches
• t#(i, j) -> t#i#j - conversely, for an index reaching past t's own shape into its element type
• (d#i ← v)#i -> v
• (d#j ← v)#i -> d#i for literal i ≠ j

Insert

• d#() ← v -> v, and likewise for an index of Idx 1 - the write replaces all of d
• (a, b, c)#1 ← x -> (a, x, c)
• ‹4; x›#2 ← y -> (x, x, y, x) - only for a literal arity below --scalarize-threshold
• d#(i, j) ← v -> d#i ← ((d#i)#j ← v) - if the outer write rebuilds an aggregate by the two rules above, or if the index reaches past d's own shape
• d#i ← ((d#i)#j ← v) -> d#(i, j) ← v - otherwise, the dual of Extract fusion: a read-modify-write chain stays a single write
• d#i ← d#i -> d
• (d#i ← y)#i ← v -> d#i ← v

Application

• (λ (_: T) = e) a -> e - an immutable λ binds no var, so it always β-reduces
• f x -> body of f if x is f's own var - substituting a var by itself is the identity
• f x -> [var ↦ x]body of f if f's filter evaluates to tt for x; nothing is reduced if the filter is ff
• an application of an axiom runs its normalizer once the curry counter hits 0
• an application of a {T: *} → e inserts a Hole per implicit argument

Unions

• T ∪ ⊥ -> T - the unit of a join is dropped
• T ∪ ⊤ -> ⊤
• A ∪ A -> A; the operands are flattened and sorted, so ∪ is commutative, associative, and idempotent
• an empty join is ⊥, and a one-element one is its operand
• x inj T -> x if T is not a union type
• match (T inj x) with ... -> the arm handling T - a constructor fixes the active case
• each case is handled by the first arm accepting it, so the arms are not sorted; an arm accepts a case if its domain is that case, or a union containing it
• a match whose scrutinee is not a union is the degenerate one-case union and reduces right away
• an arm handling no case is dropped; a case handled by no arm is an error

Variants

• a variant is never sorted, deduplicated, or flattened; an empty or one-case variant stays a variant
• match (T#i x) with ... -> the arm for case i
• the arms of a match on a variant are in the order of its cases, one each

Singletons

• #x -> e for every x: «e» - the inhabitant is read off the type, so the var of a λ (x: «e») never occurs in the body
• #‹e› -> e - a special case of the above; a singleton elimination is therefore never built

Nominal Newtypes

• #(e inj T) -> e; on an opaque value the unwrapping stays

Universes

• Type levels: l + 1 folds for a literal l, nested successors add up, and a successor distributes over an LMax
• an LMax flattens nested maxima, folds their literals into one (dropping 0), sorts and deduplicates the rest, and collapses to its sole operand
• inference: x + k = l solves x = l - k, and max(xs, c) = l solves the xs right away if l = 0 or a single x must reach l; any other such constraint is postponed to the end of the enclosing declaration, where its still unknown levels default to 0
• an untyped binder used as a type, as A in lam f (A) (B: *): * = [A, B], gets the sort Type l for a fresh level l
• the var of a mutable whose var type is Idx 1 -> 0₁, and one whose var type is [] -> ()

Previous	Next
Command-Line Reference	Contributing & Debugging