Come faccio a dimostrare che un tipo Haskell è abitato da una sola funzione?

Question

In this answer, Gabriel Gonzalez mostra come mostrare che id è l'unico abitante di forall a. a -> a. Per fare ciò (nella più formale iterazione della dimostrazione), mostra che il tipo è isomorfo su () usando lo Yoneda lemma, e dal momento che () ha solo un valore in esso, quindi deve essere il tipo di id. Riassunto, la sua prova è in questo modo:

Yoneda dice:

Functor f => (forall b . (a -> b) -> f b) ~ f a 

Se a =() e f = Identity, questo diventa:

(forall b. (() -> b) -> b) ~() 

E poiché banalmente () -> b ~ b, il LHS è fondamentalmente il tipo di id.

Questo sembra un po 'un "trucco magico" che funziona bene per id. Sto cercando di fare la stessa cosa per un tipo di funzione più complesso:

(b -> a) -> (a -> b -> c) -> b -> c 

ma non ho idea da dove iniziare. So che è abitata da \f g x = g (f x) x, e se ignori le cose brutte ⊥/undefined, sono abbastanza sicuro che non ci sono altre funzioni di questo tipo.

Non credo che il trucco di Gabriel sarà immediatamente applicare qui in qualsiasi modo scelgo i tipi. Ci sono altri approcci (che sono ugualmente formali!) Con cui posso mostrare l'isomorfismo tra questo tipo e ()?

Answer 1

È possibile applicare sequent calculus.

breve esempio, con il tipo di a -> a, potremmo costruire termine come: \x -> (\y -> y) x, ma che normalizza ancora \x -> x che è id. Nel calcolo sequenziale il sistema proibisce di costruire prove "riducibili".

vostro tipo è (b -> a) -> (a -> b -> c) -> b -> c, in modo informale:

f: b -> a 
g: a -> b -> c 
x: b 
-------------- 
Goal: c 

E non ci sono molti modi per procedere:

apply g 

f: b -> a 
g: a -> b -> c 
x: b 
--------------- 
Subgoal0: a 
Subgoal1: b 


apply f 

f: b -> a 
g: a -> b -> c 
x: b 
--------------- 
Subgoal0': b 
Subgoal1: b 


-- For both 
apply x 

Così, alla fine, sembra che g (f x) x è l'unico abitante di quel tipo .

---

approccio Yoneda lemma, devono stare attenti a realtà hanno forall x!

(b -> a) -> (a -> b -> c) -> b -> c 
forall b a. (b -> a) -> b -> forall c. (a -> b -> c) -> c 

Let concentrato sulla fine:

(a -> b -> c) -> c ~ ((a,b) -> c) -> c 

Questo è isomorfo a (a, b), quindi tutto il tipo si riduce a

(b -> a) -> b -> (a, b) 

Prendere f = Compose (Reader b) (,b)

(b -> a) -> f a ~ f b ~ b -> (b,b) 

e che è unico prendendo HP a = (a,a) funtore:

b -> (b,b) ~ (() -> b) -> HP b ~ HP() ~() 

---

EDIT il primo approccio si sente un po 'più a mano ondulato, ma si sente in qualche modo più diretto: Dato il ristretto insieme di regole, come la prova può essere costruito, quante prove possiamo costruire?