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] //=> 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 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"
Template by Bootstrapious. Ported to Hugo by DevCows.