An implementation of the type inferer can be found on GitHub. We have also provided a playground that infers and checks FT programs.
The FT calculus
David Pearce's 2012 paper Sound and Complete Flow Typing with Unions, Intersections and Negations develops a subtyping operator for a simple FT (flow typing) calculus, consisting of the proper types
$\any$ is the top type, $\never$ is the bottom type, $\int$ is the type of integers, and $\left(\T_1, \ldots, \T_n\right)$ is a tuple type. $\lnot\T$ is a negation type, inhabited by all values in the universe not inhabited in $\T$. $\T_1 \land \ldots \land \T_n$ is an intersection type, inhabited by values of type $\T_1$ and $\T_2$ and $\ldots$ and $\T_n$. $\T_1 \lor \ldots \lor \T_n$ is a union type, inhabited by values of type $\T_1$ or $\T_2$ or $\ldots$ or $\T_n$.
The syntax of FT is defined on page 4 of Pearce's paper, and restated belowOur syntactic specification differs mildly from Pearce's in that we permit declarations with multiple formals and use a post-fix type annotation syntax.:
All types except $\never$ and $\lnot \T$ are typable by the user; the latter two are generated during flow typechecking. The flow typechecker narrows variable types at checked sites; the $\tt if\ x\ is\ \T$ construct above, for example, narrows $x$ to $\T$ in the $\tt then$ branch, and to "everything except $\T$", $\typeof\ x\ \land\ \lnot\T$, in the $\tt else$ branch. Another unique feature of the flow typechecker is that applications are checked by inlining argument types into a function body and then checking that body, rather than computing a universal return type once.
As a larger example, consider the FT program
fn f(x: any) = if x is int|(int, int) then 9 else x in (f 1, f (1, 2, 3))
First we check the declaration f
, where x
will be typed as $\int\lor(\int,\int)$ in the then
branch, and $\any\land\lnot(\int\lor(\int,\int))$ in the
the else
branch. When checking the application f 1
, we
first check if $\typeof\ \mathtt{1}$ is a subtype of $\any$ (using a subtyping operator $\st$, described below), then check the body
of f
with $x\co\typeof\ \mathtt{1}$ to determine the resulting type of the
application. At the conditional, we check if $\typeof\ x$ is a subtype of
$\int\lor(\int,\int)$. According to the result, we update the environment and check the appropriate branch.
Pearce's subtyping algorithm
The crucial contribution of Pearce's paper is the construction of a subtyping operator we will call $\st$, under which all of the following hold:
Designing $\st$ to be soundSoundness means no term is illegally subtyped: $\T_1\st\T_2\implies\forall x\co\T_1, x\co\T_2$. and completeCompleteness means the subtyping operator admits all subtypable terms: $\forall x\co\T_1, x\co\T_2\implies\T_1\st\T_2$. is not trivial, and Pearce's paper is a very well-written account of constructing a (semi-)practical$\st$ requires rewriting types to their Disjunctive Normal Form, which can require an exponential amount of time. This is catastrophic in the presence of large or nested tuples, whose DNF rewriting experiences a tremendous explosion in the number of steps. For example, our implementation has been unable to terminate normalization of $(((\int,\int)\land\lnot\int, (\int,\int)\land\lnot\int), ((\int,\int)\land\lnot\int, (\int,\int)\land\lnot\int))$ even after several minutes. Nevertheless, $\st$ is more than suitable for less pathological types. algorithm that is exactly so.
$\infer$: type inference for FT
In this cc, we will design a type inference algorithm $\infer$ that "fills in" omitted type annotations in an FT program. Rather than being a component of the typechecker, $\infer$ is an out-of-band tool that does its best to complete a FT program with annotations demanded by the syntax, which a developer may find cumbersome to write. Indeed, we will prove that $\infer$ is complete, being able to infer every typable FT program; sound, annotating only those programs that are typable; and minimal, always inferring the smallest legal type. In the most extreme case, like ML, $\infer$ can type a program with no annotations at all.
It is not necessary to understand the operation of $\st$However, we will again mention that Pearce's paper is a pleasant, worthwhile read. to understand our type inference algorithm, only to believe that
- $\st$ is sound and complete
- $\st$ induces a partial order over the universe of FT types
- the universe of FT types, partially ordered by $\st$, is a lattice
Preliminaries
$\Def$ Let $\FT$ be the set of all well-typed FT programs, adhering to the syntax and types stated by the definitions of $\T$ and $\tt t$.
$\Def$ Let $\T^\delta ::= ([\T\to\T^\delta]\T) ~+\!\!|~ \msf{infer}\ n $ denote a type shape that is either a type inference variable distinguished by an integer $n$, or a proper type form where references to proper types may be type shapes.
$\Def$ Let ${\tt t}^\delta ::= [t\to t^\delta, \T\rightarrow\T^\delta] {\tt t}$ denote the syntax of a FT term shape or program shape. In a ${\tt t}^\delta$, type annotations may be type shapes than proper typesIn practice, a parser can admit a term without type annotations entirely, inserting fresh inference variables as needed., and references to other terms maybe term shapes.
$\Def$ Let $\FTS$ be the set of all valid FT program shapes, adhering to the syntax ${\tt t}^\delta$. For simplicity of our conversation, we will demand also that $\FTS$ consists only of program shapes where all type annotations of form $\msf{infer}\ n$ are unique, and furthermore all function and formal names are uniqueFormalizing both these demands is cumbersome and not relevant to our discussion..
$\Def$ Let $\require{cancel}\xFT = \left\{\untypable\right\}$ be the singleton set, symbolically marking an program shape as untypable.
We can describe $\infer$ as a function $\require{cancel}\FTS\to\FT\sqcup\xFT$, yielding either a well-typed FT program or a marker that a program shape is untypableWe could have also defined $\infer$ as a partial function.. Let $\iota_\FT$ and $\iota_\xFT$ denote the canonical projections in the codomain of $\infer$.
Per the FT syntax, we see that type annotations need appear only the formal parameters of a function declaration; hence, formals are also the only place inference variables may appear in a program shape. Our conversation will assume that we are always discussing type annotations on formals.
Inferring single variables
As a first step in approaching this problem, we will examine the simple case of resolving a single inference variable in an otherwise completely-typed program.
$\Def$ Let $x$ be a formal with a inference variable annotation $\msf{infer}\ n$ in a program shape $\PS\in\FTS$. Then $x^?$ denotes the inference variable $\msf{infer}\ n$.
Since we are supposing that all formals and inference variables in program shapes are unique, $x^?$ is unique for the unique variable $x$.
$\Def$ Let $\infvars(\PS\in\FTS)$ denote the set of inference variables $\left\{x_1^?, \ldots, x_n^?\right\}$ attached to all formals $\left\{x_1,\ldots,x_n \right\}$ in $\PS$.
Now, we will describe an algorithm $\infer1\co (x\to\FTS)\to\FTS\sqcup\xFT$ that resolves a program shape $\FTS$ and an inference variable $x^?$ in it to a shape wherein $x^?$ is replaced with the minimal type among all types, if any, satisfying a set of constraints placed on the type of $x$. We recover these constraints from definitions and uses of $x$:
- A definition $x\leftarrow y$ demands $\typeof\ x \supt \typeof\ y$
- A use $y\leftarrow x$ demands $\typeof\ x \subt \typeof\ y$
Bounds
Definition/use constraints on a variable bound that variable's type, a notion we formalize in two definitions below.
$\text{Definition}(\LB).$ Define $\LB(x, \PS) := \left\{ \typeof\ s_1, \ldots, \typeof\ s_n \right\} \setminus \left\{\typeof\ x\right\}$ to be the set of lower bounds on $\typeof\ x$, recovered from all definitions $x\leftarrow s_1, \ldots, x\leftarrow s_n \in \PS$.
$\text{Definition}(\UB).$ Define $\UB(x, \PS) := \left\{ \typeof\ t_1, \ldots, \typeof\ t_n \right\} \setminus \left\{\typeof\ x\right\}$ to be the set of upper bounds on $\typeof\ x$, recovered from all uses $t_1\leftarrow x, \ldots, t_n\leftarrow x \in \PS$.
Solution sets
Upper and lower boundaries in the universe of types form a (possibly empty) region of types assignable to a constrained variable. We call this region the solution set of an inference variable.
$\Def$ $x^?$ is solvable in $\PS\in\FTS$ if $x^?\in\infvars(\PS)$ and $\LB(x, \PS)$, $\UB(x, \PS)$ both contain no inference variables.
When $x^?$ is solvable in $\PS$, $\LB(x,\PS)$ and $\UB(x,\PS)$ yield a set of proper types $\T$, for which $\st$ is well-defined.
$\Def$ When $x^?$ is solvable in $\PS$, define
to be the solution set of $x^?$.
$\text{Proposition 1}.$ Let $x_1^?$ be solvable in $\PS$. Then
-
If there exists a set of types $\T_1,\ldots,\T_n$ such that $[x_1^?\to\T_1,\ldots,x_n^?\to\T_n]\PS$ yields a well-typed program in $\FT$, $\forall\U\in\Sol(x_1,\PS)\quad [x_1^?\to\U,x_2^?\to\T_2,\ldots,x_n^?\to\T_n]\PS\in\FT$.
-
If $\Sol(x_1, \PS)=\emptyset$, $\nexists\T_1,\ldots,\T_n$ such that $[x_1^?\to\T_1,\ldots,x_n^?\to\T_n]\PS\in\FT$.
$\Pf$ The key is that $\T_1$ does not depend on $\T_2,\ldots,\T_n$.
-
The only typing rules the formal $x_1\co \T_1$ is involved with are subtyping checks at definitions and uses. At a definition $x_1\leftarrow y$ we demand $\T_1\supt \typeof\ y$; if $y=x_1$ this holds by reflexivity of $\st$, otherwise $\T_1\supt\typeof\ y$ for all $x_1\leftarrow y$ where $x\ne y$ implies $\forall\S\in\LB(x,P);\T_1\supt\S$. The argument for uses similarly demands $\forall\U\in\UB(x_1,P);\T_1\subt\U$. If there exist $\T_1,\ldots,\T_n$ such that $[x_1^?\to \T_1,\ldots,x_n^?\to\T_n]\PS\in\FT$, $\T_1$ need only satisfy the above conditions; all types in $\Sol(x, \PS)$ satisfy these conditions.
-
By 1, if there exist $\T_1,\ldots,\T_n$ such that $[x_1^?\to\T_1,\ldots,x_n^?\to\T_n]\PS\in\FT$, $\T_1\in\Sol(x_1,\PS)$.
Existence and construction of $\infer1$
Proposition 1 tells us that finding the solution set for a variable completely tells us whether that variable is typable, and gives us valid typings for it in the case that it is. We can now formally define what it means to infer the type of a variable, give conditions on the existence of an inferred type, and give a precise formula for inferring one variable in a program.
$\text{Definition}(\Minimal).$ When $x^?$ is solvable in $\PS$, define
to be the minimal inferred type of $x$ in $\PS$, when it exists.
$\text{Proposition 2}.$ When $\Sol(x, \PS)$ is non-empty, $\Minimal(x,\PS)$ exists and is given by
$\Pf$ First of all, the equality is correct as $\never$ is uninhabited. The case when $\LB(x,\PS)=\emptyset$ is trivial. For the other, let $\T\in\Sol(x,\PS)$. Then $\forall \S\in\LB(x,\PS) ;\T\supt\S$, so $\T\supt\bigvee\LB(x,\PS)$. Hence
both hold, so $\bigvee\LB(x,\PS)\in\Sol(x,\PS)$ and is its infimum under $\st$.
$\text{Corollary 1}.$ $\Minimal(x, \PS)$ exists iff $\never\vee\bigvee\LB(x,P)\st\bigwedge\UB(x,P)$.
$\text{Corollary 2}.$ When it exists, $\Minimal(x, \PS) = \never\vee\bigvee\LB(x,\PS)$.
$\text{Definition}(\infer1).$ When $x^?$ is solvable in $\PS$, define $\T_x = \never\vee\bigvee\LB(x,\PS)$ and
When $\infer1(x, \PS) = \iota_\FTS P^{\delta+x}$, we say that $P^{\delta+x}$ is $\PS$ inferred with $x\co \T_x$.
$\text{Lemma 1(Properties of $\infer1$)}.$ Let $x_1^?$ be solvable in $\PS$. Then
-
If $\exists \T_1, \ldots, \T_n$ such that $[x_1^?\to\T_1,\ldots,x_n^?\to\T_n]\PS\in\FT$, then $\infer1(x_1,\PS) = \iota_\FTS P^{\delta+x}$ and
- $[x_2^?\to\T_2,\ldots,x_n^?\to\T_n]P^{\delta+x}\in\FT$
- Taking $P^{\delta+x}$ as $\PS$ inferred with $x\co \T_x$, $\T_x\st\T_1$ for all satisfying sequences $\T_1,\ldots,\T_n$.
-
$\nexists \T_1, \ldots, \T_n$ such that $[x_1^?\to\T_1,\ldots,x_n^?\to\T_n]\PS\in\FT$, iff $\infer1(x_1,\PS) = \iota_\xFT\untypable$.
$\Pf$ By application of Proposition 1, 2, and Corollaries 1, 2.
Dealing with cycles
At this point, it may seem that $\infer1$ gives us a constructive, sound, and complete algorithm for inferring the minimal type of an inference variable in a program shape. Indeed, we may attempt write a complete $\infer$ algorithm the following way:
$\text{Definition($\infer$: No Cycles)}$
- $\text{Algorithm $\infer$($\PS$):}$
- $\qquad\text{if }\PS\in\FT$
- $\qquad\text{then return }\iota_\FT\PS$
- $\qquad\text{else}$
-
- $\qquad\qquad\text{if }ivars=\emptyset$
- $\qquad\qquad\text{then return }\iota_\xFT\untypable$
- $\qquad\qquad\text{else}$
- $\qquad\qquad\qquad x\leftarrow x\in ivars$
- $\qquad\qquad\qquad\text{if }\infer1(x,\PS) = \iota_\FTS(P^{\delta+x})$
- $\qquad\qquad\qquad\text{then }\text{Solve}(P^{\delta+x})$
- $\qquad\qquad\qquad\text{else return }\iota_\xFT\untypable$
The issue with this algorithm lies on lines 5 and 6: if we have a program shape with inference variables, none of which are solvable, we cannot progress. This means that while $\infer1$ is complete for solvable variables, this definition of $\infer$ is not complete for program shapes!
As an example of a program shape for which the definition above is incomplete, consider
fn f(x: infer 1) = x in fn g(y: infer 2) = f y in g (f 1)
we have that $\LB(x, \PS) = \left\{y^?,\int\right\}$ and $\LB(y, \PS) = \left\{x^?\right\}$, so no variable is solvable. But $[x^?\to\int, y^?\to\int]\PS$ yields the following well-typed program
fn f(x: int) = x in fn g(y: int) = f y in g (f 1)
Throughout the rest of this section, we describe how to resolve inference variables in the presence of cycles, and prove that our updated method is complete. Our roadmap will be to
- partition inference variables into strongly connected components
- prove that all inference variables in a strongly connected component have a single, unique minimal solution, if any
- show that potential solutions and verification of solutions can be done in two passes
- wrap everything up in a sound, complete, and minimal $\infer$ algorithm
Solution orders
$\Def$ Let $\PS\in\FTS$. The inference dependency graph $\IDG(\PS)$ of $\PS$ is a directed graph where
-
the vertices are the inference variables $\infvars(\PS)$
-
there is an edge $x^?\to y^?$ exactly when $x^?\in\LB(y, \PS)$
$\text{Definition($\SolOrder$)}.$ Let $\PS\in\FTS$. Let $S_1, \ldots, S_n$ denote the connected components of $\IDG(\PS)$, ordered arbitrarily. Let $C_{i1}, \ldots, C_{in_i}$ denote the strongly connected components of $\S_i$, ordered topologically under condensation.
Then the solution order $\SolOrder(\PS)$ is the strict preorder given by $C_{11} \lt \ldots \lt C_{1n_1}\ldots \lt C_{n1}\ldots \lt C_{nn_n}$.
$\text{Proposition 3}.$ For a given strongly connected component $C_{ij} \in \SolOrder(\PS)$, for any vertex $v\in C_{ij}$, there exists an edge $u\to v$ only if $u\in C_{i1} \lor \ldots \lor u\in C_{ij}$.
$\Pf$ The strongly connected components $C_{11},\ldots, C_{(i-1)n_{i-1}}, C_{(i+1)n_{i+1}},\ldots, C_{n n_n}$ cannot contain any vertices that have an edge to $v$ because they come from disjoint connected components in $\IDG(\PS)$.
For the other components, suppose by way of contradiction there is an edge $u\to v$ where $u\in C_{ik}, k > j$. Then since the condensation of $S_i$ is given by the graph $C_{i1}\to\ldots\to C_{ij}\to\ldots\to C_{ik}\to\ldots\to C_{in_i}$, there is a cycle $C_{ij}\to\ldots\to C_{ik}\to C_{ij}$. But then $C_{ij},\ldots,C_{ik}$ are not maximal, a contradiction.
For example, suppose we have a program shape with the following inference dependency graph:
then its connected components and their condensations are given by:
yielding the solution order $C_{11}\lt C_{12}\lt C_{21}$.
Solving for minimal types
$\Def$ Let $\TS$ be a type shape. The disjunctive normal form $\DNF(\TS)$ of $\TS$ is a type shape of form $\displaystyle\bigvee_i\bigwedge_j {\TS}^*_{i, j}$, where
and $\TS$ and $\DNF(\TS)$ are equivalent under $\st$.
An algorithmic account of $\DNF$ and proof of the properties we claim is given in Pearce's paper (Definition 6, Lemmas 4-6).
$\Def$ Let $\SolOrder(\PS) = C_{1}\lt\ldots\lt C_n$. Then $C_1$ is the first-solvable component of $\PS$.
$\text{Definition($\Reify$).}$ Let $C$ be the first-solvable component of $\PS$ and $x^?\in \vert(C)$. Then $\Reify$ is a function defined as
- $\text{Algorithm $\Reify$($x$, $\PS$):}$
- $\quad \text{Algorithm $\Step$($\TS$, $seen$): match $\DNF(\TS)$ with}$
- $\quad\quad \ldots\land\TS_i\land y^?\land\TS_j,\ldots \text{ if } y\notin seen\Ra \Step(\ldots\land\TS_i\land(\bigvee\LB(y, \PS))\land\TS_j\land\ldots,\;seen\cup\{y\})$
- $\quad\quad \ldots\land\TS_i\land y^?\land\TS_j,\ldots \text{ if } y\in seen\Ra \Step(\ldots\land\TS_i\land\TS_j\land\ldots,\;seen)$
- $\quad\quad \ldots\land\TS_i\land\ldots \text{ if } y^?\subset\TS_i\Ra\Step(\ldots\land[y^?\to\never]\TS_i\land\ldots,\;seen)$
- $\quad\quad \ldots\lor\TS_i\lor y^?\lor\TS_j,\ldots \text{ if } y\notin seen\Ra \Step(\ldots\lor\TS_i\lor(\bigvee\LB(y, \PS))\lor\TS_j\lor\ldots,\;seen\cup\{y\})$
- $\quad\quad \ldots\lor\TS_i\lor y^?\lor\TS_j,\ldots \text{ if } y\in seen\Ra \Step(\ldots\lor\TS_i\lor\TS_j\lor\ldots,\;seen)$
- $\quad\quad \ldots\lor\TS_i\lor\ldots \text{ if } \TS_i \supseteq \TS_j = (\US_1,\ldots,\US_n) \text{ and } y^?\subset\TS_j$
- $\quad\quad\quad\quad \Ra\Step(\ldots\lor[y^?\to\never]\TS_i\lor\ldots,\;seen)$
- $\quad\quad \ldots\lor\TS_i\lor\ldots \text{ if } y^?\subset\TS_i\Ra\Step(\ldots\lor[y^?\to\any]\TS_i\lor\ldots,\;seen)$
- $\quad\quad \text{else }\Ra\TS$
- $\quad \Step(\bigvee\LB(x,\PS), \left\{x\right\})$
where lines 3-5 match a intersection type being the singleton variant of the union form yielded by $\DNF$, matching of $y^?$ is variable in $y \in \infvars$. The abuse of notation $y^?\subset\TS$ means that $y^?$ appears in $\TS$, and $y^?\subseteq\TS$ means that $\TS=y^?$ or $y^?\subset\TS$, all under syntactic equality. Lastly, $\ldots\lor\T\lor\ldots$ should be considered a finite type; we omit terminal types for space.
$\text{Proposition 4.}$ $\Reify(x, \PS)$ terminates and yields a proper type for all suitable $x$ and $\PS$, as described in the definition.
$\Pf$ For termination, observe that $\Step(\TS,\ seen)$ recurses so long as there is an inference variable in $\TS$ matched by a rewrite rule, but each rule decreases the number of inference variables in the next iteration's type. The only exceptions are line 7 and 12, but those rules are reached at most once each for a finite number of inference variables. As for yielding a proper type, it is enough to see that all cases in which an inference variable can appear in a DNF-normalized type are covered by the left-hand sides of lines 7, 8, and 11; all other rules are special cases.
$\text{Lemma 2.}$ Let $C$ be the first-solvable component of $\PS$ and $x_1^?\in \vert(C)$. Let $\left\{x_1^?,\ldots,x_n^?\right\}=\infvars(\PS)$. If there exists a set of types $\T_1,\ldots,\T_n$ such that $[x_1^?\to\T_1,\ldots,x_n^?\to\T_n]\PS\in\FT$, then $[x_1^?\to\Reify(x,\PS),\ldots,x_n^?\to\T_n]\PS\in\FT$, and furthermore, $\Reify(x,\PS)\st\T_1$ among all such sets of types $\T_1,\ldots,\T_n$.
$\Pf$ As in Lemma 1 and its preliminaries, the minimal type (when it exists) of an inference variable $x^?$ is the union of its lower bounds. Line 14 of $\Reify$ computes this; it remains only to show that $\Step$ retains the minimality of a type in the FT calculus. Intuitively, the thing to keep in mind is that recursive unions "grow" a type and recursive intersections "shrink" a type. We will prove minimality by case analysis on lines 7-12; lines 3-5 are analogous special cases for when there are no unions in $\TS$.
-
Line 7: Since $y^?$ is a lower bound of $x$, inlining the lower bounds of $y$ does not change the resolved type of $x$.
-
Line 8: Having already inlined the lower bounds of a inference variable, inlining them again in the presence of a union would not modify the total type, as $\T\lor\ldots\lor\T\lor\ldots = \T\lor\ldots$.
-
Line 9: This is the case of a recursive tuple type, for example $x^? = \T_1\lor\ldots\lor\T_i\lor(\ldots,x^?,\ldots)\lor\T_j\lor\ldots\lor\T_n$. Clearly this is a type of infinite depth bounded by $\any$ at position $x$ when constructed positively; this yields the finitary type $\T_x = \T_1\lor\ldots\lor\T_i\lor(\ldots,\any,\ldots)\lor\T_j\lor\ldots\lor\T_n$. We need to show also that there is no bounding finitary type $\W$ at position $x$ consisting of negations ("approaching from the top"). By way of contradiction, suppose there is such a finitary type; since it is bounded above by $\any$, $\W$ is of the form $\any\land\lnot\S_1\land\ldots\land\lnot\S_n$. Either $\T_1\lor\ldots\lor\T_i\lor\T_j\lor\ldots\lor\T_n \supt \any$ or else $\S = \T_1\lor\ldots\lor\T_i\lor\T_j\lor\ldots\lor\T_n \subt \any$. In the former case $\W$ must resolve to $\any$. In the latter case each nested level of the recursive tuple in $x^?$ induces at least one additional negation in $\W$, so $\W$ must be infinite.
-
Line 11: This is like the case on line 9, but covers the remaining cases of recursive intersections and negations. The argument for intersections is similar to that of tuples above, except that a recursive intersection continuously constricts the total type, bounding it to $\never$. This is not the case for intersections that recurse flatly on themselves; for example, $\T = \T\land\int$ is bound by $\int$, not $\never$. However, $\DNF$ normalization of $\PS$ ensures that in the case on line 9, the recursion is not flat. Flat recursion of intersections is handled on line 4.
Recursive negations can be reduced to a special form of intersections, where the above argument then applies. The reduction is due to DeMorgan; $x^? = \lnot x^?\lor\T \implies x^? = \lnot (\lnot x^?\lor\T)\lor\T = (x^?\land\lnot\T)\lor\T$.
-
Line 12: Trivial, does not modify the type.
Thus, we have shown if there is any finitary type representing the minimal type of inference variable, $\Reify$ finds it.
Putting it all together
$\text{Definition($\infer$)}$ $\infer$ is a function $\FTS\to\FT\sqcup\xFT$, defined below.
- $\text{Algorithm Infer($\PS$):}$
- $\qquad P\leftarrow\PS$
- $\qquad \text{for $C$ in $\SolOrder(P)$}:$
- $\qquad\qquad \text{for $x^?$ in $\vert(C)$}:$
- $\qquad\qquad\qquad \T_x\leftarrow\Reify(x, \PS)$
- $\qquad\qquad\qquad P\leftarrow \left([x^?\to\T_x] P\right)$
- $\qquad \text{for $x^?$ in $\infvars(\PS)$}:$
- $\qquad\qquad \T_x\leftarrow \typeof\ x \text{ in } P$
- $\qquad\qquad \U\leftarrow\bigwedge\UB(x, P)$
- $\qquad\qquad \text{if } \T_x\not\lt:\U \text{ then return } \iota_\xFT\untypable$
- $\qquad \text {return } \iota_\FT P$
Lines 3-6 of the algorithm find potential solutions to the inference variables of $\PS$, and lines 7-10 verify those solutions by comparing them to the (now-resolved) upper bounds of corresponding variables. If verification succeeds, a well-typed program in $\FT$ is returned; otherwise we mark the program shape as uninferrable, and hence untypable.
Note that $\infer$ is well-defined; the only thing that may be of concern is the call to $\Reify(x,P)$, as $\Reify$ is only defined $x\in C$ where $C$ is first-solvable in $P$. But since reification is done in linear solution order $C_1,\ldots,C_n$, once all inference variables in $C_1$ are reified in $P$, $C_2$ becomes first-solvable in $P$.
$\text{Lemma 3(Soundness of $\infer$)}.$ If $\infer(\PS) = \iota_\FT P$, it is indeed the case that $P\in\FT$.
$\Pf$ By Lemma 2, lines 3-6 rewrite every inference variable $x^?$ with its minimal legal type $\T_x = \bigvee \LB(x, \PS)$, if one exists. The condition of existence is the same as that in Proposition 1 and Corollary 1; namely, $T_x \st \UB(x, P)$, which is verified for all possible solutions of inference variables on lines 7-10.
$\text{Lemma 4(Completeness of $\infer$)}.$ Let $\PS\in\FTS$ where $\infvars(\PS)=\left\{x_1^?,\ldots,x_n^?\right\}$. If there exists as set of proper types $\T_1,\ldots,\T_n$ such that $[x_1^?\to\T_1,\ldots,x_n^?\to\T_n]\PS \in \FT$, $\infer(\PS) = \iota_\FT P$.
$\Pf$ Corollary of Lemma 2.
$\text{Lemma 5(Minimalism of $\infer$)}.$ Let $\PS\in\FTS$ where $\infvars(\PS)=\left\{x_1^?,\ldots,x_n^?\right\}$ and $\infer(\PS) = \iota_\FT P$. Let $\T_1,\ldots,\T_n$ such that $[x_1^?\to\T_1,\ldots,x_n^?\to\T_n]\PS = P$. Then among all sets of types $\U_1,\ldots,\U_n$ such that $[x_1^?\to\U_1,\ldots,x_n^?\to\U_n]\PS\in\FT$, $\T_1\st\U_1,\ldots,\T_n\st\U_n$.
$\Pf$ Corollary of Lemma 2.
Conclusion
In this cc, we have presented a sound, complete, and minimal algorithm for type inference of mandatory type annotations in the flow-typing type calculus developed by Pearce, 2012. Our algorithm is constructive and syntax-directed, resolving inference variables from types demanded at definition sites and verifying the legality from types demanded at usage sites.
Our approach to type inference is similar to the classic methods (a la Algorithm W) - collect some constraints and perform unification. Our unification step is more appropriately called resolution, and is more involved than classical unification. In our case, the fact that the FT type universe forms a complete lattice is particularly important.
The finitary nature of the FT calculus complicates the resolution process in the presence of type variable cycles, as an inference variable can incur cyclic constraints that result in a type of infinite depth. Our approach resolves such types to their "closest" legal finitary type by translation to disjunctive normal form, a process that Pearce has noted is exponential in the depth of a type in the worst case (Pearce 2012, section 3.2), and then applying a rewrite procedure whose time and space complexities are linear in variables and type depths but whose rewrite rules are somewhat tricky. The addition of (mutually) recursive types to the FT calculus would trivialize the solution to this issue, though of course would come with its own set of challenges (e.g. type simplification and reformulating $\st$ to be sound and complete).
Takeaways
This is a small problem I toyed with for a couple days, and then took far longer to write up as in this cc. I think it is rather interesting, because type inference in the presence of subtyping is generally considered difficult (though that is usually because of record types and such, not present in FT), and because the FT calculus does not make resolution of certain issues trivial (e.g. cycles cannot be resolved as recursive types).
Designing a compiler with a type inferer out-of-band of the typechecker, as we did here, is also interesting. While the inferer will need to depend a lot on the checker, this decoupling means that multiple inferers for different purposes could be designed. Some ideas include:
- A sound, complete, and minimal inferer, like the one presented here
- An inferer that optimizes for readability of types, avoiding deep nesting
- An inferer that optimizes for a minimal number of unique types
- An inferer that solves for maximal types (principal types in functional languages)


{% extends "base.html" %}
{% block content %}
{% include "stock/loc_link.html" with location=None %}
{% if locations.all|length > 0 %}
Storage Locations
{% include "stock/location_list.html" with locations=locations %}
{% endif %}
{% if items|length > 0 %}
{% include "stock/stock_table.html" with items=items %}
{% endif %}


Isar735.github.io
How to Make Money From Home as a Studypool Tutor.
Connecting with an online tutor is easy and free. You just need a library card and a computer or mobile device with internet access. Help is available. Our Finance tutors help students online and in-person with finance homework and test prep. Let our online finance tutors help today. Online Tutoring State Certified Teachers Bilingual.  Homework Help Tutor — Homework Help Tutor. Better Grades Guaranteed. Enter your city or zip code in the creative writing major mcgill box to show results in your area. Please note that all salary figures. Algebra Help - Calculators, Lessons, and Worksheets. Exclusive homework help delivered by experienced professionals. Affordable and authentic custom written assignments designed for international students. Online Tutoring Jobs Become an online tutor with Tutor.com. Our tutors are teachers, professors, adjuncts, PhD students, and industry professionals
Apply to be a Tutor - Online Tutoring, Homework Careers for aspiring Professionals as Online Homework Assignment Help Jobs with Assignment Writing Jobs. Assignments Help Tutors - A leading global e-learning service. Study Skills - A Handout for Parents LD Topics LD OnLine. Get a tutor 24/7 in 40+ subjects including Math, Science and English. We help thousands of students get better grades every day. Get an expert tutor. Math homework help. Hotmath explains math textbook homework problems with step-by-step math answers for algebra, geometry, and calculus. Online tutoring available.
Free Online Tutoring Los Angeles Public Library. 91 Weekend Homework Help Tutor jobs available. See salaries, compare reviews, easily apply, and get hired. New Weekend Homework Help Tutor careers are added daily.
Aplusmath : Free Math Worksheets, Math Games Professional Homework Help for International Students. Study Skills - A Handout for Parents. Many capable children at all grade levels experience frustration and failure in school, not because they lack ability. Free math learning resources for teachers and students - including games, flashcards, homework helpers, and worksheets. K12 Math/English/Science, ACT, SAT, TOEFL Preparation. Watch French girl seduced by Spanish tutor on Pornhub.com, the best hardcore porn site. Pornhub is home to the widest selection of free Toys sex videos Get algebra help from Chegg now! algebra guided textbook solutions, expert answers, definitions Wyzant Resources features 193,000+ free resources created by the largest network of private tutors on the web. Explore and collaborate to start learning today.
Increase confidence motivation. as academic mentors, the influence of an alchemy tutor goes far beyond school work. every alchemy tutor is selected for their.
Math, Reading, Writing, Grammar, Vocabulary, K-12, SAT, ACT Tutoring Programs K-12 Math, English, Science Tutoring; SAT, PSAT, ACT Prep, College Admissions. 95 Homework Help Tutor jobs available in Westfield, NJ on Indeed.com. Apply to Tutor, Test Preparation Tutor, Executive Coach
3 Ways to Motivate Teenagers to Do Their Homework - wikiHow. Homework Help Tutor ― Homework Help Tutor. French Girl Seduced by Spanish Tutor - Pornhub.com. Get help from Chegg now! guided textbook solutions, expert answers, definitions This list of companies with online tutor jobs breaks down the tutoring jobs by subject matter, grade level, and type of position. Watch Homework Help porn videos for free, here on Pornhub.com. Discover the growing collection of high quality Most Relevant XXX movies and clips. No other
College homework help - High School College University. Online homework help for college students. Professional academic assignments writing editing proofreading. We provide best academic assistance on a huge variety.
Homework Help Tutor Jobs, Employment in Westfield Math Homework Help - Answers to Math Problems - Hotmath.
How to Motivate Teenagers to Do Their Homework. It is pretty common for teenagers to hate doing homework. They would much rather hang out with their friends 4 Ways to Get Your Kids to Do Their Homework - wikiHow. Page not found The official provider of online tutoring and homework help to the Department of Defense. Engage your community with learning and career. 20 Best Homework Help Tutor jobs (Hiring Now!) Simply Hired. 865 Homework Help Tutor jobs available. See salaries, compare reviews, easily apply, and get hired. New Homework Help Tutor careers are added daily on SimplyHired.com.
Become a Tutor Tutor Jobs at Course. Homework Help Porn Videos Pornhub.com. The official provider of online tutoring and homework help to the Department of Defense. Check Eligibility. Can I pay someone to take my online class for me? Yes, we’re a reliable class help provider connecting you with subject tutors to take your course and tests. You can make money from home as a Studypool tutor. Some tutors do this for extra cash, while others earn a full-time income tutoring Itutor is a leading platform for online tutoring, AP exams and Test Preparation.Join our online Tutoring jobs and help students online with homework and Tutor. Alchemy Tuition - English Tutoring and Maths Tutoring.
Online Homework Assignment Help and Writing. Algebra Help. This section is a collection of lessons, calculators, and worksheets created to assist students and teachers of algebra. Discover free educational resources Wyzant Resources.
Tutoring jobs - Become a private tutor - Superprof. How to Get Your Kids to Do Their Homework. Parents around the world would love the magic formula to encourage kids to do their homework. Alas, it's not as simple. America's #1 tutoring site - Earn $25+ / hour - No commission - Local and online tutor jobs - 1000's of students - Teach maths, English, music. Become a tutor on Course Hero. Find online tutoring jobs to empower our community! We're looking for tutors who are passionate about teaching and helping students learn.


Allstar Demo by Smash Mouth MIDI loop by antha
audio
Untitled DAW Tune antha having fun with a digital audio workstation
Thunderclouds Demo by LSD MIDI cover by antha
back


One place for all your websites!! Now browse the web with ease!!
© Kushagra Singh. All Rights Reserved.


Austin Hill
Austin's Project Portfolio
Austin Hill is a cool guy.
Projects
Herd
The Other Cool Project
Final Most Legit Of Projects
...


India's fiscal deficit touches Rs 7 trillion, surpasses annual target in seven months
India’s fiscal deficit in the first seven months through October stood at Rs 7.2 trillion, or 102.4 per cent of the budgeted target for the current fiscal year, government data showed on Friday.
HIGHLIGHTS
- India's fiscal deficit in the first seven months through October stood at Rs 7.2 trillion
- It is 102.4 per cent of the budgeted target for the entire current fiscal year
- Govt's revenue in this period was Rs 9.3 trillion and expenditure Rs 16.55 trillion
The government of India's fiscal deficit has surpassed the annual target within the first seven months of the current financial year. India’s fiscal deficit in the first seven months through October stood at Rs 7.2 trillion ($100.32 billion), or 102.4 per cent of the budgeted target for the current fiscal year, government data showed on Friday.
According to government data, the net tax receipts in the April-October period was Rs 6.83 trillion, while total expenditure was Rs 16.55 trillion.
The total revenue government received in the period was Rs 9,34,460 crore, which included Rs 6,83,486 crore in tax revenue, Rs 2,24,148 crore in non-tax revenue, Rs 26,826 crore in non-debt capital receipts.
Non-debt capital receipts also include Rs 9,461 crore worth of loan recovery.
Disinvestment proceeds have contributed Rs 17,365 crore to the final revenue figures.
Total expenditure incurred by the government of India in April-October 2019 period is Rs 16,54,905 crore, out of which Rs 14,53,632 crore is on Revenue Account and Rs 2,01,273 crore is on Capital Account.
Out of the total revenue expenditure, Rs 2,89,565 crore was on account of interest payments while Rs 2,26,724 crore was on account of major subsidies.
Rs 3,66,871 crore has been transferred to state governments as devolution of share of taxes by the Centre. It is Rs 10,205 crore lower than the previous year.


[Erowid Note: IV injection of crushed pills/tablets can be very dangerous due to unknown binders and fillers present in the tablets.]
My first experience with Elavil was with my boyfriend, who is a druggy major. We were hanging out at this one guys house and he said he could hook us up with some Elavils. My boyfriend and I had never heard of them before so we asked more. He told us that they were downers and that we should just try because he didn't know because he had never taken them before.
Now I don't have that much experience with drugs, just like zannies and oxys, and weed and coke. But I was like alright lets try this thing.  Then we heated them down put them in the needle and stuck it in and all.
Minutes later I felt the most tired I had ever been in my life. I could not keep my head up for the life of me. I slowly lost consiousness and fell into a deep sleep. Hours later I woke up and was feeling pretty good. But then I came down.  I don't like Elavil, it's just a major downer and don't waste your money on it.
Experience Reports are the writings and opinions of the individual authors who submit them.
Some of the activities described are dangerous and/or illegal and none are recommended by Erowid.


Survey Questions
Name (required)
Link to Your Photo (required)
Question 1
You believe that you were going to be harmed or harassed by an individual, group or organization, even in the absence of concrete evidence?
--Selected an Option--
1: Strongly Disagree
2: Slightly Disagree
3: Neither Confirm or Deny
4: Slightly Agree
5: Strongly Agree
Question 2
You feel as if strangers were watching you or talking about you?
--Selected an Option--
1: Strongly Disagree
2: Slightly Disagree
3: Neither Confirm or Deny
4: Slightly Agree
5: Strongly Agree
Question 3
You believe that ambiguous environmental cues, gestures or symbols are directed at you?
--Selected an Option--
1: Strongly Disagree
2: Slightly Disagree
3: Neither Confirm or Deny
4: Slightly Agree
5: Strongly Agree
Question 4
You believe that you have exceptional abilities or that you’re destined for wealth or fame?
--Selected an Option--
1: Strongly Disagree
2: Slightly Disagree
3: Neither Confirm or Deny
4: Slightly Agree
5: Strongly Agree
Question 5
You feel that you don’t have control of your mind or body?
--Selected an Option--
1: Strongly Disagree
2: Slightly Disagree
3: Neither Confirm or Deny
4: Slightly Agree
5: Strongly Agree
Question 6
You sometimes see things that other people couldn’t?
--Selected an Option--
1: Strongly Disagree
2: Slightly Disagree
3: Neither Confirm or Deny
4: Slightly Agree
5: Strongly Agree
Question 7
When you're alone, do you ever hear voices that don’t have an explainable source?
--Selected an Option--
1: Strongly Disagree
2: Slightly Disagree
3: Neither Confirm or Deny
4: Slightly Agree
5: Strongly Agree
Question 8
You have trouble staying on topic during conversations, often rambling or losing track of your original train of thought?
--Selected an Option--
1: Strongly Disagree
2: Slightly Disagree
3: Neither Confirm or Deny
4: Slightly Agree
5: Strongly Agree
Question 9
You have had an experience with the supernatural, including fortune telling, telepathy or other psychic forces?
--Selected an Option--
1: Strongly Disagree
2: Slightly Disagree
3: Neither Confirm or Deny
4: Slightly Agree
5: Strongly Agree
Question 10
You often feel suspicious of people around you or find it difficult to trust others?
--Selected an Option--
1: Strongly Disagree
2: Slightly Disagree
3: Neither Confirm or Deny
4: Slightly Agree
5: Strongly Agree
Question 11
You feel that you don’t have control of your thoughts or ideas?
--Selected an Option--
1: Strongly Disagree
2: Slightly Disagree
3: Neither Confirm or Deny
4: Slightly Agree
5: Strongly Agree
Question 12
Have you lost interest in activities that you used to enjoy or find it difficult to experience happiness or pleasure in general?
--Selected an Option--
1: Strongly Disagree
2: Slightly Disagree
3: Neither Confirm or Deny
4: Slightly Agree
5: Strongly Agree


We studied Formal Grammars in some of the previous articles in this course, What is a Grammar in programming languages and How to design formal Grammars. The most important concepts we learned are:
- There are 4 types of Grammar in the Chomsky hierarchy.
- Type-2 Grammars, also said Context-Free Grammars, are the ones used to design new programming languages.
- One must avoid many pitfalls while creating a new Grammar, for example left-recursion and ambiguity.
In this article we will take all those concepts and put them into practice: I will show how I designed a new Context-Free Grammar. This Grammar is the basis of the new Programming Language I created as a learning tool for this course.
Preliminaries
The first baby-step in the design of a Formal Grammar is to decide on the Alphabet, and the set of characters allowed. If such terminology sounds a bit confusing, I can’t help but suggest you to read a bit via Wikipedia, or the previous articles in this course (see the references at the end).
Now, one thing I always had as objective while working on the design part was the simplicity of the programming language. I wanted to create a very direct programming language, almost “explicit” if you will, and without overloading it with fancy statements or complex expressions. This has been the main guideline during the whole process.
Also, to start off, I decided to focus on a small set of instructions. That means the initial version of the language (that’s what I will show in this article) does not allow for OOP, routines, coroutines, etc.. Of course, I understand that routines are an extremely important part of a language, and I will definitely add them at a later stage.
Also, I wanted the language to be explicit but not too verbose. Therefore I decided to make it non-explicitly typed. So, for example, you wouldn’t write int x = 5
, you would just write x = 5
.
However, I do want the language to be aware of types, also at compilation time, therefore it will be a language with static and implicit typing system. Based on that, the compiler will also check for typing-errors, such as adding a string to an integer (more on this in a future article).
At the theoretical level, I wanted to design a LL(1) grammar, so that I can also write my own implementation of a LL(1) recursive descent parser.
If you need to check what these naming conventions mean, start from my previous article What are the differences between programming languages, or google them!
Wherever possible, I tried to add some small nuances into the formal grammar, to give a personal touch to the whole. Having fun was one of the goals too!
Characters, Numbers and Strings
To start with, I knew I would need all basic blocks such as digits and letters in the Alphabet. Thus, I defined the following regular expressions as part of the Grammar.
digit0 : 0-9
digit : 1-9
letter : a-z | A-Z
otherChar : |!”%&/()=+-*#><;,^.][\n \t
char : letter | otherChar | digit
Let’s take a moment and think, because the choices I made have already some implications. First of all, the distinction between all digits, and the subset of them without the zero, is a bit redundant, but I found it useful (as I will tell you later).
In second place, the underscore (_) and the single quote (‘) are missing from the set of allowed characters! Why is that?
Regarding the underscore, things are quite simple: I don’t think it’s needed. The CamelCase convention (where variables are named like thisIsAVariable) is good enough in my opinion, and also very clear.
What happened to the single quote, instead? It will be clear in a moment.
With that (almost) clarified, let’s continue from the simpler to the tougher, and take a look at how I defined the numeric objects – integer and float types.
num : ('+' | '-')? float
float : (frac exp?) | (int frac? exp?)
int : '0' | digit+ digit0*
frac : '.' int
exp : '^' ('+' | '-')? int
Just one word before a full explanation: I used all over the grammar the single quotation mark to delimit parts of the grammar. So, if I write ‘+’
it means that there must be a plus symbol for that token to be valid. That’s partially why the single quote is not a valid character in the Grammar, so there’s no confusion about it.
Okay, what is happening in the last few definitions? First, I defined a num
(numeric) grammatical token. This is made by a sign (either plus or minus) followed by a float
token. Notice also that the sign is optional, and, as you would guess, the number is positive by default when the signed is omitted.
What’s the float
token? I defined it as a choice between two cases: it can either be a frac
(fractional part), followed by an optional exponent part, or it can be an integer token, optionally followed by a fraction and also an optional exponent.
Remember that the pipe |
means OR (either of two), and the question mark ?
after a parenthesis means that the group of characters in parentheses is optional. Also, the star *
after a parenthesis means that the group of characters in parentheses can be repeated zero or more times, while the plus +
means the group can be repeated one or more times. Don’t get confused between ‘+’
and just +
. The former means the symbol ‘+’, whereas the latter is a notation in the regular expression syntax.
My definition of float is not extremely elegant, but it’s very explicit. In particular, it makes clear that you don’t need to start with an integer if you want to write a floating point number. You can just start with the dot, like in the number .25
, which is interpreted as 0.25
.
What about the integer token? I very simply defined it either as a single ‘0’
, or as a sequence of digits that does not start with zero. So, in my language you could write x = 0
to define a new integer, and also x = 1
, but you could not write x = 01
. Quite standard, isn’t it?
I defined the fractional part also simply as a dot followed by an integer. So far, so good. You could write x = 1.25
, and ‘1’
would be the integer part, while ‘.25’
would be the fractional part, made by a dot and another integer.
Lastly, the exponent. Here I introduced a small novelty. The vast majority of programming languages uses the exponential notation with the E
(or e
) letter. I decided to use the caret ^
, like scientists do on the calculator. A small nuance, nothing more. After the caret you have an optional sign (plus by default) followed by an integer. So, x = 1.25^5
would be a valid num
token in my language. And its meaning it’s the same as in languages where you use the E
notation: 1.25
times 10
at the power 5
.
The other building block a language truly needs are strings, or characters array at least. I defined string in the following way.
str : quotedStr ('+' quotedStr)*
quotedStr : ' " ' (char)* ' " ' (',' obj)*
The basic unit of a string is a “quoted string”. This is what you would actually call string in other languages, that is a sequence of characters in between double quotes.
So, for example, "abc def”
is a valid quotedStr
token in my Grammar. However, my definition is a bit more complex, and let you create strings the C (or Python) way. Basically, each such sequence of characters can be followed by a comma ,
and an object obj
, possibly repeated. This is to allow string interpolation. Here’s one example:
“Abc %d defg”, 5
As you can see, there a single pair (comma, object) after the closing double quote. So, if you are familiar with other programming language, you already know that the “5”
will be interpolated where the “%d”
is in the string.
The following string, with two pairs of (comma, obj), is also valid according to Grammar:
“The number %d is greater than %d”, 5, 4
And this explains why I wrote (‘,’ obj)*
in the Grammar: to allow for multiple interpolations (zero or more).
Having said that, the definition of string in the Grammar is just a quotedStr
, optionally followed by a plus sign +
and another quotedStr
, etc. This way you can concatenate strings as in the following example:
“first “ + “second is %d”, 2 + “hello, third”
You have probably noticed that I didn’t define explicitly the obj
token used in the definition of quotedStr. We’ll do it soon.
Other basic types
The choice of what basic types are to be supported in a language is an important one. It will affect forever how people write code in your language. Can you imagine what would Python be without lists? What if C had built-in dictionaries?
I decided that I wanted to support lists, in this new programming language. The Python way, to be clear. I find lists really explicit and handy to use. However, I also want to encourage good programming patterns, therefore I will force lists to contain only objects of the same type.
I have seen enough of bad programming practice that mixes different object types in the same container, and want to avoid that to ever happen in my language. This last constraint, however, is not a syntactical one, rather is a semantic constraint, so the Formal Grammar is not concerned by it.
I also wanted to add a boolean type, and the NULL
type. Finally, I defined the “variable” type to be any sequence of characters that is not a reserved keyword.
obj : var | num | str | bool | null | list
bool : 'True' | 'False'
null : 'NULL'
var : letter (digit | letter)*
list : '[' (listExpr)? ']'
listExpr : obj (',' obj)*
listElem : var '[' int ']'
Now the obj
definition is clear. A obj
token is either a variable, a numeric, a string, a boolean, a list or even NULL
.
A detail to note is that variables (names) can only be made of letters and digits. As I already said, no underscore or other strange things!
The grammatical definition of list is more interesting. First of all, you must have a open square bracket [
. Then you have an optional token, called listExpr
(list-expression), followed by a closed square bracket ]
, that is not optional.
First remark: the definition implies that you can write empty lists: [ ]
is a valid expression according to the grammar.
The listExpr
token is not very surprising. It’s made by a obj
token, optionally followed by a sequence of pairs (comma, obj)
. This definition allows to stack up in a list as many obj tokens as you wish.
A second remark is worth noting here. My definition of list forbids to end a listExpr
token with a trailing comma. As you may already know, in Python you can have a trailing comma in a list, like in [1, 2, 3, 4,]
, and the Python interpreter will take care of that final comma for you. In my language, instead, if you have a trailing comma like that you will receive a compilation error.
After some thought I decided to include another “type”, among the basic one. I called it listElem
(list-element), and it simply identifies the natural (and explicit!) way you would index an array, or a list in this case. It’s made by a var token, which should always be the name of a list object, and a pair of square brackets with an integer token between them.
Lots of words just to say that x[1]
is a valid expression in the Grammar, and it just means to take the element in position 1
in the list identified by the variable x
. Standard stuff. Are we sure?
My first mistake
I must be honest and say that as far as numeric, strings, boolean and other basic types were concerned, my work went smoothly. Surely because these are very standard grammatical constructs, and I studied them both in the MOOC and on my reference book.
With lists things got a bit trickier. The list definition itself was not complicated, but I had to think about all its possible implications.
That’s when I made my first mistake. It’s was even more than “just” a mistake, it was a misunderstanding on an important concept. And that’s what makes it even more important: I think to go over my (wrong) reasoning, and see how I corrected it, can be very beneficial to other students.
I initially included the listElem token among the choices for the obj token. So, the definition was:
obj : var | num | str | bool | null | list | listElem
I wanted it to be that way because I thought having the listElem
like one of the basic types would be useful. However, that led to a very subtle issue. Let me illustrate it.
As we will see later in this article, the Grammar will also include a “output statement”, that has to be interpreted like the “print” function in Python, or the “printf” in C. In my Grammar, I defined it as made by the keyword writeOut
followed by a obj
token.
So, for example, if x
is a token obj
(that means, a var
, or a string
, etc.) you could write writeOut x
, and that will compile correctly, and will print at screen the value stored into x
. Formally, the definition is
output : ‘writeOut’ obj
Here’s where the problem comes. Or rather, where I thought it came.
If listElem
was part of the obj
token choices, then there would be two cases where the keyword ‘writeOut’
could be followed by a var
token:
- When it’s really just a
var
token. - When it’s the var token that starts a
listElem
.
This means the Grammar would not be LL(1), because after the parser grabs the token ‘writeOut’
and looks ahead, and sees a var
token, it wouldn’t know whether it’s just a var
or a listElem
. It would actually need to look further ahead, but I didn’t want to design a LL(2) Grammar.
If you are wondering what happens in similar cases in widely used languages, such as Python, just know that common Programming Languages have several constructs that are not LL(1), and are handled ad-hoc by the compiler.
I spent some time brainstorming about this issue, and eventually decided to exclude the listElem token
from the obj token types.
So, I thought I had solved the issue. Instead I was wrong. In fact, I was wrong twice!
I got the whole (and right) picture only much (much) later, while I was working on the Semantic Analysis module of the language. This is why I am telling you about the entire process – I think it can be a very helpful learning experience.
While working on a later module of the Compiler, I realized what was wrong in my reasoning. Let’s put ourselves in the position of the Parser, that is currently parsing an Output statement, such as
writeOut x[1]
where x
was previously defined as a list, for example
x = [1, 2, 3]
What will the parser do? I was wrong (again!) in saying that when it gets the 'writeOut'
token, it will have to look ahead two tokens to understand whether it’s just 'x'
(list) or it’s actually 'x[1]'
(listelem).
Why was I (doubly) wrong?
The reason is that after getting the “writeOut”
token the Parser will only need to know that a obj
token is after that. Therefore it won’t look ahead at all, not even 1 step. It will simply delegate the task to some sub-module that has to parse a obj
token.
What will happen next, then? This sub-module (that I will show later), will now point at the 'x'
token. Only now it will look ahead 1 token, and just 1 token, to figure out if it’s a var
or a listElem
. At this point looking ahead one token only is more than enough. Therefore the Grammar is still LL(1), and the final obj
definition is:
obj : var | num | str | bool | null | list | listElem
Operators
After the somewhat intricate definitions above, I needed something easier to work on! So I defined, in a “almost standard” way, the logical operators allowed in the Grammar. Here they are.
operator : '+' | '-' | '*' | '/' | '/.' | '%' | condOp
condOp : '&&' | '||' | '!=' | '==' | '<=' | '>=' | '>' | '<'
These are very normal definition, with the exception of the token '/.'
– this is something I added because I wanted to distinguish between the standard division operator, that truncates the result when the operands are integer numbers. So, 3/4
will yield 0
(integer division), but you can write 3/.4
and it will yield 0.75
.
Wait, there’s actually a blind spot here! What if I write 3/.4
but what I really mean is 3
divided by 0.4
? Well, in this case you will need to add one space, because the characters are read from left to right, so if the dot .
is found immediately after the slash /
, then it will be interpreted as a floating division /.
.
You would write 3/.4
if you mean “3 divided by 4, without truncating the result”, while you’d write 3/ .4
, if you mean “3 divided by 0.4, with integer truncation” (which is, by the way, quite a strange thing to do).
At any rate, I do recommend the Python convention to add spaces around the operators. So, just write 3 /. 4
and everything will be more readable. Or also 3 /. .4
if you want to compute the floating point division between 3 and 0.4.
Speaking about this, for a long time I considered to forbid floating point to start with a dot. I wanted to force the usage of zero, so you’d never write .4
, and always 0.4
. I decided not to, eventually, for consistency with many (many) other languages. Nonetheless, I do encourage programmers to type that zero on their keyboard!
Expressions
Expressions are a fundamental block of any programming languages. Actually, as you should know if you read my previous articles, the ability to write balanced expressions (with balanced parentheses) is exactly what makes Context Free Grammars more powerful than Regular Expressions, and give them the power to design entire languages.
This is also why Expressions, and in particular Arithmetic Expressions, are the single most used example in textbook about Formal Grammars. Therefore, I pretty much already knew what to do here. My only challenge was to make sure the definition included the other basic types of my Grammar, and not just numeric (like in arithmetic expressions).
expr : term ( ('+' | '-') expr)?
term : baseExpr ( ('*' | '/' | '/.' | '%') term)?
baseExpr : obj | '(' expr ')'
I suggest you pay attention to the patterns in the definition above, because they are standard and thus very important to know. Let me illustrate them.
There are three basic blocks, which you can think of as three rings in a chain: the general expression expr
, the inner term term
, and the basic expression baseExpr
. They are somehow ordered, in the sense that the definition of expr
involves the definition of term
, and the definition of term
involves the definition of baseExpr
. Finally, baseExpr
can either be a basic obj
token, or a whole new expression, but only if it’s enclosed in parentheses.
This way of defining expressions ensures a very important thing: the Grammas is not ambiguous. Ambiguity is really bad for Formal Grammars, and is to avoid with all means.
In the case of expressions, ambiguity can come from the operator precedence. If you write 5 + 3 * 2
, there must be one and only one way this expression is interpreted by the Grammar (and hopefully is the one that prioritizes the star *
operator over the plus +
).
The recursive definition with three basic blocks (Expr, Term, baseExpr) is guaranteed to be unambiguous, so it’s worth sticking it to our mind.
Program and Statements
Expressions were the last among the building blocks. With that done, I decided to jump right at the top of the Grammar and clarify what the whole Program will look like.
Once again, I took a very explicit approach to this design challenge, and I told myself: A Program will simply be a sequence of statements, that I will call Lines, and each Line must be followed by a Endline token.
The concept of Line/statement includes really all types of statement. So, a simple assignment (e.g., x = 5
) will be a line
, and also a long and complex if-then-else will be just one line
. That also implies that a Line must be able to contain more Lines.
Here’s the definition of Program I came up with. You can think of the Program token as if it’s used to represent the entire source code.
program : (line ENDLINE)*
ENDLINE : ';' '\n'
line : assign
| input
| output
| ifLine
| loopLine
| breakLine
| contLine
The first grammatical rule says a program
is a (possibly empty) sequence of pairs (line, Endline)
. As already said, a line
can be anything from an assignment operation assign
, to a complex loop instruction loopLine
. You should really think of a Line token like a “logical line”.
The Endline
token instead is a very simple token meant to clarify the end of a logical line, and it’s made of two characters: a semicolon and a newline. I believe this a small novelty that I introduced with respect to other languages. Let me explain why.
In all languages I know, you can put two logical statements on the same physical line, for example:
x = 5; y = x + 2;
is a valid string in Python, C, Java, etc., and it consists of two assignment operations.
In my Grammar instead, physical lines and logical lines are terminated together*, because the Endline token contains a ‘\n’
. Thus, the previous example would give a compilation error, and you must instead write
x = 5;
y = x + 2;
I believe this improves the readability of the code, and in fact programmers are supposed to follow this practice even if it’s not enforced by the language… just that sometimes they do not!
It is worth noting that the Endline
token is the only one where the semicolon appears. Therefore, you can’t really write a semicolon in my language if it’s not followed by a \n
character.
Now, let’s stop one more minute here to think about the implications brought by the concept of logical Lines. Let’s start with an example of valid Program:
<Program>
<Line>
<Assign>
<Endline>
<Line>
<ifLine>
<Endline>
This program
corresponds to a source file made of just two lines, the first being an assignment and the second being a ifLine
. It could look like the following excerpt:
a = “a valid string”;
if (a != NULL)
inner-Line1;
inner-Line2;
;
It’s really important to understand that the first line
ends at the second double quote (...string”
) and it’s correctly followed by a Endline
token. Then, the second line
starts and it’s a ifLine
. As we will see in a moment, the ifLine
can contain multiple Lines, each terminated by a Endline
.
What I want to underline is that the ifLine must be terminated by a Endline token too. This is the semicolon that you see as the last line in the example.
Let me repeat the concept again. The last semicolon in the example is (part of) the Endline
that terminates the ifLine
started with if (a != NULL)
.
This way to terminate complex instructions, such as a if
block, is slightly uncommon, because in most languages you open a curly bracket at the beginning of the if
, and then “close” such a bracket when the if-body is done, as in the following code
a = “a valid string”;
if (a != NULL) {
inner-Line1;
inner-Line2;
}
On the other hand, and to be absolutely honest, my idea of “logical lines” is not a new one. There are already a few languages using it. Python has the same concepts, and implements it with an INDENT token. Indeed, if you know Python then you know that indentation plays an important role in it.
Other languages terminate the if statements with the end
keyword, which is the closest to my choice that you can think of. Matlab is an example of such languages.
I must say I am very happy with this design choice of mines. To terminate complex blocks with a semicolon feels really natural once you grasp the concept of logical lines, and I think the simple, lonely, semicolon at the end of the block it’s quite nice looking. And don’t forget there’s an invisible \n
next to it!
At this point, let’s see the grammatical definition for each of the possible Lines, starting with the ifLine.
Conditional statement - if
The conditional line (statement, if you will) is meant to represent branches in the code, such as the if-then-else statement. Thus, my definition for it is quite simple.
ifLine : 'if' ifCond ifBody
Basically, the `ifLine is a sequence of three elements.
- First, a constant token,
“if”
. - Then a token called
ifCond
. This is meant to represent the logical condition that, if True, will let the flow “enter” the if. - Then, a token called
ifBody
, which hopefully is superfluous to explain.
Now, it’s time to recursively define the ifCond
and ifBody
token, to complete the definition of ifLine
. Let’s start with the ifCond token.
My second (bigger, and most useful) mistake
To define a sound syntax for the if
statement was a tricky affair. It wasn’t all clear to me until I wrote the code for the parser. I do understand the details now though, so this is also a very good lesson to share.
In my mission to keep things explicit, I initially defined the ifCond as it follows
ifCond : '(' obj condOp obj ')'
It made perfect sense to me, at the beginning. Open a parenthesis, create a conditional expression with two obj
token (that is, two primitive types of my Grammar) and then close the parenthesis.
Unfortunately, I soon realized this was way too restricted. With this syntax you can’t even write
if (x + 1 == y)
because the first part x+1
is not just a token obj
, it’s a whole expression. Therefore, I understood that I could not keep things too restricted in the ifCond
and decided to change it to the following.
ifCond : '(' expr condOp expr ')'
This sounds right, isn’t it? The expr
token gives a lot of flexibility and all you have to do is to write two expressions with a conditional operator (==
, !=
, &&
, <
, etc.) in between them.
For example, you could now write
if (x + 1 == y + z)
and the Grammar would be fine with it. I thought I nailed it.
Not quite.
As I kept digging deeper (again, I understood all this later, while I was writing the parser) I realized the latest definition of ifCond
didn’t work well.
To start with, I couldn’t use more than two conditions, such as in
if (boolean1 && boolean2 && boolean3)
This could be solved by rewriting it as
ifCond : '(' expr (condOp expr)+ ')'
so that we could use as many boolean expressions as we wanted. But then, when I thought about this, I realized there was a much bigger issue in my design.
What about the following line:
if (x + 1 == y && boolean1)
This is a perfectly fine, intuitive way to write a piece of code and it should really be supported by a good Grammar. However, notice that in the parentheses there is one conditional operator ==
used as part of the expression x+1==y
, and another one &&
used to link and evaluate two expressions.
This clarifies that there was a major flow in my design, at this point. But luckily, I also figured out the source of the problem.
The problem lied in a simple fact: I was not able to use conditional operators in the logical expressions!
After I realized this single thought, everything became clearer soon. In fact, in many languages, expressions have a value. In C, for example, you can write int x = a && b;
and the result of the expression a && b
is assigned to the variable x
.
This also allowed me to understand that I didn’t need to design the ifCond
as a condition between two expressions. One expression alone is enough, because it’s evaluated no matter how complex it is. And, as a convention, there is a defined set of basic values that evaluate to “false” (e.g., 0
, NULL
, False
, and a possibly empty list).
Thus, I was finally clear about the way to go. I had to redesign the expr
token to include conditional operators and then the ifCond will simply be
ifCond : '(' expr ')'
That single expression will be evaluated, and its value will be the condition to enter the if branch or not.
In hindsight this all looks pretty obvious now, but it totally wasn’t for me!
Okay, so, how to modify the grammatical definition of expression token? We understood in a previous paragraph that operators priority is implemented with a chain of tokens, such as the chain made by expr
, term
, baseExpr
.
Now, if I want to add conditional operators and assign them a different priority then I need to add a new ring to the chain.
I decided this was the case, because in general conditional operators have the lowest priority, at least in my intuition. Let’s take an example. When I write
if (x + y <= 3)
I really mean that I first want to compute the sum x+y
and then check if it’s smaller or equal than 3
. This means that the conditional operator <=
has a lower priority than the plus +
. And plus is already at the lowest priority (less than multiplication and division, for instance).
Sure, I could use more parentheses. If I wrote
if ((x + y) <= 3)
then it would be all good, but it definitely seems unnecessary to do so.
So, all considered, I added one more element in the recursive rule for the expr
token and called it pred
(as for logical predicate). Since this is the lowest in the priorities, it will be at the top of the chain.
Here’s the new grammatical rule for the expr
token.
expr : pred (condOp expr)?
pred : term ( ('+' | '-') pred)?
term : baseExpr ( ('*' | '/' | '/.' | '%') term)?
baseExpr : obj | '(' expr ')'
By comparing this with the previous (flawed) rule, the design pattern is very clear and easy to understand.
One last thing worth noticing. I didn’t differentiate between conditional operators. It means that, for example, &&
and <=
have the same priority. As a consequence, if you write
if (x <= y && boolean1)
it’s not guaranteed which of the two logical expressions will be executed before. It could either be (x <= y) && boolean1
, or it could be x <= (y && boolean1)
. This is not a case of ambiguity, it’s a design choice. I know the first case is far more common, yet all logical operators are the same to me, so in similar case I want you use parentheses.
Alright! With this troublesome issue solved, now it’s time to breath again!
Back to the if statement
Let’s complete the definition of ifLine by specifying what the ifBody is.
ifBody : (line ENDLINE)+ (optElse)?
optElse : 'else' (line ENDLINE)+
At this point, the above two definitions should be very easy to understand. The ifBody
token is defined as a non-empty sequence of (line, Endline)
. The last of these pairs may be followed by a optElse
token (optional Else).
The optElse
token is made of the keyword “else”
followed by a non-empty sequence of (line, Endline)
.
I think this is quite intuitive. Basically, both the if and the else branch are sub-Program tokens.
Here is how a simple and valid if-then-else would look like in my Grammar.
if (expr1)
line1;
line2;
else
line3;
;
Mind the final semicolon!
Nested if statements would be written like this one:
if (expr1)
line1-1;
line1-2;
else
if (expr2)
line2-1;
line2-2;
else
line2-3;
line2-4;
;
;
Writing a sound grammatical rule for the conditional statement (ifLine) was definitely the piece of work I learnt the most from!
Loop statement - while
With the ifLine
out of our way, I believe the loop statement will not require any comment!
Here’s the definition.
loopLine : 'while' ifCond loopBody
loopBody : program
Just notice that I am using again the ifCond
, as well as the whole program token. Pretty useful, isn’t it?
Input, Output, Assignment
The line
definitions that we are still missing to complete the program
token are those related to I/O and assignment. Luckily, I kept these very simple and, once again, explicit.
input : ‘readIn’ var
output : 'writeOut' obj
assign : var '=' expr
Notice that “readIn”
and “writeOut”
are reserved keyword. I will leave the understanding of these three simple definitions as exercise for you!
My third (but not last!) mistake
Here’s another thing I got wrong about the Grammar. It’s going to be the last mistake for this article, but definitely not my last one in the whole Compiler’s studies!
As I said at the beginning, my objective is to build an implicitly typed programming language. This means that the Compiler knows about types, but it’s able to understand them all by itself. The programmer does not need to declare types explicitly.
For example, you would simply write
x = 5;
y = NULL;
And the Compiler would understand that x
is integer and y
is a null type. You do not need to write
int x = 5;
Object y = NULL;
like in Java, C++, etc. What’s even more important is that, if later in the program you write
z = x + y;
The Compiler will remember the types x
and y
were assigned to, and will tell you that the operation +
is not allowed between these two types. And the compilation will stop with an error.
So, my language is statically typed, but implicitly, which saves some time in typing on the keyboard.
It’s worth underlining that this is a very different behavior from what we see, for example, in Python, Perl, and other scripting language. There, when an operation is not possible between two types, the error is generated at runtime, not during the compilation (which often does not even exist, in scripting languages).
Type-checking is part of the Semantic Analysis, and this is why I didn’t immediately realize that I made a mistake at this point. The problem is with the Input Line.
If all we declare is readIn var
, how could the Compiler possibly know what’s the type of the newly assigned variable? It just can’t.
That’s true in many languages. For example in Python3, you would do
x = input()
And x
would automatically given a str
class (because Python is Object Oriented), regardless of what you enter. Even if enter just digits, such as 1234
, and wanted to have an integer variable, x
will still be a string.
You are required to do an explicit type cast, if you want an integer. Something like
x = int(input())
Type cast is a very weird beast in my opinion. It’s totally unsafe, and can potentially lead to crashes at runtime. Still, it’s very common especially in interpreted languages.
At any rate, since types are implicit in my language, it didn’t make sense to support type casting. I would also have to introduce all keywords reserved to types.
I therefore decided to modify the Input Line. The new definition is
input : readIn var
where readIn
is not a keyword anymore, it’s another token type, defined as it follows.
readIn : 'readInt' | 'readFloat' | 'readBool' | 'readStr'
Like that, when you write an Input Line you will also have to declare what’s the input type, for example
readInt x;
and the Compiler will assign type int to the identifier x
. Obviously, it does not make sense to have a readNull
keyword.
Break and Continue
In the program
token, as you’ve already seen, I also added the break
and continue
instructions, that are quite useful when managing control flow. I kept them as last ones because they are the easiest!
breakLine : 'break'
contLine : 'continue'
Summary
At this point all pieces of the Grammar have taken their places. Here’s how the entire thing looks like.
digit0 : 0-9
digit : 1-9
letter : a-z | A-Z
otherChar : |!”%&/()=+-*#><;,^.][\n \t
char : letter | otherChar | digit
num : ('+' | '-')? float
float : (frac exp?) | (int frac? exp?)
int : '0' | digit+ digit0*
frac : '.' int
exp : '^' ('+' | '-')? int
str : quotedStr ('+' quotedStr)*
quotedStr : ' " ' (char)* ' " ' (',' obj)*
bool : 'True' | 'False'
null : 'NULL'
var : letter (digit | letter)*
list : '[' (listExpr)? ']'
listElem : var '[' int ']'
obj : var | num | str | bool | null | list | listElem
listExpr : obj (',' obj)*
program : (line ENDLINE)*
ENDLINE : ';' '\n'
line : assign
| input
| output
| ifLine
| loopLine
| breakLine
| contLine
input : readIn var
readIn : 'readInt' | 'readFloat' | 'readBool' | 'readStr'
output : 'writeOut' obj
assign : var '=' expr
expr : pred (condOp expr)?
pred : term ( ('+' | '-') pred)?
term : baseExpr ( ('*' | '/' | '/.' | '%') term)?
baseExpr : obj | '(' expr ')'
operator : '+' | '-' | '*' | '/' | '/.' | '%' | condOp
condOp : '&&' | '||' | '!=' | '==' | '<=' | '>=' | '>' | '<'
ifLine : 'if' ifCond ifBody
ifCond : '(' expr ')'
ifBody : (line ENDLINE)+ (optElse)?
optElse : 'else' (line ENDLINE)+
loopLine : 'while' ifCond loopBody
loopBody : program
breakLine : 'break'
contLine : 'continue'
I must say I do like the result. First of all because is a neat and quite simple Grammar. Sure, at the moment it does not allow for many important things, such as OOP and routines. I will definitely add routines at some point down the road.
Despite that, this Grammar is LL(1), a feature I really wanted so that I can further learn by implementing a LL(1) recursive descent parser. Moreover, the Grammar does allow for constructs such as input, output, conditional branching and loops, therefore the generated Language is Turing-complete.
A Complete Example
Although this work is still far away to be a new Programming Language, I want to show you how a meaningful source code would look like.
As an example, let’s consider every student’s favorite exercise: read an integer number N and compute the total sum of the first N prime numbers.
Here’s how I would implement this in Python (> 3.6) and in my own language.
# Python3.6
N = int(input())
total = 0
for i in range(2, N + 1):
isPrime = True
for j in range(2, int(i/2) + 1):
if i % j == 0:
print(f'{i} is not prime')
isPrime = False
if not isPrime:
break
if isPrime:
total += i
print(f'Total primes sum until {N} is {total}')
# My language
readInt N;
totSum = 0;
i = 2;
while (i <= N)
j = 2;
isPrime = True;
while ((j <= i / 2) && isPrime)
if (i % j == 0)
writeOut "%d is not prime", i;
isPrime = False;
;
j = j + 1;
;
if (isPrime)
totSum = totSum + i;
;
i = i + 1;
;
writeOut "Total primes sum until %d is %d", N, totSum;
Conclusions and Outlook
The design of a formal, LL(1) Grammar for a new Programming Language is not only a fun task, but it’s also very instructive.
A Grammar itself though, while fun to design, is not very useful. To take this one step further and build a new Programming Language out of it, as we already know, all the other main modules of a Compiler must be built: Parsing, Semantic Analysis and Code Generation.
References
Language Implementation Patterns. A book by Prof. Terrence Parr.
Alex Aiken’s class Compilers at Stanford University. Available as free MOOC online.
My article What Is A Programming Language Grammar?.
My article How to design Formal Grammars.
My article What are the differences between programming languages?.
Python Lexical Analysis documentation page.
My GitHub repository for this course.


Open3D
latest (cf20af6)
About Open3D
Getting Started
Compiling from source
Building Documentation
Contributing to Open3D
Tutorial
Basic
Advanced
Point cloud outlier removal
Colored point cloud registration
Global registration
Fast global registration
Multiway registration
RGBD integration
Color Map Optimization
Customized visualization
Non-blocking visualization
Interactive visualization
Headless rendering
Reconstruction system
C++ interface
Docker
Reference
Python API
open3d.camera
open3d.color_map
open3d.geometry
open3d.io
open3d.integration
open3d.odometry
open3d.registration
open3d.utility
open3d.visualization
Open3D
Docs
»
Advanced
Advanced
¶
Point cloud outlier removal
Prepare input data
Select down sample
Statistical outlier removal
Radius outlier removal
Colored point cloud registration
Helper visualization function
Input
Point-to-plane ICP
Colored point cloud registration
Global registration
Input
Extract geometric feature
RANSAC
Local refinement
Fast global registration
Input
Baseline
Fast global registration
Multiway registration
Input
Visualize optimization
Make a combined point cloud
RGBD integration
Read trajectory from .log file
TSDF volume integration
Extract a mesh
Color Map Optimization
Input
Rigid Optimization
Non-rigid Optimization
Customized visualization
Mimic draw_geometries() with Visualizer class
Change field of view
Use callback functions
Capture images in a customized animation
Non-blocking visualization
Review draw_geometries
Prepare example data
Initialize Visualizer class
Transform geometry and visualize it
Interactive visualization
Crop geometry
Manual registration
Select correspondences
Registration using user correspondences
Headless rendering
Install OSMesa
Install virtualenv
Build Open3D with OSMesa
Test headless rendering
Docs version
latest (cf20af6)
Versions


Classes
The following classes are available globally.
-
Used to manage connections to Qredo and create, manage and respond to Rendezvous.
See moreNote
Your app must be initialised and connected to a network before using any Qredo services.Declaration
Objective-C
@interface QredoClient : NSObject
Swift
class QredoClient : NSObject
-
The highwater mark is the marker from which to retrieve messages in a Conversation. Objects of this class are not created directly
See moreDeclaration
Objective-C
@interface QredoConversationHighWatermark : NSObject
Swift
class QredoConversationHighWatermark : NSObject
-
Used to refer to a specific
QredoConversation
. Not created directly. Developers can find extract this value from theQredoConversationMetadata
.Declaration
Objective-C
@interface QredoConversationRef : QredoObjectRef
Swift
class QredoConversationRef : QredoObjectRef
-
Contains information about a
QredoConversation
. Accessed fromQredoConversation.metadata
and returned by enumerateConversationsWithBlockThe properties are all read only.
See moreDeclaration
Objective-C
@interface QredoConversationMetadata : NSObject
Swift
class QredoConversationMetadata : NSObject
-
Represents a secure channel of communication between two app users
Objects of this class are never created directly, but returned by the Qredo SDK as a result of:
- responding to a Rendezvous by calling respondWithTag
enumerating the list of Conversations that the current user is a party to by calling enumerateConversationsWithBlock
See moreNote
When a Conversation is established between two parties, as a result of one user responding to a Rendezvous, a Diffie-Hellman key exchange takes place between the creator and the responder. These keys are randomly generated and used to derive a further set of keys that are used to encrypt messages in such a way that only the two parties in the Conversation are able to read the messages. All of this is handled behind the scenes by the Qredo SDK, but you can use the fingerprints of the public keys to authenticate the Conversation and ensure that there has not been a ‘man-in-the-middle’ attack. See the Authenticating a Conversation methods later in this section.
Declaration
Objective-C
@interface QredoConversation : NSObject
Swift
class QredoConversation : NSObject
-
Represents a Conversation message. Contains the message itself, together with metadata
See moreSee
Sending a Conversation Message: Objective-C, Swift Listening for Conversation Messages: Objective-C, SwiftDeclaration
Objective-C
@interface QredoConversationMessage : NSObject
Swift
class QredoConversationMessage : NSObject
-
Logs diagnostic output to the console.
By default logging will be reported for all objects, however you can restrict logging to a list of permitted classes using addLoggingForObject or addLoggingForClassName
You can use logging in two ways:
QredoLogError(@"My car is %@",car.colour]);
This is similar to NSLog - here the car.colour is calculated each time the line is encountered, whether or not the message is displayed.
In this case the logging will only be output if the logging level is
QredoLogLevelError
or above.For other logging levels, use
QredoLogWarning
,QredoLogInfo
,QredoLogDebug
orQredoLogVerbose
- For a more flexible version of logging, you can specify a code block that will be executed only when the current logging level requires it.
For example, the following code takes a code block that will only be executed when the logging level is QredoLogLevelDebug or above. The block will return a value that is displayed in the log.
QredoLogDebug(@"Index item count : %i", ^{ return [self count];}());
Use this method of logging if calculating the required logging output will take a long time to process.
See moreDeclaration
Objective-C
@interface QredoLogger : NSObject
Swift
class QredoLogger : NSObject
-
Encapsulates the decoding of incoming Apple Push Notifications into Qredo Objects it contains the decrypted message and a refernece of it’s parent ‘QredoConversation’. The APN contains a Qredo Queue ID which is an internal representation of one side of a QredoConversation, this reference is used to lookup a reference to the coresponding QredoConversaition. This lookup table is stored in NSUserDefaults Although the Payload of the Push Notification is encrypted, the remaining parts of the Push Notification leaks some information - in particular the Queue ID could be used to group a number of Push Notificaiotns together. Careful thought should be given to the security requirements of your App, before using Push Notifications.
Without a QredoClient object the Push Notificaiton can’t be decrypted. So in order to automatically create a QredoClient when an incoming Push Message is received the Login/Credential values must be stored somewhere locally. See Qredo.h initializeFromUserDefaultCredentialsInAppGroup for more details.
See moreDeclaration
Objective-C
@interface QredoPushMessage : NSObject
Swift
class QredoPushMessage : NSObject
-
Used to represent ConversationIDs and other values used by the SDK.
Developers should not need to manipulate QredoQUID objects
See moreDeclaration
Objective-C
@interface QredoQUID : NSObject <NSCopying, NSSecureCoding>
Swift
class QredoQUID : NSObject, NSCopying, NSSecureCoding
-
Used to retrieve, activate and deactivate a particular Rendezvous.
Pass this ref to fetchRendezvousWithRef, activateRendezvousWithRef and deactivateRendezvousWithRef
Stored in the
QredoRendezvousMetadata
Declaration
Objective-C
@interface QredoRendezvousRef : QredoObjectRef
Swift
class QredoRendezvousRef : QredoObjectRef
-
Contains information about a previously created Rendezvous. Used to retrieve the
QredoRendezvousRef
QredoRendezvousMetadata
objects are returned by enumerateRendezvousWithBlock:completionHandlerOther Rendezvous information can be accessed from the
See moreQredoRendezvous
Declaration
Objective-C
@interface QredoRendezvousMetadata : NSObject
Swift
class QredoRendezvousMetadata : NSObject
-
Represents a Rendezvous. Created with createAnonymousRendezvousWithTagType
See moreDeclaration
Objective-C
@interface QredoRendezvous : NSObject
Swift
class QredoRendezvous : NSObject
-
The class that
See moreQredoRendezvousRef
andQredoConversationRef
derive from Objects of this class are not created directlyDeclaration
Objective-C
@interface QredoObjectRef : NSObject
Swift
class QredoObjectRef : NSObject
-
A collection of utility functions for converting between keys, hex data strings and readable words. RFC1751 is a standard for the representation of binary keys as 3 or 4 character English words.
This class includes RFC1751 compliant methods and a non-compliant implementation designed for smaller, low entropy keys
See moreDeclaration
Objective-C
@interface QredoUtils : NSObject
Swift
class QredoUtils : NSObject
-
Helper Class to faciliate the easy creation of Diffie Hellman Channels. Use for exchanging Rendezvous over an insecure communciations channel.
Device 1 sends publicKey to Device 2
Device 2 sends publicKey to Device 1
Device 1 sends encrypted message to Device 2
Device 2 decrypts message from device 1
Declaration
Objective-C
@interface QredoSecureChannel : NSObject
Swift
class QredoSecureChannel : NSObject
-
Used to represent the state of the Vault. This is the mark to search from when enumerating VaultItems
Pass this as a parameter to
enumerateVaultItemsUsingBlock
Declaration
Objective-C
@interface QredoVaultHighWatermark : NSObject
Swift
class QredoVaultHighWatermark : NSObject
-
Identifies a specific version of a vault item.
Developers do not create this objects directly. Stored in the QredoVaultItemMetadata Used to retrieve a vault item with getItemWithDescriptor, getItemMetadataWithDescriptor, getLatestItemWithDescriptor and getLatestItemMetadataWithDescriptor
See moreDeclaration
Objective-C
@interface QredoVaultItemDescriptor : NSObject
Swift
class QredoVaultItemDescriptor : NSObject
-
Information about a vault item. These properties are read only. Constructed when a
See moreQredoVaultItem
is created and returned fromenumerateVaultItemsUsingBlock
Declaration
Objective-C
@interface QredoVaultItemMetadata : NSObject <NSCopying, NSMutableCopying>
Swift
class QredoVaultItemMetadata : NSObject, NSCopying, NSMutableCopying
-
Declaration
Objective-C
@interface QredoMutableVaultItemMetadata : QredoVaultItemMetadata
Swift
class QredoMutableVaultItemMetadata : QredoVaultItemMetadata
-
Represents a VaultItem. Contains properties for the vault item’s data and metadata
See moreDeclaration
Objective-C
@interface QredoVaultItem : NSObject
Swift
class QredoVaultItem : NSObject
-
Contains the methods to add, retrieve, search for and delete items in a Qredo Vault.
Objects of this class are not constructed by the developer, but returned from the defaultVault method
See moreDeclaration
Objective-C
@interface QredoVault : NSObject
Swift
class QredoVault : NSObject


surfactant OpenUrl albumin cell solution alveolar sPLA SRB Fig. raise CrossRef lung debris ARDS Science Web lysate blood surface acid concentration mucins plasma acute albumin, raises respiratory Physiol distress images likely liquid solutions Infasurf alter does effect ghost IIA albumin. exogenous fluorescein intact monolayer normal pressure test T-raising alveolus debris, effects hydrolysis injection lipid phospholipase reduce saline Abstract cmH elevated lungs obtain ARDS. Appl HCl RBCs Sulforhodamine cells edema epithelial following heparinized injections membranes normalizes presence proteins suggests supernatant, tension FREE Med Perlman Table Text airway concentrations determine elevation fraction injury lower mechanism native pellet phospholipid pulmonary reduces sPLA<;sub>;<;/sub>; substances supernatant therapy tracheal volume (B) Biophys Download Effects However, IB, Images Ochs View aerated damage experimental fractions group hydrochloric include increase interfere isolated lipids model mucin possible present rat representative saline, solution, study syndrome tension, <; ARDS, Cell Holm Respir Sigma Surface area causes centrifuge confocal data extract function gastric hemoglobin injury. lining liquid, low lungs, membrane obtaining porcine previous product protein red secretory shown solution. sulforhodamine suspend syndrome. transpulmonary water (A) Care Chem Conricode Figure Hite IIA, Image Open Protocol RBC SRB, Sci Seeds Solution Waite Zhou activity alveoli and, attributable bar bovine charge compression concentrated contribute counter data-hide-link-title=""> data-icon-position="" different elevates figure flooded fully functional hydrophobic indicated indicating inhibition interaction macrophage marginally mechanical mechanisms min min) models mucins, mucins. new plus results serum study. subsequent substance surfactant, tab that, type ventilation ventilation-induced vitro °C,


These methods, respectively, set and query the default rank of the grammar. When a grammar is created, the default rank is 0. When rules and symbols are created, their rank is the default rank of the grammar.
Changing the grammar's default rank does not affect those rules and symbols already created, only those that will be created. This means that the grammar's default rank can be used to, in effect, assign ranks to groups of rules and symbols. Applications may find this behavior useful.
Return value: On success, returns the rank after the call, and sets the error code to
MARPA_ERR_NONE
. On failure, returns −2, and sets the error code to an appropriate value, which will never beMARPA_ERR_NONE
. Note that when the rank is −2, the error code is the only way to distinguish success from failure. The error code can be determined by using themarpa_g_error()
call.
These methods, respectively, set and query the rank of a symbol sym_id. When sym_id is created, its rank initialized to the default rank of the grammar.
Return value: On success, returns the rank after the call, and sets the error code to
MARPA_ERR_NONE
. On failure, returns −2, and sets the error code to an appropriate value, which will never beMARPA_ERR_NONE
. Note that when the rank is −2, the error code is the only way to distinguish success from failure. The error code can be determined by using themarpa_g_error()
call.


Doge Social Network
Home
Profile
Friends
Profile of Doge
Name:
Doge
Birthday:
Top secret
Occupation:
All eater
Area of occupation:
Web


Glaðsheimr
The fifth is Glaðsheimr,
and gold-bright there
Stands Valhöll stretching wide;
And there does Oðinn
each day choose
The men who have fallen in fight.
Grímnismál, The says of Grímnir
Vision
Glaðsheimr is an open project to research building complete applications that are capable of providing true privacy and transparency to end users. Research is focused on developing use cases and technologies that leverages concepts such as TinyML, FGPAs and concepts of orchestration. Glaðsheimr will also be develop tooling (Mjolnir) to allow application developers to design, build and orchestrate applications.
What is Orchestration?
Orchestration is the automatic process of managing or scheduling the work of individual components (models, sensors, frontend) within multiple devices. Orchestration automates such things as configuration, availability, provisioning and health monitoring of the application.
Orchestration is a common concept in web development (with projects such as Kubernetes) although the scope for orchestration in Mjölnir.
Proof Of Concepts
- Vatn: Does your water intake increases morning energy?
- Water tracking: Audio signals based on poured water
- Person energy: Time spent in bed tracked with human presence or sleep tracking
- Integration using only bluetooth mesh protocols
- Another concept is built around exploring metabolic syndrome
Contributors
What’s with the names?
I am just a geek who loves mythos and lately I have been reading old norse mythos and poems.
- Glaðsheimr Is the realm in which Odin’s hall of Valhalla
- Mjölnir Though most famous for its use as a weapon, Mjolnir played a vital role in Norse religious practices and rituals.
- Vatn Old norse word for water