XXIIVV

Types are a way to suggest or restrict the activities possible for an object of that type.

A type system defines how a programming language classifies values and expressions into types, how it can manipulate those types and how they interact. The goal of a type system is to verify and usually enforce a certain level of correctness in programs written in that language by detecting certain incorrect operations. Type inference refers to the automatic detection of the type of an expression.

Weak typing allows a value of one type to be treated as another, for example treating a string as a number. Strong typing raises an error on attempts to perform an operation on the wrong type of value.

Type Inference in Stack-Based Programming Languages

In an applicative language, things are evaluated by applying functions to arguments. This includes almost all programming languages in wide use, such as C, Python, ML, Haskell, and Java. In a concatenative programming language, things are evaluated by composing several functions which all operate on a stack, passed from function to function.

Concatenative programming is so called because it uses function composition instead of function application.

Type inference in stack-based programming language is done by checking the stack effect declarations of words before they can be run, against the cumulative stack state of each item in the definition of each word.

pop ( 1 -- )
swap ( 1 2 -- 2 1 )

Words that do not pass the stack checker are rejected and cannot be run, and so essentially this defines a very simple and permissive type system that nevertheless catches some invalid programs and enables compiler optimizations.

The simplest case is when a piece of code does not have any branches or recursion, and just pushes literals and calls words. Pushing a literal has stack effect ( -- x ). The stack effect of most words is always known statically from the declaration.

Typed Concatenative Languages

incoming uxntal types