blob: 435bdcbbec1a4ed4b45b695a632241eb96ef502a (
plain)
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
|
Explanation: The Dhall programming language does not allow functions from terms
to types. These function types are also known as "dependent function types"
because you have a type whose value "depends" on the value of a term.
For example, this is $_NOT a legal function type:
┌─────────────┐
│ Bool → Type │
└─────────────┘
Similarly, this is $_NOT legal code:
┌────────────────────────────────────────────────────┐
│ λ(Vector : Natural → Type → Type) → Vector +0 Text │
└────────────────────────────────────────────────────┘
⇧
Invalid dependent type
Your function type is invalid because the input has type:
↳ $txt0
... and the output has kind:
↳ $txt1
... which makes this a forbidden dependent function type
|
