One language for everything

// the answer, computed the long way
fn double(x: i32) -> i32 {
    x + x
}

fn main() {
    let mut sum = 0;
    for i in 0..7 {
        sum += i;
    }
    println!("{}", double(sum)); // 42
}

// the answer, computed the long way
const std = @import("std");

fn double(x: i32) i32 {
    return x + x;
}

pub fn main() void {
    var sum: i32 = 0;
    var i: i32 = 0;
    while (i < 7) : (i += 1) sum += i;
    std.debug.print("{d}\n", .{double(sum)}); // 42
}

// the answer, computed the long way
#include <stdio.h>

/* double is a keyword, so: */
int twice(int x) { return x + x; }

int main(void) {
    int sum = 0;
    for (int i = 0; i < 7; i++) sum += i;
    printf("%d\n", twice(sum)); /* 42 */
    return 0;
}

# the answer, computed the long way
def double(x: int) -> int:
    return x + x

total = 0
for i in range(7):
    total += i
print(double(total))  # 42

// the answer, computed the long way
const double = (x: number): number => x + x;

let sum = 0;
for (let i = 0; i < 7; i++) sum += i;
console.log(double(sum)); // 42

;; the answer, computed the long way
#lang racket

(define (double x) (+ x x))

(define sum
  (for/sum ([i (in-range 7)]) i))
(displayln (double sum)) ; 42

-- the answer, computed the long way
def double (x : Int) : Int := x + x

def main : IO Unit := do
  let mut sum : Int := 0
  for i in [0:7] do
    sum := sum + i
  IO.println (double sum) -- 42

lacking: 0.1 is a float; no exact rational in std

// a literal is a float from the start; no exact
// rational in the language or its standard library
fn main() {
    println!("{}", 0.1 + 0.2 == 0.3); // false
}

lacking: no exact literals, not even at compile time

// a literal is a float from the start, even at
// compile time, where it is an f128
const std = @import("std");

pub fn main() void {
    // false
    std.debug.print("{}\n", .{0.1 + 0.2 == 0.3});
}

lacking: no exact literals; 0.1 is a double

// a literal is a double from the start
#include <stdio.h>

int main(void) {
    printf("%d\n", 0.1 + 0.2 == 0.3); /* 0: false */
    return 0;
}

lacking: 0.1 is a float; exact needs Fraction and a string

# a literal is a float; exactness is a library type
from fractions import Fraction as F

print(0.1 + 0.2 == 0.3)                 # False
print(F("0.1") + F("0.2") == F("0.3"))  # True

lacking: no exact literals; 0.1 is a double

// a literal is a double from the start
console.log(0.1 + 0.2 === 0.3); // false

;; a decimal literal is inexact unless marked #e,
;; which makes it an exact rational
#lang racket
(displayln (= (+ 0.1 0.2) 0.3))        ; #f
(displayln (= (+ #e0.1 #e0.2) #e0.3))  ; #t

-- a Float literal rounds; as a ℚ it is exact
import Mathlib

#eval (0.1 : Float) + 0.2 == 0.3  -- false
example : (0.1 : ℚ) + 0.2 = 0.3 := by norm_num

not supported

// a function can return a type, run at compile time
const std = @import("std");

fn pick(i: u8) type {
    return if (i == 0) i32 else f64;
}

pub fn main() void {
    const a: pick(1) = 9.9; // a is an f64
    const same = pick(0) == i32;
    std.debug.print("{d} {}\n", .{ a, same });
}

not supported

# types are values, so a function can return one,
# though nothing checks what is then done with it
def pick(i: int) -> type:
    return int if i == 0 else float

a = pick(1)(9.9)       # an ordinary float
print(pick(0) is int)  # True

not supported

not supported

-- a definition can return a type; types are terms
def pick (i : Nat) : Type :=
  if i = 0 then Int else Float

def a : pick 1 := (9.9 : Float) -- a is a Float
example : pick 0 = Int := rfl

not supported

not supported

not supported

not supported

not supported

not supported

not supported

// a Box owns its heap value and frees it when the
// owner goes out of scope; a move hands that duty on
fn main() {
    let a = Box::new(40);
    let b = a; // ownership moves to b; a is gone
    println!("{}", *b); // 40
}

not supported

not supported

not supported

not supported

not supported

not supported

// a move ends the name; a later use is a compile
// error, nothing waits for run time
fn main() {
    let a = Box::new(40);
    let b = a;
    println!("{}", *b); // 40
    println!("{}", *a); // error[E0382]: moved value
}

not supported

not supported

not supported

not supported

not supported

not supported

// a value's type has an identity at run time,
// though nothing more of it can be read back
use std::any::{Any, TypeId};

fn main() {
    let x: i32 = 5;
    let same = x.type_id() == TypeId::of::<i32>();
    let cross = x.type_id() == TypeId::of::<f64>();
    println!("{}", same && !cross); // true
}

// @TypeOf reads a type at compile time; types compare
// with ==
const std = @import("std");

pub fn main() void {
    const x: i32 = 5;
    const same = @TypeOf(x) == i32; // true
    const cross = @TypeOf(x) == f64; // false
    const meta = @TypeOf(i32) == type; // true
    const all = same and meta and !cross;
    std.debug.print("{}\n", .{all});
}

not supported

# types are objects, and `type` is its own type
x = 5

same = type(x) is int     # True
cross = type(x) is float  # False
meta = type(int) is type  # True
print(same and meta and not cross)

// typeof names a handful of run-time kinds; the
// static types themselves are gone by run time
const x = 5;

const same = typeof x === "number"; // true
const cross = typeof x === "string"; // false
console.log(same && !cross);

not supported

-- types are terms; a metaprogram reads a value's type
import Lean
open Lean Meta

def x : Int := 5

#eval show MetaM Bool from do
  let t ← inferType (mkConst ``x)
  return t == mkConst ``Int -- true

not supported

not supported

not supported

not supported

not supported

not supported

-- a theorem is a type and its proof a term the kernel
-- checks; the rewrites are the same steps
import Mathlib

theorem half (a : ℚ) (h : a ≠ 0) :
    (a + a) / a = 2 := by
  rw [← two_mul, mul_div_assoc, div_self h, mul_one]

#print axioms half -- the world it rests on

not supported

not supported

not supported

not supported

not supported

lacking: no precedence, one operator per parenthesis; the math is the built-in expt

;; a module can redefine application itself, so
;; (x ^ 3) reads the operator between its operands
#lang racket
(module infix racket
  (require (for-syntax syntax/parse))
  (provide (rename-out [app #%app])
           (except-out (all-from-out racket) #%app))
  (define-syntax (app stx)
    (syntax-parse stx
      [(_ lhs (~literal ^) rhs) #'(expt lhs rhs)]
      [(_ f x ...) #'(#%app f x ...)])))

(module main (submod ".." infix)
  (define (f x) (+ (x ^ 3) 1))
  (displayln (f 2))) ; 9, one operator per parenthesis

lacking: Int base and Nat exponent only: no floats, no negative or fractional exponent

-- a new operator is a notation, written in Lean and
-- used in the same file
def power (b : Int) : Nat → Int
  | 0 => 1
  | n + 1 => b * power b n

infixr:75 " ** " => power

def f (x : Int) : Int := x ** 3 + 1
#eval f 2 -- 9

not supported

lacking: parameters and return type only; the body cannot be read

// @typeInfo reads a function's parameters and return
// type at compile time; its body cannot be read
const std = @import("std");

fn power(b: i32, n: u32) i32 {
    var r: i32 = 1;
    for (0..n) |_| r *= b;
    return r;
}

pub fn main() void {
    const info = @typeInfo(@TypeOf(power)).@"fn";
    std.debug.print("{d} {s}\n", .{
        info.params.len,
        @typeName(info.return_type.?),
    });
}

not supported

lacking: source comes back as text and bytecode, not nodes; an expression runs before it can be read

# a function is an object: its signature, its source
# and its bytecode can all be read back
import inspect, dis

def power(b: int, n: int) -> int:
    return b ** n

print(inspect.signature(power))  # the signature
print(inspect.getsource(power))  # the source text
dis.dis(power)                   # the bytecode

lacking: name, arity and source text only; the types are erased

// a function is an object: its name, arity and source
// text can be read back; its types are erased
function power(b: number, n: number): number {
  return b ** n;
}

console.log(power.name, power.length); // power 2
console.log(power.toString());  // the source text

lacking: name and arity only; the body is gone once compiled

;; a procedure's name and arity can be read back;
;; its body cannot, once compiled
#lang racket

(define (power b n) (expt b n))

(displayln (object-name power))     ; power
(displayln (procedure-arity power)) ; 2

lacking: read only from a metaprogram, not by the running program

-- a definition is a term the environment holds, and a
-- metaprogram reads its type and its body back
import Lean
open Lean Meta

def power (b : Int) : Nat → Int
  | 0 => 1
  | n + 1 => b * power b n

#print power   -- the definition: its type and body
#eval show MetaM Expr from do
  return (← getConstInfo ``power).type

lacking: file and line only; no scope to read or walk up

// the spot a line is written at is text, not a scope:
// its file and line; nothing walks up from it
fn main() {
    println!("{}:{}", file!(), line!()); // file, line
}

lacking: file, line and the type around; the scopes above are not values

// @src() is the spot a line is written at and @This()
// the type around it; the scopes above are not values
const std = @import("std");

pub fn main() void {
    const here = @src();
    std.debug.print("{s}:{d}\n", .{
        here.file, here.line,
    });
}

lacking: file and line only; no scope to read or walk up

// the spot a line is written at is text, not a scope:
// its file and line; nothing walks up from it
#include <stdio.h>

int main(void) {
    printf("%s:%d\n", __FILE__, __LINE__);
    return 0;
}

lacking: call frames at run time; the lexical scopes are not values

# the call stack is reachable as frames at run time;
# the lexical scopes themselves are not values
import inspect

x = 1
def g():
    y = 2
    f = inspect.currentframe()
    print("y" in f.f_locals)         # True: here
    print("x" in f.f_back.f_locals)  # True: one up
g()

not supported

lacking: a namespace to look names up in; the scopes are not values

;; a namespace lists what a spot can name; the scopes
;; a line stands in are not values, hygiene keeps them
#lang racket
(define x 1)
(define-namespace-anchor here)
(define ns (namespace-anchor->namespace here))
(displayln (namespace-variable-value 'x #t #f ns)) ; 1

lacking: names in scope, only in a metaprogram; the scopes above are not values

-- inside a metaprogram, the local context is a value:
-- the names in scope, in order; nothing above them
import Lean
open Lean Elab Term

elab "names_here" : term => do
  let ns := (← getLCtx).decls.toList.filterMap
    (fun d => d.map (·.userName))
  logInfo m!"{ns}"
  return mkNatLit 0

def f (x y : Nat) : Nat := names_here -- [x, y]

lacking: prefix only; `4 twice` cannot be written

// a macro rewrites tokens, written in Rust and used
// in the same file; prefix only, never `4 twice`
macro_rules! twice {
    ($e:expr) => { $e * 2 };
}

fn main() {
    println!("{}", 3 + twice!(4)); // 11
}

not supported

lacking: prefix only; `4 TWICE` cannot be written

// a macro rewrites text before the compiler reads it;
// prefix only, never `4 TWICE`
#include <stdio.h>
#define TWICE(e) ((e) * 2)

int main(void) {
    printf("%d\n", 3 + TWICE(4)); /* 11 */
    return 0;
}

not supported

not supported

lacking: prefix only; `4 twice` cannot be written

;; a macro rewrites syntax, written in Racket and used
;; in the same file; prefix, as every form is a list
#lang racket
(define-syntax-rule (twice e) (* e 2))
(displayln (+ 3 (twice 4))) ; 11

-- a notation is a syntax rewrite, written in Lean and
-- used in the same file, postfix included
notation:70 x:70 " twice" => x * 2

#eval 3 + 4 twice -- 11

lacking: `Point::DIMS` cannot be read through a value

// a struct holds the fields; an associated const is
// read through the type only, never through a value
struct Point { x: i32, y: i32 }
impl Point { const DIMS: i32 = 2; }

fn main() {
    let p = Point { x: 1, y: 2 };
    println!("{} {}", p.x + p.y, Point::DIMS); // 3 2
}

lacking: `Point.dims` cannot be read through a value

// a struct is also a namespace: a decl inside it is
// read through the type, never through a value
const std = @import("std");

const Point = struct {
    x: i32,
    y: i32,
    const dims: i32 = 2;
};

pub fn main() void {
    const p = Point{ .x = 1, .y = 2 };
    std.debug.print("{d} {d}\n", .{p.x, Point.dims});
}

not supported

# a class is both: instance attributes and class
# attributes, the latter read through either
class Point:
    dims = 2
    def __init__(self, x, y):
        self.x, self.y = x, y

p = Point(1, 2)
print(p.x, Point.dims, p.dims)  # 1 2 2

lacking: `Point.dims` cannot be read through an instance

// a class holds fields; a static member is read
// through the class, not through an instance
class Point {
  static dims = 2;
  constructor(public x: number, public y: number) {}
}

const p = new Point(1, 2);
console.log(p.x, Point.dims); // 1 2

not supported

lacking: `Point.dims` cannot be read through a value

-- a structure holds the fields; a definition in its
-- namespace is read through the name, not a value
structure Point where
  x : Int
  y : Int

def Point.dims : Int := 2

def p : Point := ⟨1, 2⟩
#eval (p.x, Point.dims) -- (1, 2)