A low-level functional langugae

For exploring refinement types and lifetime inference

Ante is in active development

Ante is currently in active development and the compiler is in a very early state. In addition, the features listed on this website detail the language itself rather than the subset that is implemented by the current compiler. If you are interested to see which features are implemented, please look at the github page linked below. Otherwise, if you just want to see the current design of the language, check out the language tour.

Factorial

fact x =
    if x == 0 then 1
    else x * fact (x - 1)

print (fact 5) //=> 120

Iterators

given Iterable iter string
parse_csv (text: iter) -> Vec (Vec string) =
    lines text
    |> skip 1
    |> map (split _ ",")
    |> collect

csv1 = parse_csv (File.open! "input.csv")
csv2 = parse_csv "a,b,c\n1,2,3\n4,5,6"

Type Inference

//A collection c of elements of type e
trait Collection c -> e with
    len: c -> usz
    get: (collection: c) (index: usz) -> e given index < len collection

trait Show t with
    to_string: t -> string

// Inferred type:
// elem_to_string: (c: a) (i: usz) -> string
//    given Collection a b, Show b, i < len c
elem_to_string c i =
    get c i |> to_string

Refinement Types

given len v1 == len v2
dotproduct (v1: Array u64) (v2: Array u64) -> u64 =
    // Sum the products of each element of both arrays
    products = map2 v1 v2 (*)
    sum products


dotproduct [1, 2, 3] [4, 5, 6] //=> 22
dotproduct [1, 2, 3] [4, 5]    //error: Failed to prove len [1,2,3] == len [4,5]

Lifetime Inference

type Person = job: string, name: ref string

// the data referenced via `&` should not be freed inside this function
make_person job =
    Person job &"bob"

// bob is only used at this scope, so it can be safely freed afterward
bob = make_person "programmer"

// unlike ownership systems, aliasing is allowed with lifetime inference
bob_twin = bob
assert (bob.name == bob_twin.name)

Goals

Ante aims to help bridge the gap between low-level languages like C++/Rust and higher level garbage-collected languages like Java, OCaml, or Haskell. Another key goal is experimentation with novel features like refinement type inference, always-incremental compilation, and lifetime inference.

Refinement Types

Refinement types can prevent bugs like array index out of bounds errors at compile-time. They can also be inferred to cut down on the number of annotations required.

Expressive

Common patterns like error handling and looping have syntax sugar to cut down on repetitive code while keeping things explicit.

Simple Module System

Ante’s module system mirrors the file tree and is easy to understand and easy to build as a result.

Always-Incremental Compilation

Incremental compilation metadata is distributed along with source code. This avoids the need for each user to rebuild most libraries or applications.

High & Low Level language

To try to bridge the gap between high and low level languages, ante adapts a high-level approach by default, maintaining the ability to drop into low-level code when needed.

Gradual Memory Management

Ante plans on using lifetime inference for temporary references to help simplify memory management. The design for this isn’t finalized yet though and is subject to change, beware!

The compiler is on GitHub

All are welcome to contribute!

github.com/jfecher/ante