Carml

A minimal ml-like language with secret annotations.

Example

let obfuscate msg: secret(string) -> string =
  let l: int = string_len msg in
  mk_string '*' l



let log msg: string -> unit = print msg
let log msg: secret(string) -> unit = print (obfuscate msg)

let main: unit =
  let token: secret(string) = load_secret_value () in
  log token;
  log "Loaded secret value"

Syntax

The program is a series of statements. Every let binding requires explicit type annotations (no type inference).

Statements

variable binding let ident: type = expression
function binding let ident params: type = expression
type declaration type ident = constructors

Literals

Simple literals

integers -- 1, 2, 11223344
booleans -- true, false
floats -- 1.234, 0.123
strings -- "hello, world"
characters -- 'a'
unit -- ()

Compound literals

tuples -- (a, b, c)
lists -- [a; b; c], a :: b :: c :: []
records -- A, B 1, C (B 1)

Types

Simple types

int
bool
float
string
char

Compound types

tuples -- A * B
functions -- A -> B
lists -- A list
secrets -- secret(A)

Expressions

binary expressions (as you would expect, > >= = < <= != !)
numeric expressions (as you would expect, + - * /)
list operators (@)
let-in binding -- let ident: type = expression in expression
sequencing -- expression; expression

Functions (closures)

fun params: type ->> expression A function expression uses a double-arrow (->>) to disambiguate the explicit type annotation, this will be removed when type inference is implemented. The function can take multiple parameters, separated by a space. See examples below:

fun a: int -> int ->> a + 1
fun a b: int -> int -> int ->> a + b

The top-level function statement is syntactic sugar for a variable-binding of a function expression.

let add1 a: int -> int = a + 1
let add1: int -> int = fun a: int -> int ->> a + 1

Function applications require explicit type annotations on arguments

let b: bool = (fun gt0 x: int -> bool ->> x > 0) (1: int)

Partial application is supported

let b: int -> bool = (fun gt a b: int -> int ->> a > b) (1: int)

Pattern matching

The match expression requires an explicit type annotation.

match (expression: type) with
| match_expression -> expression

Match expressions

_
a
(a, b)
a :: b
A
A 1
A (1, 2)

ssize-t/carml