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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
Explanation: Every function declares what type or kind of argument to accept
For example:
┌───────────────────────────────┐
│ λ(x : Bool) → x : Bool → Bool │ This anonymous function only accepts
└───────────────────────────────┘ arguments that have type ❰Bool❱
⇧
The function's input type
┌───────────────────────────────┐
│ Natural/even : Natural → Bool │ This built-in function only accepts
└───────────────────────────────┘ arguments that have type ❰Natural❱
⇧
The function's input type
┌───────────────────────────────┐
│ λ(a : Type) → a : Type → Type │ This anonymous function only accepts
└───────────────────────────────┘ arguments that have kind ❰Type❱
⇧
The function's input kind
┌────────────────────┐
│ List : Type → Type │ This built-in function only accepts arguments that
└────────────────────┘ have kind ❰Type❱
⇧
The function's input kind
For example, the following expressions are valid:
┌────────────────────────┐
│ (λ(x : Bool) → x) True │ ❰True❱ has type ❰Bool❱, which matches the type
└────────────────────────┘ of argument that the anonymous function accepts
┌─────────────────┐
│ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of
└─────────────────┘ argument that the ❰Natural/even❱ function accepts,
┌────────────────────────┐
│ (λ(a : Type) → a) Bool │ ❰Bool❱ has kind ❰Type❱, which matches the kind
└────────────────────────┘ of argument that the anonymous function accepts
┌───────────┐
│ List Text │ ❰Text❱ has kind ❰Type❱, which matches the kind of argument
└───────────┘ that that the ❰List❱ function accepts
However, you can $_NOT apply a function to the wrong type or kind of argument
For example, the following expressions are not valid:
┌───────────────────────┐
│ (λ(x : Bool) → x) "A" │ ❰"A"❱ has type ❰Text❱, but the anonymous function
└───────────────────────┘ expects an argument that has type ❰Bool❱
┌──────────────────┐
│ Natural/even "A" │ ❰"A"❱ has type ❰Text❱, but the ❰Natural/even❱ function
└──────────────────┘ expects an argument that has type ❰Natural❱
┌────────────────────────┐
│ (λ(a : Type) → a) True │ ❰True❱ has type ❰Bool❱, but the anonymous
└────────────────────────┘ function expects an argument of kind ❰Type❱
┌────────┐
│ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an
└────────┘ argument that has kind ❰Type❱
You tried to invoke the following function:
↳ $txt0
... which expects an argument of type or kind:
↳ $txt1
... on the following argument:
↳ $txt2
... which has a different type or kind:
↳ $txt3
Some common reasons why you might get this error:
● You omit a function argument by mistake:
┌────────────────────────────────────────┐
│ List/head ([1, 2, 3] : List Integer) │
└────────────────────────────────────────┘
⇧
❰List/head❱ is missing the first argument,
which should be: ❰Integer❱
● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱
┌────────────────┐
│ Natural/even 2 │
└────────────────┘
⇧
This should be ❰+2❱
|
