Lambda the Ultimate

Lembrando que no LtU Imperative os modelos semânticos se baseiam apenas em:

1. expressões lambda
2. expressões condicionais
3. atribuição

Se tivermos avaliação em ordem normal, até mesmo as expressões condicionais podem ser modeladas usando expressões lambda. Assim, teríamos apenas a necessidade de 1 e 3. O problema é que, como notado no paper original sobre Scheme, a ordem normal de avaliação complica a implementação correta da recursividade final. Mas, se usarmos o estilo de passagem de continuações sempre, obtemos independência da ordem de avaliação específica, como observado por Reynolds e Steele & Sussman; assim podemos ter uma linguagem em ordem normal e com recursividade final, eliminando a necessidade de ter expressões condicionais como primitivas.

Agora acabei de reler essa parte no AIM-349 (o "Scheme: an Interpreter for Extended Lambda Calculus") e vi que esta observação também está lá. Enfim, é difícil ser original, ainda mais considerando que esses artigos têm em média 30 anos de idade.

Seria possível eliminar a atribuição, ficando apenas com expressões lambda para tudo ? Aparentemente não, até porque o lambda-calculus puro é livre de efeitos colaterais, e nós queremos modelar estruturas que apresentam efeitos colaterais. Será que não dá para colocar uma mônada aí no meio ? E mais, fazer isso sem passar para uma extensão do lambda-calculus puro ?

(Nota: se não me engano alguém já provou que ter continuações e atribuição em uma linguagem é equivalente a ter mônadas numa linguagem sem efeitos colaterais, mas qualquer conjunto menor é menos expressivo; depois vou procurar esse artigo)