dotproduct (v1: Array U64) (v2: Array U64 where 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]   //=> 32
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 with
    flip: Unit -> Bool

calculation () =
    if flip () then
        unused = flip ()
        if flip () then 0.5
        else 4.0
    else 1.0

expected_value (f: Unit -> F64 can Flip): F64 =
    handle f ()
    | flip () -> (resume true + resume false) / 2.0

print (expected_value calculation) //=> 1.625

Index array = x:Usz where 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
//    with 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)

parse_csv (text: it) -> Vec (Vec String) with Iterator it 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"