Digitare il combinatore Y

Question

http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html è una definizione concisa del calcolo lambda tipizzato in Prolog.

Sembra a posto, ma poi si pretende di assegnare un tipo alla Combinator Y ... mentre in un senso molto reale l'intero scopo di aggiungere tipi di lambda calcolo è quello di rifiutare di assegnare un tipo di cose come la Y combinatore.

Qualcuno può vedere esattamente dove il suo errore o - più probabilmente - il mio malinteso è?

Answer 1

Il combinatore Y, nella sua forma di base

Y f = (\x -> f (x x)) (\x -> f (x x)) 

solo non può essere digitato utilizzando il semplice sistema tipo proposto nell'articolo.

ci sono altri, molto più facile ma gli esempi significativi che non possono essere digitati a quel livello:

Prendete per esempio

test f = (f 1, f "Hello") 

questo funziona ovviamente per test (\x -> x), ma non possiamo dare il tipo più alto in classifica che è stato richiesto qui, vale a dire

test :: (∀a . a -> a) -> (Int, String) 

Ma anche in sistemi di tipo più avanzate come le estensioni GHCI di Haskell che permettono la sopra, Y è ancora difficile da digitare.

Quindi, data la possibilità di ricorsione, possiamo basta definire e lavoro utilizzando il fix combinatore

fix f = f (fix f) 

con fix :: (a -> a) -> a

Answer 2

Typing dovrebbe non consentire l'applicazione di sé, non dovrebbe essere possibile trovare un tipo per (t t). Se possibile, allora t avrebbe un tipo A -> B e avremmo A = A -> B. Dato che l'auto-applicazione fa parte del combinatore Y, non è nemmeno possibile dargli un tipo.

Sfortunatamente molti sistemi Prolog consentono una soluzione per A = A -> B. Ciò accade per molti motivi, o il sistema Prolog consente termini circolari, quindi l'unificazione avrà successo e le associazioni risultanti potranno essere ulteriormente elaborate. Oppure il sistema Prolog non consente termini circolari, quindi dipende dal fatto che implementa un controllo di verifica. Se il controllo di verifica è attivo, l'unificazione non avrà esito positivo. Se il controllo di verifica è disattivato, l'unificazione potrebbe avere esito positivo, ma i binding risultanti non possono essere ulteriormente elaborati, il che probabilmente porterà ad un overflow dello stack nella stampa o ad ulteriori unificazioni.

Quindi immagino che un'unificazione circolare di questo tipo si verifichi nel codice fornito dal sistema Prolog utilizzato e che non venga notata.

Un modo per risolvere il problema sarebbe quello di attivare il controllo di verifica o di sostituire una qualsiasi delle occorrenze unificate nel codice mediante una chiamata esplicita a unify_with_occurs_check/2.

Cordiali saluti

P.S.: Il seguente codice di prologo funziona meglio:

/** 
* Simple type inference for lambda expression. 
* 
* Lambda expressions have the following syntax: 
* apply(A,B): The application. 
* [X]>>A: The abstraction. 
* X: A variable. 
* 
* Type expressions have the following syntax: 
* A>B: Function domain 
* 
* To be on the save side, we use some unify_with_occurs_check/2. 
*/ 

find(X,[Y-S|_],S) :- X==Y, !. 
find(X,[_|C],S) :- find(X,C,S). 

typed(C,X,T) :- var(X), !, find(X,C,S), 
       unify_with_occurs_check(S,T). 
typed(C,[X]>>A,S>T) :- typed([X-S|C],A,T). 
typed(C,apply(A,B),R) :- typed(C,A,S>R), typed(C,B,T), 
       unify_with_occurs_check(S,T). 

Ecco alcune piste di esempio:

Jekejeke Prolog, Development Environment 0.8.7 
(c) 1985-2011, XLOG Technologies GmbH, Switzerland 
?- typed([F-A,G-B],apply(F,G),C). 
A = B > C 
?- typed([F-A],apply(F,F),B). 
No 
?- typed([],[X]>>([Y]>>apply(Y,X)),T). 
T = _T > ((_T > _Q) > _Q)