1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
-- | Simple functional combinators.
-- | Left-to-right application. Particularly useful for describing
-- computation pipelines:
--
-- ```
-- x |> f |> g |> h
-- ```
def (|>) '^a '^b (x: a) (f: a -> b) : b = f x
-- | Right to left application.
--
-- Due to the causality restriction (see the language reference) this
-- is less useful than `|>`@term. For example, the following is
-- a type error:
--
-- ```
-- length <| filter (>0) [-1,0,1]
-- ```
--
-- But this works:
--
-- ```
-- filter (>0) [-1,0,1] |> length
-- ```
def (<|) '^a '^b (f: a -> b) (x: a) = f x
-- | Function composition, with values flowing from left to right.
--
-- Note that functions with anonymous return sizes cannot be composed.
-- For example, the following is a type error:
--
-- ```
-- filter (>0) >-> length
-- ```
--
-- In such cases you can use the pipe operator `|>`@term instead.
def (>->) '^a '^b '^c (f: a -> b) (g: b -> c) (x: a) : c = g (f x)
-- | Function composition, with values flowing from right to left.
-- This is the same as the `∘` operator known from mathematics.
--
-- Has the same restrictions with respect to anonymous sizes as
-- `>->`@term.
def (<-<) '^a '^b '^c (g: b -> c) (f: a -> b) (x: a) : c = g (f x)
-- | Flip the arguments passed to a function.
--
-- ```
-- f x y == flip f y x
-- ```
def flip '^a '^b '^c (f: a -> b -> c) (b: b) (a: a) : c =
f a b
-- | Transform a function taking a pair into a function taking two
-- arguments.
def curry '^a '^b '^c (f: (a, b) -> c) (a: a) (b: b) : c =
f (a, b)
-- | Transform a function taking two arguments in a function taking a
-- pair.
def uncurry '^a '^b '^c (f: a -> b -> c) (a: a, b: b) : c =
f a b
-- | The constant function.
def const '^a '^b (x: a) (_: b) : a = x
-- | The identity function.
def id '^a (x: a) = x
-- | Apply a function some number of times.
def iterate 'a (n: i32) (f: a -> a) (x: a) =
loop x for _i < n do f x
-- | Keep applying `f` until `p` returns true for the input value.
-- May apply zero times. *Note*: may not terminate.
def iterate_until 'a (p: a -> bool) (f: a -> a) (x: a) =
loop x while !(p x) do f x
-- | Keep applying `f` while `p` returns true for the input value.
-- May apply zero times. *Note*: may not terminate.
def iterate_while 'a (p: a -> bool) (f: a -> a) (x: a) =
loop x while p x do f x
|
