Simple Types cannot ban Curry Paradox? (Was: Honoring Raymond Smullyan)

Hi,
Although Simple Types can ban self application,
like making (x x) typeable is impossible. It cannot
completely ban the Curry Paradox,
since we can still derive:
?- between(1,16,N), search(typeof(X, [],
    ((a->(a->b))->(((a->b)->a)->b))), N, 0).
N = 15,
X = lam(lam(lam(0*(1*0))*lam(2*0*0))) .
This is a well known fact that in Minimal Logic
the Curry Paradox is still derivable. But what
about Affine Logic, can it ban the Curry Paradox?
I guess so, if Affine Logic ban contraction,
then Lambda Exprssions such as lam(0*(1*0)) and
lam(2*0*0) cannot be formed, since 0 apears twice.
But how rigorously show the conjecture that
Affine Logic bans the Curry Paradox?
Bye
Source code for the proof search with de Brujin
indexes, which requires a ternary typeof/3, since
we need also pass around a context L:
/* Implication Intro */
typeof(lam(Y), L, (A -> B)) :-
    typeof(Y, [A|L], B).
/* Axiom */
typeof(K, L, B) :-
    nth0(K, L, A),
    unify_with_occurs_check(A, B).
/* Modus Ponens */
typeof((S*T), L, B) :-
    typeof(S, L, (A -> B)),
    typeof(T, L, A).
search(true, N, N).
search((A,B), N, M) :-
    search(A, N, H),
    search(B, H, M).
search(typeof(P, L, T), N, M) :- N>0, H is N-1,
    clause(typeof(P, L, T), B),
    search(B, H, M).
search(unify_with_occurs_check(A,B), N, N) :-
    unify_with_occurs_check(A,B).
search(nth0(K, L, A), N, N) :-
    nth0(K, L, A).
Mild Shock schrieb:

Hi,
 Now you can listen to Bird songs for a minute:
 2016 Dana Scott gave a talk honoring Raymond Smullyan
https://www.youtube.com/watch?v=omz6SbUpFQ8
 A little quiz:
 Q: And also on the Curry-Howard Isomorphism. Is
there a nice way to put it in bird-forest form like To
Mock a Mocking Bird. This book made everything so
simple and intuitive for me.
 A: Hardly, because xx has no simple type.
 Right?
 Bye