Existe um cálculo de SKI digitado?

26

Muitos de nós sabemos a correspondência entre lógica combinatória e cálculo lambda . Mas nunca vi (talvez não tenha examinado o suficiente) o equivalente a "combinadores digitados", correspondendo ao cálculo lambda simplesmente digitado. Existe algo assim? Onde alguém poderia encontrar informações sobre isso?

Hugo Sereno Ferreira
fonte
Você pode estar interessado em The Reader Monad e Abstraction Elimination in The Monad.Reader, Edição 17 . A mônada do Reader (ou mais precisamente seu função aplicador) está intimamente relacionada ao SKI digitado.
Petr Pudlák

Respostas:

18

A completividade expressiva dos combinadores digitados em comparação com o cálculo lambda simplesmente digitado foi demonstrada . Para cada combinador não digitado, é necessário uma família inteira de combinadores digitados. Por exemplo, um tem

  • Euαα
  • Kα(βα)
  • Sα(βγ)(αβ(αγ))

para todas as combinações de tipos simples e γ .α,βγ

Em alternativa, basta pensar nos tipos como regimes de tipo (ou tipos polimórficos) e inseri-los em Haskell e voila: combinadores .

Dave Clarke
fonte
Nunca pensei no combinador agindo sobre uma mônada! É assim mesmo? S
Hugo Sereno Ferreira
Na verdade, eu tenho sido apontado que corresponde ao operador de Applicative Functores, e o K . S<*>pureK
Hugo Sereno Ferreira
é bastante fundamental, portanto poderia corresponder a muitas coisas. S tem o mesmo tipo que a função mônade um p para functor Λ X . ct X . SSumapΛX.αX
Dave Clarke