The type system

A type in Dendrite is a small structure, never a string. Three shapes, and only the first is ever registered anywhere:

{ kind: "name", name: "number" }                          // number, string, Bus, …
{ kind: "array", element: Type }                          // number[]
{ kind: "function", params: Type[], returns: Type }       // (number) -> boolean

Named types are registered; arrays and functions are built

A language has a table of named types. number, string, boolean, any and null are in it from the start; a host adds its own.

Arrays and functions are not in any table. They are structural: number[] means exactly “array whose element is number”, and two of them are the same type if their elements are. There is no registration step, no T[] generated per T, and no list of “all the array types”, which is what makes string[][] and ((number) -> boolean)[] cost nothing to have.

It also means a type’s identity is structural all the way down for those two, and nominal for named types. Bus is Bus because it is called Bus.

One function decides compatibility

Everything that asks “does this value fit there” calls isCompatible, and nothing re-implements it. It is the single extension point for subtyping, and its rules are these.

any is data-only, in both directions. A data value flows into any, and an any flows into any data type. The second direction is the unsound one and it is deliberate: it is what lets a host say “I do not know what this is” without stopping the program. Each crossing raises an implicit_any_cast warning so you can see where you traded the check away.

That includes an any inside a list. An any[] fits a number[] through the covariance below, and it is the same trade one level down, so it warns the same way, however deep the lists nest. Two things stay quiet on purpose. An empty list literal has no items to take a type from, so Average([]) is not a cast. And a function is left alone: an untyped lambda handed to Filter is gradual typing the rules below allow, not a value whose type was lost.

The warning names what you wrote. $height >= 10 over an any height says '$height' is 'any' typed, not Input 'a': a is an input of the LessThan that >= became, and nobody typed it. A value with no name of its own, a call or a literal, is named by the op and the input it went into.

Nothing else converts. There is no coercion between data types: a number is never read as a boolean, because that would need a conversion node inserted behind the author’s back, a rewrite this language does not have. The sound alternative is to convert in the open, with ToString, ToNumber and ToBool (conversion): ordinary ops with fixed output types, so the checker stays honest about what comes out.

A function is never any. This is the one exception to the rule above and it carries a lot of weight. See below.

null flows anywhere a data value is expected. An unset input holds null, so a program over unset inputs still compiles. It is the same trade as any and it is why Default and IsSet exist.

Arrays are covariant. number[] fits any[], because reading is all you can do with a list here: there is no mutation, so the usual unsoundness of covariant arrays has nothing to bite on.

Functions are contravariant in their parameters and covariant in their return. A function accepting any fits where one accepting number is wanted, because it accepts more; one returning number fits where any is wanted, because it promises more. The ordinary rule, and the reason Filter can hand your lambda a number when its signature says any.

extends makes a chain. A named type may extend another, and compatibility walks up the chain. A struct field may be narrowed in the extending type but not made incompatible, which is what incompatible_field_override catches.

Why a function is never any

This single rule is what makes every Dendrite program terminate.

Self-application is the shape recursion needs: a function that takes itself. To type it, you need somewhere for “a function” to fit loosely, and the only candidate is any. Close that door and the shape is untypable: there is no way to write the fixed-point combinator that would let a lambda reach itself.

The other door is a name referring to itself, and that is a binding_cycle.

Both shut, and what you get is a language that is strongly normalising: every program finishes, in time bounded by the program’s own size and its data. Which matters most when you are the one embedding it, because it means no program a user writes can hang your application. You pay for it with no user-written recursion, and you get the list ops instead.

A literal’s type is read off it

You never have to annotate a list:

let numbers = [4, 8, 15]
output total = Average(numbers)

numbers is number[], inferred from the elements. Mixed contents fall back to any[]. An empty list is any[] too, since there is nothing to read, which is the one place you may want to say more: let none: number[] = [] states the type, the checker holds the value to it, and every reader of none sees a number[]. A stated type that the value does not fit is a binding_type_mismatch, and a name in it the language does not have is an unknown_type.

Ops can be more precise than their signature

A signature is the general case. An op may narrow it for a particular call, through two hooks a host can use as well:

• inferInputTypes refines what an op expects from what it was given. Filter uses it to tell you its predicate takes the element type of the list you passed, which is why the lambda parameter needs no annotation.
• inferOutput computes the concrete output type. Filter returns the list’s own type, Map the return type of your function, If the branch type when both branches agree and any when they do not.

So the reference tells you what an op accepts, and the analyser tells you what your call produced. Where those differ, the analyser is right.

What is not here

No generics, no unions, no intersections, no optional fields. The type system is as small as it can be while checking what programs in this language actually do, and every rule above exists because something needed it. come from.