Existe-t-il un calcul SKI tapé?

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?

reference-request logic lambda-calculus type-theory combinatory-logic 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:

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

$\mathbf{I}_{\alpha\to\alpha}$
$\mathbf{K}_{\alpha\to(\beta\to\alpha)}$
$\mathbf{S}_{\alpha\to(\beta\to\gamma)\to(\alpha\to\beta\to(\alpha\to\gamma))}$

pour toutes les combinaisons de types simples et . $\alpha,\beta$ $\gamma$

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

$\mathbf{S}$

Hugo Sereno Ferreira

En fait, je l' ai fait remarquer que

correspond à l' opérateur de Applicative Foncteurs, et le

S

$\mathbf{S}$ <*>pure

K

$\mathbf{K}$

Hugo Sereno Ferreira

est assez fondamental, il pourrait donc correspondre à beaucoup de choses.

est du même type que la fonction de monade

pour foncteur

S

$\mathbf{S}$

S

$\mathbf{S}$

a p

$ap$

Λ X . α \to X

$\Lambda X.\alpha\to X$

Dave Clarke