-
Notifications
You must be signed in to change notification settings - Fork 2
/
typtyp.typ
200 lines (184 loc) · 6.05 KB
/
typtyp.typ
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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
// TypTyp
// Type assertions library for Typst
//
// by Neven Villani [email protected]
//
// The purpose of this library is to provide easy type annotations
// (or to be more precise: field requirements) for Typst objects.
//
// Example usage:
//
// ```
// #import "typtyp.typ"
// #let tt = typtyp
//
// #let Person = tt.typedef(tt.struct(
// name: tt.str,
// age: tt.int,
// ))
//
// #let jack = tt.ret(Person, ( name: "Jack", age: 31 ))
// #let jane = ( name: "Jill", age: 22, gender: "W" )
// #tt.is(Person, jane) // assertion error: field 'gender' not part of 'Person'
// ```
//
// The general way that this is implemented for easy composition is that a
// type can be seen a function `any -> bool` that returns `true` iff the object
// has the right type.
// In reality, mostly for diagnostics purposes
// - instead of a boolean, the output is either `()` or an `( err: "Error message" )`
// - a type isn't actually just a `any -> bool` but a `( fn: any -> bool, label: str )`
//
// Note that typechecking is naive and may be costly on large datasets.
// Improvements will be designed if necessary.
#let has_type_of(t) = (obj) => {
if type(t) == type(obj) {
()
} else {
(
err: "Object " + repr(obj) + " does not have the right type: expected " + str(type(t)) + ", got " + str(type(obj)) + ".",
)
}
}
#let result_join_array(arr, fn) = {
let curr = ()
for new in arr {
if curr != () { return curr }
curr = fn(new)
}
curr
}
#let result_join_dict(map, fn) = {
let curr = ()
for (k, v) in map {
if curr != () { return curr }
curr = fn(k, v)
}
curr
}
#let typing_assert(r) = { if r != () { panic(r.err) } }
#let verify(t, o) = { typing_assert((t.fn)(o)); [ ok #o \ ] }
#let falsify(t, o) = { assert((t.fn)(o) != ()); [ #{ (t.fn)(o).err } \ ] }
#let typedef(name, t) = {
if type((:)) == type(t) {
( label: name, fn: t.fn )
} else {
( label: name, fn: t )
}
}
#let is(t, o) = typing_assert((t.fn)(o))
#let ret(t, o) = { is(t, o); o }
// Basic types
#let any = typedef("any", (_) => ())
#let never = typedef("never", (_) => ( err: "There are no instances of the nevertype" ))
#let bool = typedef("bool", has_type_of(true))
#let int = typedef("int", has_type_of(0))
#let color = typedef("color", has_type_of(rgb(0, 0, 0)))
#let str = typedef("str", has_type_of(""))
#let content = typedef("content", has_type_of([]))
#let null = typedef("none", has_type_of(none))
#verify(any, 1)
#verify(any, true)
#falsify(never, true)
#verify(color, rgb(1, 1, 1))
#verify(bool, false)
#falsify(bool, "")
#verify(null, none)
// Composition mechanisms
// Union types
#let union(..ts) = typedef("union { ... }", obj => {
let ts = ts.pos()
ts.fold(
( err: "None of " + ts.map(t => t.label).join(", ") + " match " + repr(obj) ),
(old, add) =>
if old == () or (add.fn)(obj) == () {
()
} else {
old
},
)
})
#verify(union(bool, int), 1)
#verify(union(bool, int), true)
#falsify(union(str, int), true)
#let option(t) = typedef(t.label + "?", union(t, null))
// Products
#let array(t) = typedef("array { ... }", arr => {
let old = has_type_of(())(arr)
if old != () { old } else { result_join_array(arr, t.fn) }
})
#verify(array(bool), (true, false, true))
#falsify(array(bool), (true, 1, true))
#verify(array(union(int, bool)), (true, 1, true))
#falsify(array(union(int, bool)), (true, 1, "foo"))
#falsify(array(array(bool)), (((true,), (true)), ((true,), (true))))
#falsify(array(array(array(bool))), (((true,), (true)), ((true,), (true))))
#verify(array(array(array(bool))), (((true,), (true,)), ((true,), (true,))))
// Test nesting
// We don't have much room in terms of maximum recursion limit, so ensuring
// that our typechecking assertions don't consume too much function depth
// is actually relevant.
#let nested(n, node, leaf) = {
if n <= 0 { leaf } else { node(nested(n - 1, node, leaf)) }
}
#{ let n = 30; verify(nested(n, array, bool), nested(n, x => (x,), true)) }
#let contains_field(map, field) = { map.at(field, default: none) == map.at(field, default: 1) }
#let struct(..args) = typedef("struct { ... }", obj => {
// Needs to be positional XOR named arguments
let map = args.named()
let tup = args.pos()
if type((:)) == type(obj) {
// Check that the type is a dictionnary with the right fields
// This simply consists of
// - checking that all keys in the type exist in the object and, these recursively match
// - checking that all keys in the object are declared in the type
let pre = result_join_dict(
map, (field, ft) => {
if not contains_field(obj, field) {
( err: "Should have field " + repr(field) )
} else {
(ft.fn)(obj.at(field))
}
}
)
if pre != () { return pre }
result_join_dict(
obj, (field, _) => {
if not contains_field(map, field) {
( err: "No such field " + repr(field) )
} else {
()
}
},
)
} else if type(()) == type(obj) {
// Check that the type is a tuple with the right fields
// I.e. lengths match, and the types/values match 1-1 (zip them together)
if tup.len() == obj.len() {
result_join_array(
tup.zip(obj), (vs) => {
let (t, v) = vs;
(t.fn)(v)
}
)
} else { ( err: "Mismatched lengths" ) }
} else { ( err: "Object is not a dictionnary or an array" ) }
})
#verify(struct(foo: str, bar: int, baz: bool), (foo: "abc", bar: 1, baz: false))
#falsify(struct(foo: str, bar: int, baz: bool), (foo: "abc", bar: 1))
#falsify(struct(foo: str, baz: bool), (foo: "abc", bar: 1, baz: false))
#verify(struct(int, bool, str), (1, true, "foo"))
#{ let n = 20; verify(nested(n, x => struct(foo: x), bool), nested(n, x => (foo: x), true)) }
// Demo
#let Person = typedef("Person", struct(age: int, name: str))
#let jack = ( age: 31, name: "Jack" )
#is(Person, jack)
#let Pair(T, U) = typedef("Pair", struct(T, U))
#let swap = (T, U) => (tup) => {
is(Pair(T, U), tup)
let (t, u) = tup
ret(Pair(U, T), (u, t))
}
#let thing = (42, "foobar")
#is(Pair(int, str), thing)
#is(Pair(str, int), swap(int, str)(thing))