Guide › The Silo Handbook › The Type System

Chapter 5 The Type System

Source

Silo is a statically typed language, and its type system carries more load than most. A Silo function's signature can tell you what it pops, what it pushes, what side effects it might have, what structural constraints it places on its inputs, and — if the types track length — how the size of its output relates to the size of its input.

This chapter introduces the type-level vocabulary in layers. Each layer is independently useful; you can stop at any point and still write productive Silo.

  1. (named block placeholder leaked into renderer — pair_named_blocks not run)
    signatures.
  2. Type variables (lowercase) and concrete types (uppercase).
  3. Type application — (Vec Int | 3).
  4. (named block placeholder leaked into renderer — pair_named_blocks not run)
    { (Ord a) }.
  5. (named block placeholder leaked into renderer — pair_named_blocks not run)
    parameterised by values.
  6. Type-level arithmetic.
  7. (named block placeholder leaked into renderer — pair_named_blocks not run)

Stack effects are the signatures

Every word declares its type with a stack effect:

:fn swap-em ( a b -> b a )
  pop-> second pop-> first
  second first
:end

The signature on its own tells you what the word does to the stack. Here, two values are swapped: the deeper a becomes the top, the top b goes beneath.

The compiler reads a stack effect the same way a Rust compiler reads a function signature — as a contract that the body must satisfy. If the body of swap-em left only one value on the stack, or left them in the original order, the program would not compile.

Stack effects can carry effects on the right-hand side (( Str -> ) +Console) and trait constraints in a following { … } block (( a a -> a ) { (Ord a) }). Both are covered below.

Type variables and concrete types

Silo uses case to distinguish a type variable from a concrete type. Lowercase names like a, b, elem, n are universally quantified — they stand for "any type" at the call site. Uppercase names like Int, Str, F64, Vec refer to specific types.

:fn id ( a -> a )              # works for any a
  #( the body is empty; the stack shape (a -> a) is already
     satisfied by doing nothing. )#
:end

:fn double-int ( Int -> Int )  # only Int
  2 *
:end

Calling id with an Int produces an Int; calling it with a Str produces a Str. The caller's types flow through. This is the same parametric polymorphism you find in Rust generics or ML type variables — Silo just writes the parameters in lowercase rather than angle-brackets.

Type application

Some types take parameters. You apply a type to its parameters with parentheses, head-first:

(Vec Int | 3)                    # a Vec of 3 Ints
(Option Str)                   # an optional Str
(Result Int Str)               # either Ok(Int) or Err(Str)
(HashMap Str Int)              # a map from Str to Int

This is the same shape as calling a word: the head is the type constructor, the arguments follow. The arity is checked by the compiler — passing too many is an error ((Vec Int | 3 4) wouldn't compile).

Primary vs associated parameters

Types can split their parameters with a | wall, the same way traits do (see chapter 9). Parameters before the | are primary — the caller always supplies them. Parameters after the | are associated — the impl determines them, and at use sites they can be elided entirely.

Vec is the canonical example. Its declaration pins size as associated:

@lang(vec)
:impl (Vec elem | size) ... :end

At use sites either form is valid:

(Vec Int)                      # size is associated; left free / inferred
(Vec Int | 3)                    # size pinned to 3

(Vec Int) is the existential-length form — equivalent to (Vec Int | n) with a fresh n — and is what most library signatures use when the length doesn't matter. (Vec Int | 3) is the length-indexed form when you need to commit to a specific size.

Type applications nest. Any argument slot can itself be an applied type, so you can write arbitrarily deep shapes:

(Vec (Pair (Option a) (Result t e)))

Reading that outside-in: a Vec whose element type is a Pair whose first component is an (Option a) and whose second is a (Result t e). There's no limit on nesting depth, and there are no special rules at the boundary between constructors — each pair of parentheses applies its head to its arguments in the same way.

Unit and Never

Two special primitive types bracket the spectrum.

Unit is a type with exactly one value, written unit. The intrinsic word unit has signature ( -> Unit ) — it pushes that single value onto the stack, where it occupies a slot like any other value.

An empty output side in a stack effect — ( Str -> ) — is not the same as ( Str -> Unit ). The first produces zero stack slots; the second produces one, holding unit. Most side-effectful words use the empty form: print is ( Str -> ) +Console, not ( Str -> Unit ) +Console.

Unit earns its keep in generic contexts. (Result Unit Str) is a fallible operation whose success case doesn't carry data but still has to fit a Result-shaped type. (Option Unit) collapses to a presence-or-absence tag. Without a single-value type, every generic that wanted to convey "nothing" would need an ad-hoc workaround.

Never sits at the other extreme: a type with no values at all — the bottom type. An expression of type Never is one that provably doesn't return. Standard examples are panic and .exit:

:fn panic ( err -> Never ) +(Panic err) ...

Since Never has no values, a Never-typed expression coerces to any type — the coercion is vacuous, because there is no value to actually convert. That is how code after panic continues to type check in whatever context it appears in.

Never becomes particularly interesting when it appears inside a generic type. (Option Never) has effectively only the None variant, because Some(Never) would require producing a Never value. Chapter 8 develops the resulting type-level isomorphisms.

Constraint blocks

To write a generic word that needs a specific capability on its type parameters, add a constraint block in curly braces after the stack effect. Each clause is a trait applied to one or more type variables:

:fn maximum ( a a -> a ) { (Ord a) }
  pop-> b pop-> a
  a b > :if a :else b :end
:end

{ (Ord a) } reads "a must implement Ord". Inside the body, you can use any Ord method on an a. Multiple constraints stack up with whitespace separation:

:fn hash-and-show ( a -> AnyInt Str )
    { (Hash a) (Display a) }
  peek-> x
  x .hash swap x "{}" format
:end

The Rust analogue is the where clause:

fn maximum<A>(x: A, y: A) -> A where A: Ord { … }

Constraint blocks are one of Silo's two ways to restrict what types can flow through a generic word. The other is predicates, introduced in chapter 5. Traits are for dispatch (different code per type); predicates are for gatekeeping (different types allowed at different call sites).

Dependent types

Silo is dependently typed, which means types can take values as arguments, not only other types. The classic example is a Vec whose length is in its type:

(Vec Int | 3)                    # a Vec of exactly three Ints
(Vec Str | n)                    # a Vec of n Strs, n is a variable

The 3 and the n above are values — integers, in this case — occupying what would otherwise be a type slot. When two Vecs have different type-level lengths, the compiler knows their types are different.

Range-refined integers work the same way:

:type Port (Int 0..2^16)

(Int 0..2^16) is the type of integers in the half-open range [0, 65536). Calling a function that expects a Port with any integer outside that range is a compile error. To go from a plain integer to a Port, you use the fallible .try-from:

80 (Port .try-from)            # ⌊Ok(Port(80))⌉
100000 (Port .try-from)        # ⌊Err("out of range")⌉

You can treat dependent types at two levels. Most of the time you rely on the standard library using them internally — Vec.append knows the length of the result because it knows the lengths of its inputs, and that propagates automatically. When you do want to reach for them yourself, the mechanism is the same: put a value in a type-parameter slot.

If "dependently typed" sounds alarming: in practice, it is almost always invisible. You don't write proofs, you don't annotate lengths, you don't wrestle with dependent pattern matches. The language is doing the bookkeeping in the background so that common invariants hold mechanically.

Type-level arithmetic

Because values live in the types, you need arithmetic at the type level. Silo writes it in the same postfix style as ordinary code, inside parentheses:

(n 1 +)                        # n plus 1
(n 2 *)                        # n times 2
(n m +)                        # sum of two type variables

These are most useful on signatures that describe how a word's output length relates to its input length:

:fn .append ( (Vec a | n) (Vec a | m) -> (Vec a | (n m +)) )
    { (AnyUInt n) (AnyUInt m) }
  ...
:end

The result type (Vec a | (n m +)) encodes "a Vec of length n plus m". The { (AnyUInt n) (AnyUInt m) } constraint says both lengths must be non-negative integers (values of kind AnyUInt). Together, you can chain .append calls and the compiler will track the cumulative length through the whole pipeline.

Higher-kinded types

A type variable can stand for any type. A higher-kinded type (HKT) variable stands for any type constructor — something that itself takes parameters.

In Silo, an HKT is just a type variable applied to more arguments. Here's a trait parameterised over a container type f:

:trait Mappable f mapped { (Foldable f) }
  .map ( (f a) [a -> b] -> (mapped b) )
:end

Read this as: a type f is Mappable into mapped if, given an (f a) and a function a -> b, you can produce a (mapped b). f ranges over containers — Vec, Option, HashMap, and so on — not over concrete types like Int.

HKTs are the reason .map works uniformly across every Silo container. Rust doesn't have them; the closest Haskell analogue is Functor, which is exactly this trait at a higher level of abstraction. If you've written Haskell, Mappable is just Functor specialised for the stack-based shape.

You won't often write HKT-quantified traits yourself, but you'll see them throughout the standard library. Knowing the syntax is enough to read what's there.

How the checker actually works

Silo's type checker uses forward propagation: it walks through each word's body from the start, tracking the stack's type at every point, and checks that every call matches the declared stack effect. Any mismatch becomes a compile error pointing at the specific word where the stack shape diverged from what the next caller expected.

This is different from ML-style Hindley-Milner inference, which gathers constraints across the whole program and solves them globally. Forward propagation is simpler and gives more localised error messages — the error appears where the mistake is, not at some other place the constraint bubbled up to. It's also what lets Silo check dependent types without a proof-assistant-grade solver: the compiler always knows concretely what's on the stack at each point.

Key points

  • Stack effects serve as type signatures. Lowercase names are universally quantified variables; uppercase names are concrete types.
  • Type application is parenthesised and head-first: (Vec Int | 3), (Option Str).
  • { (Trait x) … } after a signature is a constraint block: trait bounds on the word's type variables.
  • Types can take values as parameters. (Vec elem | n) tracks the length in the type; (Int 0..256) is a refinement type.
  • Type-level arithmetic is postfix: (n 1 +), (n m +). Use it in signatures where an output length relates to an input length.
  • An HKT variable stands for a type constructor. That's how Mappable, Foldable, and the rest of Silo's generic traversals are uniform across every container type.
  • The compiler uses forward propagation rather than global inference. Errors localise to where the mistake was made.

The next chapter covers numerics — the four numeric representations and the arithmetic-variant operators that prevent silent overflow.