Making uniqueness typing less unique

Abstract

Computer science distinguishes between two major programming paradigms: imperative and functional programming. Central to imperative programming is the notion of some form of state (or memory) together with a list of instructions that inspect and modify that state. The canonical example of this paradigm is the Turing machine. Functional programming on the other hand is centred around a mathematical language with a notion of evaluation of expressions in this language. The notion of state- the core concept in imperative programming- is completely absent. The canonical example of the functional paradigm is the lambda calculus.