Existe-t-il un calcul SKI tapé?

26

La plupart d'entre nous connaissent la correspondance entre la logique combinatoire et le calcul lambda . Mais je n'ai jamais vu (peut-être que je n'ai pas regardé assez profondément) l'équivalent de "combinateurs typés", correspondant au calcul lambda simplement tapé. Une telle chose existe-t-elle? Où trouver des informations à ce sujet?

Hugo Sereno Ferreira
la source
Vous pourriez être intéressé par The Reader Monad and Abstraction Elimination in The Monad.Reader, Numéro 17 . La monade Reader (ou plus précisément son foncteur applicatif) est étroitement liée au SKI typé.
Petr Pudlák

Réponses:

18

L'exhaustivité expressive des combinateurs typés par rapport au calcul lambda simplement typé a été démontrée . Pour chaque combinateur non typé, il faut toute une famille de combinateurs typés. Par exemple, on a

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

pour toutes les combinaisons de types simples et γ .α,βγ

Alternativement, considérez simplement les types comme des schémas de types (ou types polymorphes) et entrez-les dans Haskell et le tour est joué: combinateurs .

Dave Clarke
la source
Je n'ai jamais pensé que le combinateur agissait sur une Monade! Est-ce vrai? S
Hugo Sereno Ferreira
En fait, je l' ai fait remarquer que correspond à l' opérateur de Applicative Foncteurs, et le K . S<*>pureK
Hugo Sereno Ferreira
est assez fondamental, il pourrait donc correspondre à beaucoup de choses. S est du même type que la fonction de monade un p pour foncteur Λ X . alpha X . SSapΛX.αX
Dave Clarke