cálculo lambda simplesmente tipado

O cálculo lambda simplesmente tipado, ou cálculo lambda com tipagem simples, é um modelo da teoria dos tipos que adiciona o conceito de tipagem ao cálculo lambda. Isso é possível com adição de apenas um elemento (o construtor de tipos: ) para construir tipos de funções. Esse é o exemplo mais simples e canônico de um cálculo lambda com tipagem. O cálculo lambda simplesmente tipado foi introduzido originalmente por Alonzo Church em 1940 como uma tentativa de evitar o uso paradoxal do , o qual mostrou várias propriedades interessantes e desejadas. O termo tipo simples também é utilizado para se referir à extensões do cálculo lambda simplesmente tipado como produtos, coprodutos, números naturais ou até recursão completa. Em contraste, sistemas que introduzem tipos polimórficos (como o ) ou não são considerados simplesmente tipados. O cálculo lambda simplesmente tipado é considerado simples por conta da Codificação de Church de suas estruturas que pode ser feita usando apenas o símbolo e variáveis de tipos adequadas, enquanto polimorfismo e dependência não podem.