Construire une expression à partir d'un schéma de type

Question

Je suis donc demandé de trouver une expression du type:

(int -> ((int -> (bool -> int)) -> (bool -> int))) 

J'ai construit le code suivant pour produire (bool -> int) Cependant, il est la mise sur écoute de combinaison moi:

(%which (T) 
     (%typing '(lambda (f) 
        (lambda (x) 
         (succ (f (not x))))) 
       T)) 

Quelqu'un peut-il me dire de bonnes règles ou méthodes? :)

Answer 1

Il existe quelques outils pour dériver des implémentations de types (via la correspondance Curry/Howard). Un exemple est Djinn. Il y a an introduction, montrant comment, en général, générer des termes à partir de types.

Vous pourriez en apprendre davantage sur Curry-Howard et porter les outils de type à code vers Scheme?

Answer 2

Pour les détails de votre question (plutôt que les techniques générales), voici comment je pourrais aller à ce sujet:

(int -> ((int -> (bool -> int)) -> (bool -> int))) peut être simplifié à (A -> ((A -> B) -> B)) où A = int et B = (bool -> int). Cette version simplifiée est facile à construire:

(lambda (a) 
    (lambda (f) 
    (f a))) 

Il est facile de voir pourquoi cela fonctionne: a est de type A et f a le type (A -> B), afin d'appeler (f a) entraînera B. Pour mettre des types concrets à ces variables, a a le type int, f a le type (int -> (bool -> int)), et le résultat est, bien sûr, (bool -> int). Donc, maintenant vous devez trouver une fonction appropriée qui a le type (int -> (bool -> int)) pour insérer dans le paramètre f. Ceci est assez simple à faire un exemple:

(lambda (n) 
    (lambda (negate?) 
    ((if negate? - +) n))) 

Et voici comment vous pouvez utiliser ces fonctions:

> (define (foo a) 
    (lambda (f) 
     (f a))) 
> (define (bar n) 
    (lambda (negate?) 
     ((if negate? - +) n))) 
> (define baz ((foo 42) bar)) 
> (baz #t) 
-42 
> (baz #f) 
42 

Answer 3

Personnellement, je pense que ça devient un peu plus évident lorsque vous supprimez entre parenthèses redondantes de la le type (comme un non intrigant écrirait):

int -> (int -> bool -> int) -> bool -> int 

Alors vous êtes censé écrire une fonction qui est donnée trois arguments et renvoie un int . Autrement dit, une solution doit pouvoir être exprimée sous la forme suivante:

lambda n. lambda f. lambda b. ____ 

Mais comment remplir le trou? Eh bien, en regardant quels types vous obtenez à partir des paramètres, il est facile de voir que vous pouvez les brancher ensemble en appliquant f à n et b, ce qui donne un int. Donc:

lambda n. lambda f. lambda b. f n b 

C'est une solution.Mais en regardant le terme soigneusement on remarque que le lambda le plus intérieur peut effectivement être réduite eta, donnant un terme encore plus simple:

lambda n. lambda f. f n 

Mais en fait, la question est un dégénéré peu, parce que le retour d'un entier est toujours trivial . Donc, la solution est probablement plus simple:

lambda n. lambda f. lambda b. 0 

Le régime général d'arriver à une solution est souvent par une simple induction sur la structure du type: si vous avez besoin d'une fonction, puis écrire un lambda et procéder récursive avec le corps. Si vous avez besoin d'un tuple, écrivez un tuple et continuez récursivement avec ses composants. Si vous avez besoin d'un type primitif, vous pouvez simplement choisir une constante. Si vous avez besoin de quelque chose que vous n'avez pas (habituellement dans le cas polymorphe), cherchez certains des paramètres de la fonction dans la portée qui vous donnerait une telle chose. Si ce paramètre est lui-même une fonction, essayez de construire récursivement un argument approprié.

Answer 4

Ceci est la solution I recherche pour:

(lambda (i) (lambda (f) (lambda (b) (succ ((f (succ i)) (pas b))))))

qui peut être confirmée par: (% qui (T) (% tapant « (lambda (i) (lambda (f) (lambda (b) (succ ((f (succ i)) (pas b)))))) T))

Succ s'assure que c'est un nombre entier et non -> bool.