Navigation Menu

Skip to content


Folders and files

Last commit message
Last commit date

Latest commit



54 Commits

Repository files navigation

Nazo ML (nml)

This is an experimental implementation of temporal-logic-based Hindley-Milner type system.

This is (currently) not for practical use.


In NML, technically, there are three temporal modal operators: Next(○), Finally(◇), and Globally(□).

The basic idea of NML's type system is that every non-temporal type is □-type.

This restriction makes it able to explicitly insert run when we want to "lift" ("fmap", or whatever) a function and then apply it to a delayed (quoted) term.

Non-formal explanation

Delayed term/type

(@ 1 @) has type Next[1] Nat, which means that we can obtain a Nat value at the next stage.

Also, <@ 1 @> has type Finally Nat, which means that we can obtain a Nat value at some stage in the future. So, Finally Nat essentially means Next[inf] Nat.

Lifted let expression

let-next x = (@ 1 @) in
if eq x 0 then

is the equivalent of

let x = (@ 1 @) in
  if eq (run[1] x) 0 then

, delays the computation, and thus has type Next[1] Bool.


let-finally x = <@ 1 @> in x + 1

is the equivalent of

let x = <@ 1 @> in <@ (run[inf] x) + 1 @>

and has type Finally Nat.

Useful example: I/O

The classical "scan" function can be thought as a function that returns a delayed value.

> readNat;;
type: Unit -> Next[1] Nat

Now we can use this like:

let-next x = readNat () in
let-next y = readNat () in
let-next z = readNat () in
(x + y) * z

Subtyping by stage

In NML, there is a built-in subtyping relation based on stage:

a <: Next[1] a <: Next[2] a <: ... <: Next[inf] a = Finally a

This means that, for example, a function with type Finally a -> b can also be applied to a value with type Next[n] a for any n, including 0 (= a).

See further example below:

subtyping example

NML and real-world linearity

The execution of a NML program is defined as

eval :: Next[n] a -> a (for any n in [0,inf])
eval program = run[inf] program

Each computation in each stage is kept pure functional:

  • Everything impure will be done between discrete time stages.
  • Once the stage is successfully transited, the computation at the current stage will certainly finite.

This ensures the linearity of the whole execution, while

  • allowing non-strict evaluation inside stages (because they are pure): lazy evaluation and even partial evaluation
  • not relying on specific compiler magics (such as RealWorld in GHC)

Also, it should be doable to express parallel computation in this type system as

parallel :: List (Finally a) -> Finally (List a)

, and I'm currently investigating it.


Practical things

  • Polymorphism
    • Let expressions
    • Type operators (eg. tuples)
    • Forall quantifier
  • Variants
    • With type parameters
  • Inductive data types (extends variant types)
    • Well-founded recursive functions (fixpoint)
  • Pattern matching (match)
    • Exhaustiveness check
    • Matching functions (function)
  • Operators
    • Operator definitions (let (+) l r = ...)
    • Use as a function
  • Top-level expressions
    • Let/Do expressions
    • Type definitions
    • Define/Open modules
    • On REPL

Type system extensions

  • Next(○) type operator (Next[1] T)
    • Code quotation ((@ t @))
    • Lifted let expression (let-next)
    • Macros (macro)
  • Dependent types
    • Length-dependent List
    • Compile-time type generation
  • Refinement types
    • Assertions
  • Finally(◇) type operator (Finally T, <@ t @>, let-finally)
    • Infinite recursive functions
    • Asynchronous computation

Runtime improvements

  • REPL
    • Line editor
    • Suggestions & completions
    • Load and execute source files
    • Import sources on the fly
  • Compiler
  • Interop
    • Built-in functions written in F#
    • Call .NET methods directly


GPL v3


Nazo ML - my toy programming language







No packages published