Na teoria dos tipos, as variáveis de uso único são modeladas com (uma derivada de) lógica linear . Na lógica linear, uma proposição só pode ser usada uma vez; lógica linear às vezes é vista como uma lógica de recursos . Na lógica linear, se você quiser usar A duas vezes, você precisa ter A⊗A (A e A) disponíveis; se você quiser usar A quantas vezes quiser, você precisa ter! A (“claro que é A”).
A lógica linear não entrou em muitas linguagens de programação tradicionais. É a base da tipagem de exclusividade no linguagem de programação limpa que é usada para modelar efeitos colaterais. Em Clean, uma expressão do tipo Int
denota uma computação pura que produz um valor inteiro, ou seja, um cálculo que pode ser feito a qualquer momento, ou várias vezes, sem alterar o comportamento do programa. Uma expressão do tipo u:Int
denota uma computação que produz um inteiro e que deve ser executada exatamente uma vez, por exemplo, porque realiza um efeito colateral.