dotproduct (v1: Array u64) (v2: Array u64 & len v1 == len v2) -> 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]

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 in region inference
bob_twin = bob
assert (bob.name == bob_twin.name)

// computing expected value from a function that takes a coin flip effect.
effect Flip: bool

calculation () =
    if do Flip then
        unused = do Flip
        if do Flip then 0.5
        else 4.0
    else 1.0

expected_value (f: unit -> f64 can Flip): f64 =
    handle f ()
    | Flip -> (continue true + continue false) / 2.0

print (expected_value calculation) //=> 1.625

Index array = x:usz & x < len array

//A collection c of elements of type e
trait Collection c -> e with
    len: c -> usz
    get: collection: c -> Index collection -> e

trait Show t with
    to_string: t -> string

// Inferred type:
// elem_to_string: collection:a -> Index collection -> string
//    given Collection a b, Show b
elem_to_string c i =
    get c i |> to_string

// Something can iterate if it implements next, returning either
// Some (next_iterator, current_element) or None to stop iterating 
trait Iterator it elem with
    next: it -> Maybe (it, elem)

given Iterator it string
parse_csv (text: it) -> 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"