1# The Type System
2
3Silo is a statically typed language, and its type system carries
4more load than most. A Silo function's signature can tell you what
5it pops, what it pushes, what side effects it might have, what
6structural constraints it places on its inputs, and — if the types
7track length — how the size of its output relates to the size of
8its input.
9
10This chapter introduces the type-level vocabulary in layers. Each
11layer is independently useful; you can stop at any point and still
12write productive Silo.
13
141. :gloss[Stack effects](./A1-glossary.simd#stack-effect) are the type
15 signatures.
162. Type variables (lowercase) and concrete types (uppercase).
173. Type application — `(Vec Int | 3)`.
184. :gloss[Constraint blocks](./A1-glossary.simd#constraint-block) —
19 `{ (Ord a) }`.
205. :gloss[Dependent types](./A1-glossary.simd#dependent-type) — types
21 parameterised by values.
226. Type-level arithmetic.
237. :gloss[Higher-kinded types](./A1-glossary.simd#higher-kinded-type-hkt).
24
25## Stack effects are the signatures
26
27Every word declares its type with a stack effect:
28
29```silo
30:fn swap-em ( a b -> b a )
31 pop-> second pop-> first
32 second first
33:end
34```
35
36The signature on its own tells you what the word does to the stack.
37Here, two values are swapped: the deeper `a` becomes the top, the
38top `b` goes beneath.
39
40The compiler reads a stack effect the same way a Rust compiler reads
41a function signature — as a contract that the body must satisfy. If
42the body of `swap-em` left only one value on the stack, or left them
43in the original order, the program would not compile.
44
45Stack effects can carry effects on the right-hand side
46(`( Str -> ) +Console`) and trait constraints in a following
47`{ … }` block (`( a a -> a ) { (Ord a) }`). Both are covered below.
48
49## Type variables and concrete types
50
51Silo uses case to distinguish a **type variable** from a **concrete
52type**. Lowercase names like `a`, `b`, `elem`, `n` are universally
53quantified — they stand for "any type" at the call site. Uppercase
54names like `Int`, `Str`, `F64`, `Vec` refer to specific types.
55
56```silo
57:fn id ( a -> a ) # works for any a
58 #( the body is empty; the stack shape (a -> a) is already
59 satisfied by doing nothing. )#
60:end
61
62:fn double-int ( Int -> Int ) # only Int
63 2 *
64:end
65```
66
67Calling `id` with an `Int` produces an `Int`; calling it with a
68`Str` produces a `Str`. The caller's types flow through. This is
69the same parametric polymorphism you find in Rust generics or ML
70type variables — Silo just writes the parameters in lowercase
71rather than angle-brackets.
72
73## Type application
74
75Some types take parameters. You apply a type to its parameters with
76parentheses, head-first:
77
78```silo
79(Vec Int | 3) # a Vec of 3 Ints
80(Option Str) # an optional Str
81(Result Int Str) # either Ok(Int) or Err(Str)
82(HashMap Str Int) # a map from Str to Int
83```
84
85This is the same shape as calling a word: the head is the type
86constructor, the arguments follow. The arity is checked by the
87compiler — passing too many is an error (`(Vec Int | 3 4)`
88wouldn't compile).
89
90### Primary vs associated parameters
91
92Types can split their parameters with a `|` wall, the same
93way traits do (see
94[chapter 9](./09-traits.simd#primary-parameters-vs-associated-types)).
95Parameters **before** the `|` are primary — the caller always
96supplies them. Parameters **after** the `|` are **associated**
97— the impl determines them, and at use sites they can be
98elided entirely.
99
100`Vec` is the canonical example. Its declaration pins `size`
101as associated:
102
103```silo
104@lang(vec)
105:impl (Vec elem | size) ... :end
106```
107
108At use sites either form is valid:
109
110```silo
111(Vec Int) # size is associated; left free / inferred
112(Vec Int | 3) # size pinned to 3
113```
114
115`(Vec Int)` is the **existential-length** form — equivalent
116to `(Vec Int | n)` with a fresh `n` — and is what most library
117signatures use when the length doesn't matter. `(Vec Int | 3)`
118is the length-indexed form when you need to commit to a
119specific size.
120
121Type applications nest. Any argument slot can itself be an applied
122type, so you can write arbitrarily deep shapes:
123
124```silo
125(Vec (Pair (Option a) (Result t e)))
126```
127
128Reading that outside-in: a `Vec` whose element type is a `Pair`
129whose first component is an `(Option a)` and whose second is a
130`(Result t e)`. There's no limit on nesting depth, and there are no
131special rules at the boundary between constructors — each pair of
132parentheses applies its head to its arguments in the same way.
133
134## Unit and Never
135
136Two special primitive types bracket the spectrum.
137
138**:gloss[Unit](./A1-glossary.simd#unit)** is a type with exactly one
139value, written `unit`. The intrinsic word `unit` has signature
140`( -> Unit )` — it pushes that single value onto the stack, where
141it occupies a slot like any other value.
142
143An empty output side in a stack effect — `( Str -> )` — is **not**
144the same as `( Str -> Unit )`. The first produces zero stack slots;
145the second produces one, holding `unit`. Most side-effectful words
146use the empty form: `print` is `( Str -> ) +Console`, not
147`( Str -> Unit ) +Console`.
148
149`Unit` earns its keep in generic contexts. `(Result Unit Str)` is
150a fallible operation whose success case doesn't carry data but
151still has to fit a `Result`-shaped type. `(Option Unit)` collapses
152to a presence-or-absence tag. Without a single-value type, every
153generic that wanted to convey "nothing" would need an ad-hoc
154workaround.
155
156**:gloss[Never](./A1-glossary.simd#never)** sits at the other extreme: a
157type with *no* values at all — the **bottom type**. An expression
158of type `Never` is one that provably doesn't return. Standard
159examples are `panic` and `.exit`:
160
161```silo
162:fn panic ( err -> Never ) +(Panic err) ...
163```
164
165Since `Never` has no values, a `Never`-typed expression coerces to
166any type — the coercion is vacuous, because there is no value to
167actually convert. That is how code after `panic` continues to type
168check in whatever context it appears in.
169
170`Never` becomes particularly interesting when it appears inside a
171generic type. `(Option Never)` has effectively only the `None`
172variant, because `Some(Never)` would require producing a `Never`
173value. [Chapter 8](./08-pattern-matching.simd) develops the
174resulting type-level isomorphisms.
175
176## Constraint blocks
177
178To write a generic word that needs a specific capability on its
179type parameters, add a constraint block in curly braces after the
180stack effect. Each clause is a trait applied to one or more type
181variables:
182
183```silo
184:fn maximum ( a a -> a ) { (Ord a) }
185 pop-> b pop-> a
186 a b > :if a :else b :end
187:end
188```
189
190`{ (Ord a) }` reads "`a` must implement `Ord`". Inside the body,
191you can use any `Ord` method on an `a`. Multiple constraints stack
192up with whitespace separation:
193
194```silo
195:fn hash-and-show ( a -> AnyInt Str )
196 { (Hash a) (Display a) }
197 peek-> x
198 x .hash swap x "{}" format
199:end
200```
201
202The Rust analogue is the `where` clause:
203
204```rust
205fn maximum<A>(x: A, y: A) -> A where A: Ord { … }
206```
207
208Constraint blocks are one of Silo's two ways to restrict what types
209can flow through a generic word. The other is
210:gloss[predicates](./A1-glossary.simd#predicate), introduced in
211[chapter 5](./05-data.simd#predicates). Traits are for dispatch
212(different code per type); predicates are for gatekeeping
213(different types allowed at different call sites).
214
215## Dependent types
216
217Silo is **dependently typed**, which means types can take *values*
218as arguments, not only other types. The classic example is a Vec
219whose length is in its type:
220
221```silo
222(Vec Int | 3) # a Vec of exactly three Ints
223(Vec Str | n) # a Vec of n Strs, n is a variable
224```
225
226The `3` and the `n` above are values — integers, in this case —
227occupying what would otherwise be a type slot. When two Vecs have
228different type-level lengths, the compiler knows their types are
229different.
230
231Range-refined integers work the same way:
232
233```silo
234:type Port (Int 0..2^16)
235```
236
237`(Int 0..2^16)` is the type of integers in the half-open range
238`[0, 65536)`. Calling a function that expects a `Port` with any
239integer outside that range is a compile error. To go from a plain
240integer to a `Port`, you use the fallible `.try-from`:
241
242```silo
24380 (Port .try-from) # ⌊Ok(Port(80))⌉
244100000 (Port .try-from) # ⌊Err("out of range")⌉
245```
246
247You can treat dependent types at two levels. Most of the time you
248rely on the standard library using them internally — `Vec.append`
249knows the length of the result because it knows the lengths of its
250inputs, and that propagates automatically. When you do want to
251reach for them yourself, the mechanism is the same: put a value in
252a type-parameter slot.
253
254If "dependently typed" sounds alarming: in practice, it is almost
255always invisible. You don't write proofs, you don't annotate
256lengths, you don't wrestle with dependent pattern matches. The
257language is doing the bookkeeping in the background so that common
258invariants hold mechanically.
259
260## Type-level arithmetic
261
262Because values live in the types, you need arithmetic at the type
263level. Silo writes it in the same postfix style as ordinary code,
264inside parentheses:
265
266```silo
267(n 1 +) # n plus 1
268(n 2 *) # n times 2
269(n m +) # sum of two type variables
270```
271
272These are most useful on signatures that describe how a word's
273output length relates to its input length:
274
275```silo
276:fn .append ( (Vec a | n) (Vec a | m) -> (Vec a | (n m +)) )
277 { (AnyUInt n) (AnyUInt m) }
278 ...
279:end
280```
281
282The result type `(Vec a | (n m +))` encodes "a Vec of length n plus
283m". The `{ (AnyUInt n) (AnyUInt m) }` constraint says both lengths
284must be non-negative integers (values of kind `AnyUInt`). Together,
285you can chain `.append` calls and the compiler will track the
286cumulative length through the whole pipeline.
287
288## Higher-kinded types
289
290A type variable can stand for any type. A
291**:gloss[higher-kinded type](./A1-glossary.simd#higher-kinded-type-hkt)**
292(HKT) variable stands for any *type constructor* — something that
293itself takes parameters.
294
295In Silo, an HKT is just a type variable applied to more arguments.
296Here's a trait parameterised over a container type `f`:
297
298```silo
299:trait Mappable f mapped { (Foldable f) }
300 .map ( (f a) [a -> b] -> (mapped b) )
301:end
302```
303
304Read this as: a type `f` is `Mappable` into `mapped` if, given an
305`(f a)` and a function `a -> b`, you can produce a `(mapped b)`.
306`f` ranges over containers — `Vec`, `Option`, `HashMap`, and so on
307— not over concrete types like `Int`.
308
309HKTs are the reason `.map` works uniformly across every Silo
310container. Rust doesn't have them; the closest Haskell analogue is
311Functor, which is exactly this trait at a higher level of
312abstraction. If you've written Haskell, `Mappable` is just
313`Functor` specialised for the stack-based shape.
314
315You won't often write HKT-quantified traits yourself, but you'll
316see them throughout the standard library. Knowing the syntax is
317enough to read what's there.
318
319## How the checker actually works
320
321Silo's type checker uses **forward propagation**: it walks through
322each word's body from the start, tracking the stack's type at every
323point, and checks that every call matches the declared stack
324effect. Any mismatch becomes a compile error pointing at the
325specific word where the stack shape diverged from what the next
326caller expected.
327
328This is different from ML-style Hindley-Milner inference, which
329gathers constraints across the whole program and solves them
330globally. Forward propagation is simpler and gives more localised
331error messages — the error appears where the mistake is, not at
332some other place the constraint bubbled up to. It's also what lets
333Silo check dependent types without a proof-assistant-grade solver:
334the compiler always knows concretely what's on the stack at each
335point.
336
337## Key points
338
339- Stack effects serve as type signatures. Lowercase names are
340 universally quantified variables; uppercase names are concrete
341 types.
342- Type application is parenthesised and head-first:
343 `(Vec Int | 3)`, `(Option Str)`.
344- `{ (Trait x) … }` after a signature is a
345 :gloss[constraint block](./A1-glossary.simd#constraint-block): trait
346 bounds on the word's type variables.
347- Types can take *values* as parameters. `(Vec elem | n)` tracks the
348 length in the type; `(Int 0..256)` is a refinement type.
349- Type-level arithmetic is postfix: `(n 1 +)`, `(n m +)`. Use it
350 in signatures where an output length relates to an input length.
351- An HKT variable stands for a type constructor. That's how
352 `Mappable`, `Foldable`, and the rest of Silo's generic
353 traversals are uniform across every container type.
354- The compiler uses
355 :gloss[forward propagation](./A1-glossary.simd#forward-propagation)
356 rather than global inference. Errors localise to where the
357 mistake was made.
358
359The next chapter covers
360[numerics](./07-numerics.simd) — the four numeric representations
361and the arithmetic-variant operators that prevent silent overflow.