Implicit generics

Par already supports explicit generics via forall:

module Main

import {
  @core/Int
  @core/String
}

dec Swap : [type a, type b, (a, b)!] (b, a)!
def Swap = [type a, type b, pair]
  let (first, second)! = pair
  in (second, first)!

With forall, callers pass types explicitly when they use Swap:

def Pair = ("Hello!", 42)!
def Swapped = Swap(type String, type Int, Pair)

That is precise and fully explicit. But in many everyday cases, the types are obvious from the value you are passing. For those cases, Par also has implicit generics.

Syntax

Implicit generics are not a standalone type. The <a, ...> binder is an extension of a function type: it must appear immediately before the [...] of that type.

<a, b>[Arg] Res

You cannot write <a> in front of either, choice, box, or anything else.

The key rule is local inference:

Implicit type variables are inferred only from the single argument immediately following the <...> binder.

This is also reflected in the syntax: the bracket right after <...> must contain exactly one argument type. If you need multiple value arguments, you still write a curried function type.

So this is valid:

dec Concat : <a>[List<a>] [List<a>] List<a>

But this is not valid syntax:

dec Concat : <a>[List<a>, List<a>] List<a>

When calling such a function, you can still pass all arguments at once:

Concat(left, right)

The type is still written in curried form, because inference must happen from that first argument alone.

One more important point: there is no syntax for “manually specifying” implicit type arguments. When designing an API you choose, for each type variable, whether it is implicit or explicit:

• If it is implicit (<a>), it is always inferred.
• If it is explicit ([type a]), it is always specified by the caller.

This is intentional: it keeps call sites predictable.

Implicit type parameters can also carry constraints, such as <a: box> or <a: data>. The constraints themselves are covered in Type Constraints.

Construction

Start with the Swap example, but make it implicit:

dec Swap : <a, b>[(a, b)!] (b, a)!

To construct a value of this type, you also introduce the implicit type names at the term level, and then receive the value argument:

dec Swap : <a, b>[(a, b)!] (b, a)!
def Swap = <a, b>[pair]
  let (first, second)! = pair
  in (second, first)!

This is intentionally different from forall: an implicit generic and an explicit forall generic are different types, and they do not subtype into one another.

You can also use implicit generics when the type variable is nested inside a larger argument:

dec Flatten : <a>[List<List<a>>] List<a>

Destruction

To use an implicit generic, you call it like an ordinary function:

def Swapped = Swap(Pair)

Here a = String and b = Int are inferred from the type of Pair (the argument immediately following <a, b>).

If you want to steer inference, you can still add annotations locally, for example by ascribing a type to an expression:

type T in expr

For example (this is a bit contrived, but it shows the point):

Concat(type List<Nat> in *(), numbers)

If you wrote Concat(*(), numbers), the empty list *() would lead a to be inferred as either {} (an impossible type), so inference would not pick Nat for you.

Higher-order arguments

Implicit generics infer their type variables from the argument value. This works great when that argument already has a clear type, and Par can also use the expected argument type to check expressions whose type is only partially known.

A classic example is an anonymous function. The box here is not the point — it just happens that Map takes a boxed function.

dec Map : <a>[List<a>] <b>[box [a] b] List<b>

The list argument infers a. When checking the mapper, b is still unknown, but the checker can still use the partial expected type box [a] b. That means the lambda parameter gets type a, while constraints from the lambda body solve b:

Map(numbers, box [x] `#{x}`)

Here x is checked using the element type of numbers, and the string interpolation result infers b = String.

You may still need a local annotation when the argument does not constrain the type enough. Empty structures are the usual example:

Concat(type List<Nat> in *(), numbers)

The annotation is on the value being passed, not on the implicit type parameter. There is still no syntax for manually passing an implicit type argument.

(Map is discussed in Box.)

Implicit generics and pairs

Implicit generics also exist for pair types. This is the implicit counterpart of exists.

Just like with functions, the <a, ...> binder is part of the following pair type: it must appear right before the (...) of that pair type.

Here is a simple example. AnyDrop stores a value of some unknown type, plus a small “vtable” for dropping it (a boxed choice):

type AnyDrop = <a>(a) box choice {
  .drop(a) => !,
}

This is the implicit counterpart of the existential type:

type DropMe = (type a, a) box choice {
  .drop(a) => !,
}

Construction

Notice that you do not specify the hidden type when constructing an AnyDrop:

def Example: AnyDrop = (7) box case {
  .drop(_) => !,
}

Destruction

Dually, when you unpack an implicit-generic pair, you introduce a local type variable:

let <a>(value) vtable = Example
vtable.drop(value)

This is the “mirror image” of implicit-generic functions: there you introduce <a, ...> at construction time and inference happens at call time; here you construct without naming a, and introduce a when unpacking.