Getting started

Welcome to the Wipple Guide! This guide contains a tour of the Wipple programming language designed for people with an existing programming background.

You can jump between sections using the table of contents on the left.

Hello, world!

Let’s start by displaying the string “Hello, world!” on the screen. Wipple has a built-in function named show for this:

show "Hello, world!"

Notice that in Wipple, you don’t need parentheses to call a function. Instead, parentheses surround code that’s nested inside a function call, like in these examples:

show (increment 1)
show (increment (increment 1))
show (1 + 2)

You can also store values in variables to give them a name. In Wipple, variables are defined using a colon (:):

name : "Wipple"
show name

sum : 1 + 2
show sum

If a string contains underscores (_s), you can perform string interpolation — variables placed after the string will replace the underscores:

show ("Hello, _!" name)

Blocks and control flow

A block is a piece of code surrounded in braces ({⋯}). Blocks let you store code to run it later. To run the code in a block, use do:

greeting : {show "displays second"}
show "displays first"
do greeting

Wipple uses blocks to implement control flow. For example, the if function accepts a Boolean condition (True or False) and two blocks. If the condition is True, the first block will be evaluated with do, and if it’s False, the second block will be evaluated.

secret : 5
guess : 3
if (guess = secret) {show "You win!"} {show "Try again"}

If the calls to show weren’t wrapped in blocks, they would both run and both messages would appear on the screen.

You can run a block with do multiple times, which is how repeat is implemented:

repeat (3 times) {
    show "Hello, world!"
}

Just like with if, without the block, the message would only be displayed once.

Blocks produce values, which means you can assign the result of if to a variable and factor out the show:

message : if (guess = secret) {"You win!"} {"Try again"}
show message

It’s important to remember that blocks are values, just like strings and numbers are — they can be stored in variables and passed to functions. if and repeat are regular functions that accept blocks as input. You can build your types of control flow easily, and we’ll do just that in the next section!

Functions

Functions in Wipple are written with an arrow (->) separating the inputs from the output. Just like blocks, Wipple’s functions are also values. That means to give a function a name, you assign it to a variable; there’s no special syntax for defining a named function. Putting it all together, here’s a function that adds two numbers:

add : a b -> a + b
show (add 1 2)

(Also notice that you don’t need to separate multiple inputs with commas.)

If you want to have multiple statements in a function, you can run a block with do. If a block has multiple statements, the last one is the function’s return value:

debug-add : a b -> do {
    show ("called debug-add with _ and _" a b)
    a + b
}

show (debug-add 1 2)

Don’t forget to put do before the block — since blocks are values, without do, the function will return the block itself instead of running its code!

You can combine blocks and functions to build your own control flow. Here, twice accepts a block as input and runs it twice:

twice : block -> do {
    do block
    do block
}

twice {show "Hello, world!"}

The type system

Wipple has a powerful type system that can catch bugs in your program. Types in Wipple begin with a capital letter, such as String. All Wipple code is checked at compile time to ensure it has exactly one known data type. A lot of the time, Wipple can determine this type automatically — for example, Wipple knows that "abc" is a String, which means the show in show "abc" must be a function accepting a String.

How it works

At compile time, Wipple simulates the flow of information through the program and sorts the code into groups. All members of each group must have the same data type. Groups are formed using a few rules:

• Variables are grouped with their values.

• All uses of a variable belong to the same group. In other words, accessing the same variable will always give you a value of the same data type.

• When you call a function, each argument is grouped with its corresponding parameter.

• When you run a block with do or call a function, the result is grouped with the output defined within the block or function.

Let’s apply these rules to an example program:

increment : x -> x + 1
a : increment 123
b : increment "abc"

We get two groups of interest:

1. The group containing x, 123, and "abc" (the inputs).

2. The group containing x + 1, a, and b (the outputs).

After forming groups, Wipple then considers data types like Number and String. Unlike in other languages, data types apply to groups rather than individual expressions. In the first group:

• x doesn’t contribute a type of its own.
• 123 contributes Number to the group.
• "abc" contributes String to the group.

That means Group 1 contains two data types, Number and String. Since there is more than one type in the group, Wipple produces an error, which appears on the first member of the group (the input x).

x -> x + 1
~ error: `x` is a `Number` or a `String`, but it can only be one of these.

Wipple’s approach differs from languages where you might see an “expected Number, but found String” error message on "abc". These languages create a placeholder for the input x that is replaced with Number when the function is first called with 123. Wipple, on the other hand, doesn’t assume any one group member is the “right” candidate — it waits to fill the placeholders with concrete data types until all group members are considered, and is thus able to provide more accurate error messages.

As a bonus, this group-based design means you can easily see code related to your cursor! Try pasting this program into the playground, click on x, and observe how 123 and "abc" are highlighted.

Type annotations

In addition to letting Wipple infer types, you can use :: to annotate any piece of code with its expected data type, and Wipple will verify that it’s correct at compile time. These type annotations serve as a form of documentation, describing the kinds of values your code works with and produces.

sum : 1 + 1
show (sum :: Number) -- correct
show (sum :: String) -- error

As a special case, if you add a type annotation on its own line, Wipple defines a constant value that is “lifted” out of the normal control flow and can be used anywhere. Constant values are evaluated when they are used, not at their definition like with variables.

show pi -- defined below

pi :: Number
pi : 3.14

In general, type annotations mirror the syntax of their corresponding expression. If you use a lowercase name in a type annotation, the constant becomes generic and can work with any type:

add :: Number Number -> Number
add : a b -> a + b

identity :: value -> value
identity : x -> x

if :: Boolean {output} {output} -> output
if : todo

When a constant is generic, a copy of its type annotation is made whenever it is referenced. That means uses of constants don’t share groups with each other.

Constraints

Recall our earlier program involving increment that had an error (because x, 123, and "abc" were all grouped together):

increment : x -> x + 1
a : increment 123
b : increment "abc"

Let’s try to fix the error by making increment generic, and run our rules again!

increment :: value -> value
increment : x -> x + 1

a : increment 123
b : increment "abc"

Now our groups look different:

1. One group contains a unique copy of value and 123. This group has type Number.
2. The other group contains a unique copy of value and "abc". This group has type String.

In addition, because value is also the output of the function, Group 1 contains a and Group 2 contains b. Therefore, a is a Number and b is a String as expected.

However, in fixing this issue, we have introduced another one! Because a new copy of value is made each time increment is referenced, inside the definition of increment, value is unknown. In other words, because our constant is generic, we can no longer assume anything about the input. That means x + 1 isn’t necessarily a valid operation. (It may be when value is a Number, but not when it is a String.)

Wipple supports fixing this new error by introducing a constraint to our function. With the where keyword, we move the requirement that + 1 is valid to each user of increment. It looks like this:

increment :: value -> value where (Add value Number value)
increment : x -> x + 1

Reading this code out loud, it says “increment requires that you can Add your value and a Number to get a new value.”

(As an exercise, what would the constraint be for the function double shown below?)

double :: value -> value where ???
double : x -> x + x

Now it’s up to each caller of increment to ensure that the input they provide can be added with a Number.

a : increment 123 -- works!
b : increment "abc" -- error: can't add `"abc"` and `Number`

Constraints are a powerful way to make your code more flexible. Wipple has several built-in constraints, including Add for +; Describe, which converts the input to a String and is used by show; and Equal, which lets you compare two values for equality.

Traits and instances

Wipple also supports defining traits, which can be used to make custom constraints. They work similarly to interfaces in other languages and look like this:

Count : container => trait (container -> Number)

Let’s look at each component:

Count : container => trait (container -> Number)
-----   ---------           -------------------
name    parameters          value

The => means that Count behaves like a function on types: provide an input type corresponding to container, such as String, and you get back a constraint that requires Count to have a valid String -> Number value.

Before we can use a trait, we also have to define its value for each type we’re interested in. That is done using instance:

instance (Count (List element)) : list -> length list
instance (Count String) : string -> length (characters string)
instance (Count (Dictionary key value)) : dict -> length (keys dict)

You can use a trait directly, in which case the parameters are inferred, or you can use it as part of a constraint:

show (Count "abc") -- 3

count-both :: left right -> Number where (Count left) (Count right)
count-both : a b -> Count a + Count b

Finally, instances may themselves have constraints!

-- Implementation omitted
instance (Count (Pair first second)) where (Count first) (Count second)

Modeling data

Structures

To define a structure type, use the type keyword:

Sport : type {
    name :: String
    players :: Number
}

You can construct a structure value similarly:

basketball : Sport {
    name : "Basketball"
    players : 5
}

To get the values out of a structure, you can put a block on the left-hand side of the colon (:), listing the field(s)’ names and the corresponding variable names.

Sport {name : sport-name} : basketball
show sport-name

Basketball

Pattern matching

Wipple uses pattern matching to express control flow. For example, let’s say we want to generate a report card:

Grade : type {
    A
    B
    C
    D
    F
}

report-card :: Grade -> String
report-card : grade -> when grade {
    A -> "top of the class"
    B -> "good work"
    C -> "need to study"
    D or F -> "didn't pass"
}

show (report-card A) -- top of the class

First, we define our patterns using type. Rather than providing fields, we list the variants, and Wipple will create an enumeration for us. Then, we use when to return a different value for each variant. You can use or to match multiple variants at once.

In fact, in Wipple, if is just a regular function that matches on Boolean. We can create our own easily:

My-Boolean : type {
    My-True
    My-False
}

my-if : bool then else -> when bool {
    My-True -> do then
    My-False -> do else
}

show (my-if My-True {123} {456}) -- 123

In addition to enumerations like these, you can store data alongside each pattern, allowing you to express values that are tied to a condition — in other words, the value is “wrapped” in a pattern, and you need to “unwrap” the value by checking for the condition using when. This may sound a bit confusing if you’ve used other languages without this feature, so let’s look at an example:

Maybe-Number : type {
    Some-Number Number
    No-Number
}

Here, we create a Maybe-Number value with two patterns. The first pattern contains a Number, and the second pattern contains nothing. Now, we can use pattern matching to “unwrap” the Maybe-Number:

describe-maybe-number : maybe -> when maybe {
    Some-Number n -> "we have a number: _" n
    No-Number -> "we don't have a number"
}

show (describe-maybe-number (Some-Number 42))
show (describe-maybe-number No-Number)

Why is this useful? It means we can represent errors in our program! Let’s go back to our report card example, and allow the user to specify a grade as input:

Maybe-Grade : type {
    Valid-Grade Grade
    Invalid-Grade
}

parse-grade :: String -> Maybe-Grade
parse-grade : string -> when string {
    "A" -> Valid-Grade A
    "B" -> Valid-Grade B
    "C" -> Valid-Grade C
    "D" -> Valid-Grade D
    "F" -> Valid-Grade F
    _ -> Invalid-Grade
}

repeat forever {
    grade : parse-grade (prompt "Enter your grade")

    when grade {
        Valid-Grade g -> show (report-card g)
        Invalid-Grade -> show "invalid grade"
    }
}

Wipple’s type system will check for us that we handle the error — watch what happens if we pass our Maybe-Grade to report-card directly:

grade : parse-grade (prompt "Enter your grade")
show (report-card grade) -- error

Wipple includes a built-in type for error handling, Maybe. Here is its definition:

Maybe : value => type {
    Some value
    None
}

Similarly, the built-in Read trait is defined as:

Read : output => trait (String -> Maybe output)

The example above can be rewritten to use Maybe and Read, and prompt will handle validation for us!

instance (Read Grade) : string -> when string {
    "A" -> Some A
    "B" -> Some B
    "C" -> Some C
    "D" -> Some D
    "F" -> Some F
    _ -> None
}

grade : prompt "Enter your grade"
show (report-card grade)

Documentation and error messages

Wipple displays your documentation comments in IDEs and error messages, and allows you to customize errors using the type system.

Links in documentation comments

Documentation comments are regular comments (--) that appear immediately above a definition. Within documentation comments, you can use Markdown links to reference any defined type parameters. Each of these links will resolve to the expression that corresponds to the type parameter.

For example, the Add trait has a documentation comment that looks like this:

-- [`Add`] adds [`left`] and [`right`] together, returning a [`sum@type`].
Add : left right (infer sum) => trait (left right -> sum)

When you write 1 + 2:

• Add is replaced with the expression 1 + 2.
• left is replaced with the expression 1, and right is replaced with the expression 2.
• sum@type is replaced with Number, the type of sum.

`1 + 2` adds `1` and `2` together, returning a `Number`.

Sometimes, your definition will accept a concrete type, such as Number, instead of a type parameter, but you still want to reference the provided expression in a link. Wipple supports this with inline type annotations:

-- [`positive?`] returns `True` if [`n`] is greater than 0.
positive? :: (n :: Number) -> Boolean
positive? : n -> n >= 0

positive? 1 -- `positive?` returns `True` if `1` is greater than `0`.

You can use inline type annotations anywhere in the signature, including on types containing type parameters of their own.

Custom errors with error instances

An error instance is an instance marked with the error keyword and has no value. When a trait resolves to an error instances, Wipple will replace the default error message with the instance’s comment:

-- Can't count the contents of a block. Are you missing `do`?
error instance (Count {output})

You can combine error with default to customize the error displayed when no other instances match:

-- Can't count the contents of [`value`].
default error instance (Count value)

Error instances also support inline type annotations:

Count : value => trait (value -> Number)

-- Can't count the contents of [`block`]. Try adding `do` to count the
-- inner [`output`].
error instance (Count (block :: {output}))

number : {123}
Count number -- Can't count the contents of `number`.

In addition, you can define traditional “expected/found”-style error messages with the Mismatched trait. Whenever a group has more than one type, Wipple will attempt to resolve Mismatched instances for each pair of types. To display a custom error message, define an error instance for the types you are interested in.

Distance : type {meters :: Number}

[unit] m :: Number -> Distance
m : value -> Distance {meters : value}

-- Missing a unit for distance. Try adding `m` after [`n`].
error instance (Mismatched (n :: Number) Distance)

forward :: Distance -> ()
forward : todo

forward 50

Overview

The Wipple compiler is designed around a database of nodes, where nodes can have arbitrary facts. A node is a handle to an expression, pattern, type, or other program element. Facts represent the results of parsing (e.g., Syntax), name resolution (e.g., Defined and Resolved), type checking (e.g., Typed and Bounds), and other phases. The IDE can query these facts to obtain the information it needs for error messages, autocomplete, etc.

Syntax

Nodes that represent program elements written directly in the source code have the Syntax fact, which contains a span (a file path and range) and the underlying AST value. The AST is generated by a recursive-descent parser.

All AST values implement Visit, which the compiler calls to traverse the program and perform name resolution and instantiation. Most nodes call visit on their children directly, but some forward to other nodes created while visiting. For example, operators (such as 1 + 2) instead create a virtual function call node (such as Add 1 2) and visit that.

Type checking

Wipple’s type system operates on groups of nodes. Concrete types, such as String, are assigned to the group as a whole rather than individual expressions.

The type checker accepts constraints (defined on nodes) as input. There are five types of constraints:

1. Group constraints place two nodes in the same group.

2. Type constraints assign a concrete type to the group of a representative node. When more than one concrete type is assigned to the same group, the types are unified if possible.

   For example, the expression n :: Number would generate a group constraint between n and Number. Then, the node representing Number would generate a type constraint for the concrete type Number, resulting in n and Number sharing this type.

   Of note is that the node representing the source code Number and the concrete type Number are different objects in the compiler — most nodes representing types in the source code contribute equivalent type constraints, but some contribute different constraints. For instance, placeholders (_) do not contribute any constraints, and instead inherit their type from the group they belong to; _ is not a concrete type. This allows code like (1, 2, 3) :: List _ to resolve to List Number. Similarly, the first time a type parameter is used, it contributes a type constraint, but subsequent uses instead contribute group constraints linking back to the first use.

3. Instantiate constraints take a generic definition and makes a copy of all of the definition’s constraints, where any mentioned type parameters are replaced with fresh nodes, and where mentions of the definition node are replaced by the instantiated node. This design straightforwardly preserves groups, bounds, and other information beyond the definition’s concrete type.

   For example, the definition id :: value -> value would generate a group constraint between the two values, and a type constraint assigning the concrete type parameter value to this group. Then, calling id 123 would generate a fresh node representing the instantiated value, along with the original group constraint and type constraint modified to use this fresh node. Finally, the literal 123 generates a type constraint assigning Number to the instantiated value group, resulting in the function call expression id 123 also having type Number.

4. Bound constraints resolve trait bounds.

   To resolve bounds, the type checker iterates over each available instance, unifying the instance’s instantiated parameters with the bound’s. If any errors occur during unification, the instance is discarded and the type checker is restored to its previous state. For example, given the instances As-Sequence String String and As-Sequence (List element) element and the bound As-Sequence (List Number) x, the first instance fails because String and List _ do not unify, and the second instance succeeds, assigning Number to the group containing x.

   During bound resolution, if more than one instance matches, the bound is considered ambiguous and is added back to the queue. To prevent infinite loops, the type checker stops if no progress is made (i.e., a concrete type is assigned to a group or a bound is resolved) after iterating through the entire queue.

5. Default constraints act like type constraints, but only if the node’s group does not already have another concrete type.

Querying and feedback generation

Feedback (error messages) is created by querying the database for nodes with specific facts. For example, the conflicting-types error message is produced for any node belonging to a group with multiple concrete types.

Code generation

Wipple compiles to an intermediate representation (IR) via a Codegen fact. Then, the IR is monomorphized and compiled to JavaScript.

Generics and instantiation

Instantiation is the process performed by the compiler to give each use of a generic definition a “fresh” set of types. For example, in the program below, show is called with both a Number and a String, which is allowed because the value type parameter is copied into each call separately, forming different groups:

show :: value -> () where (Describe value)
show : output (Describe value)

show 123 -- `value` is `Number`
show "abc" -- `value` is `String`

Definition site

In generic code, such as within the signature and body of show above, type parameters are given a unique concrete type using a type constraint. This prevents values of parameter type (e.g., value) from being used in place of other concrete types or type parameters. Without this constraint, you could easily define a transmute function:

transmute :: a -> b
transmute : x -> x -- if `a` was assignable to `b` here...

x : (transmute 123 :: String) -- ...then `x` can be a `String` but hold a `Number`!

Similarly, in the body of show above, this means the Describe value bound only applies to the specific value parameter, not any arbitrary type like at the use site. Since bounds are implied inside the body of generic definitions, allowing type parameters to be assignable to each other would allow you to refer to an undefined instance.

When a type parameter appears multiple times in a signature, only the first appearance is given the type constraint; the other appearances are grouped with the first.

Use site

During instantiation, instead of deeply applying the type of the definition once and then replacing encountered type parameters, Wipple creates a copy of all the constraints generated — including bounds — while traversing the definition’s signature (but not its implementation). Then, every node referenced in these constraints is replaced with a fresh node, and any type constraints involving type parameters are similarly replaced by fresh group constraints. Finally, these new constraints are enqueued in the type checker.

The mapping between generic and instantiated nodes/parameters is recorded in a mutable substitutions list, which can be shared across multiple instantiations using a key. This allows, for example, bound resolution to retrieve back the resolved parameters from each candidate.

In addition, the compiler passes around the source node responsible for instantiating a given definition. This source node is attached to all instantiated nodes via the Instantiated fact. When there are no non-generic nodes available (i.e., all relevant nodes are constants or traits), this allows diagnostics to show conflicts in instantiated type parameters on the source node, such as for the program below:

f :: Number -> ()
list :: List String

-- There are no variables here!
(each f) list -- error: in `each`, `element` is a `String` or a `Number`

This information is also used to populate links in comments. Links to the definition are replaced with the source node, and links to type parameters are replaced with a representative from the instantiated parameter’s group:

-- [`Equal`] returns `True` if both [`value@type`] values are equal.
Equal : value => trait (value value -> Boolean)

123 = 456 -- on hover: `123 = 456` returns `True` if both `Number` values are equal.

The trait system

Wipple supports ad-hoc polymorphism using traits. Traits in Wipple are similar to multi-parameter type classes in Haskell. A trait is defined over one or more type parameters, and users can define instances replacing these type parameters with specific types. Wipple will select the appropriate instance automatically.

For example, a common trait in Wipple is Describe, which is used by show to convert its input to a String:

Describe : value => trait (value -> String)

instance (Describe String) : s -> s
instance (Describe Boolean) : b -> if b {"True"} {"False"}

To reference an instance of a trait, you write the trait’s name (forming a trait expression), and the compiler will select the matching instance based on the data type of the trait expression.

(Describe :: String -> String) -- instance (Describe String)
(Describe :: Boolean -> String) -- instance (Describe Boolean)

If the trait is a function, then you can also simply call the trait expression directly, and type inference allows you to omit the annotation.

Describe "abc" -- instance (Describe String)
Describe True -- instance (Describe Boolean)

The remainder of this article explains how the compiler selects instances.

The trait’s signature

When the compiler encounters a trait expression, it first instantiates the trait’s signature, replacing all referenced type parameters with “fresh” placeholders. For Describe, the trait expression begins with the type <value> -> String, where <value> represents the instantiated value parameter.

Recall that Wipple’s type checker operates on a list of ordered constraints, so each trait expression actually generates the following constraints:

• A group constraint grouping the instantiated signature with the trait expression;

• Type constraints for each concrete type in the signature; and

• A bound constraint to find the matching instance.

Because all constraints of each type are evaluated before moving to the next type, the bound constraint won’t be evaluated until all available type information from the context surrounding the trait expression is collected. For example, given the program Describe True, the constraint True :: Boolean will be evaluated before searching for a matching Describe instance, allowing the compiler to easily select instance (Describe Boolean).

Bound resolution

When the compiler reaches the bound constraint, it iterates through each instance defined on the trait and attempts to instantiate them. This process is performed on copies of the type checker, because otherwise, non-matching instances would “pollute” the groups involved in the trait expression. (For example, instance (Describe String) adds the type String to the group containing True in Describe True, but that group already contains the type Boolean, leading to an error. Instead of showing the user this error, we want to ignore this non-matching instance.)

First, the compiler sorts the instances into four groups: “regular” instances, error instances, default instances, and default error instances. These groups are considered in order, so that the compiler will only try default instances if no regular instances match. Similarly, when the compiler checks for overlapping instances, this check is done per group, allowing users to define generic default instances as well as specific regular instances.

Within each of these groups, the compiler creates a copy of the type checker for every instance. Within these copies, the associated instance is instantiated, and the type checker is ran until the first bound constraint is reached (i.e., only group and type constraints are evaluated). If at this point the type checker has reported an error, the instance is discarded. Otherwise, the instance and the copy of the type checker are added to a list.

Next, the compiler looks at the length of the resulting list of instances:

• If there are no matching instances, the next group of instances is considered. If all groups have been considered and there are still no matching instances, then the compiler reports an error.

• If there is more than one matching instance, then the bound constraint is added back into the queue, and will run again when more type information is available (i.e., by resolving another instance or via a default type constraint).

• If there is exactly one matching instance, then evaluation of the bound constraint stops and the outer type checker’s state is replaced with the copy’s state.

Assuming there is a single matching instance, the type checker will now contain the remaining constraints not evaluated by the inner copy (namely, the bounds on the selected instance itself). This enables instances to have bounds of their own. To prevent infinite recursion of the form instance (A value) where (B value) and instance (B value) where (A value), the type checker has an iteration limit.

error instances are treated the same as regular instances during bound resolution. The compiler runs a separate query later to report error instances as error messages.

Implied instances

Bounds placed on instance and constant definitions are the responsibility of the caller to satisfy. That means within the definitions, we can assume these bounds will have a single matching instance. Importantly, these bounds are not instantiated and instead only apply to the specific type parameters they use — in other words, the type parameters are treated as concrete types. For example, unzip has two bounds for Initial containing different type parameters:

unzip :: collection -> (left; right)
  where (Initial left) (Initial right) ...

When unzip’s implementation references Initial, it could refer to either of these bounds. If the bounds were instantiated like regular instances, then the trait expression (Initial :: right) would resolve to both Initial <left> and Initial <right> (where <left and <right> are instantiated placeholders). However, since Initial left and Initial right are implied, they remain uninstantiated and only Initial right will be selected.

Finally, when type checking instance definitions, the instance being defined is also implied inside its own definition, allowing for recursive instances.

Inferred parameters

Traits can mark one or more of their type parameters as inferred using infer. During bound resolution, inferred parameters are not checked and instead propagate back to the caller. If regular type parameters behave as “inputs” to the trait when searching for bounds, inferred parameters effectively behave as “outputs”. For example, the Add trait defines its sum parameter as inferred:

Add : left right (infer sum) => trait (left right -> sum)
instance (Add Number Number Number) : ...

As a result, if you call Add with two Numbers where a String is expected, the instance (Add Number Number Number) is still selected (because the third Number is ignored), and you get a standard type conflict error on the call to Add instead.

sum :: String
sum : 1 + 2 -- error: `1 + 2` is a `Number` or a `String`