Tipo firme che non ha senso

Question

consideri

(a->a) -> [a] -> Bool 

Esiste una definizione significativo per questa firma? Questa è una definizione che non ignora semplicemente l'argomento?

x -> [a] -> Bool 

Sembra che ci siano molte firme di questo tipo che possono essere escluse immediatamente.

Answer 1

Carsten König ha suggerito in un commento per usare il teorema libero. Proviamoci.

Primo cannone

Iniziamo generating the free theorem corrispondente al tipo (a->a) -> [a] -> Bool. Questa è una proprietà che ogni funzione con quel tipo deve soddisfare, come stabilito dal famoso documento di Wadler Theorems for free!.

forall t1,t2 in TYPES, R in REL(t1,t2). 
forall p :: t1 -> t1. 
    forall q :: t2 -> t2. 
    (forall (x, y) in R. (p x, q y) in R) 
    ==> (forall (z, v) in lift{[]}(R). f_{t1} p z = f_{t2} q v) 

lift{[]}(R) 
    = {([], [])} 
    u {(x : xs, y : ys) | ((x, y) in R) && ((xs, ys) in lift{[]}(R))} 

Un esempio

Per comprendere meglio il teorema di cui sopra, corriamo più di un esempio concreto. Per utilizzare il teorema, dobbiamo prendere qualsiasi due tipi t1,t2, in modo che possiamo scegliere t1=Bool e t2=Int.

allora abbiamo bisogno di scegliere una funzione p :: Bool -> Bool (diciamo p=not), e una funzione q :: Int -> Int (diciamo q = \x -> 1-x).

Ora, dobbiamo definire una relazione R tra Bool s e Int s. Prendiamo la corrispondenza booleana standard < -> intera, ad es.:

R = {(False,0),(True,1)} 

(la precedente è una corrispondenza di uno a uno, ma non deve essere, in generale).

Ora dobbiamo controllare che (forall (x, y) in R. (p x, q y) in R). Abbiamo solo due casi per verificare la presenza di (x,y) in R:

Case (x,y) = (False,0): we verify that (not False, 1-0) = (True, 1) in R (ok!) 
Case (x,y) = (True ,1): we verify that (not True , 1-1) = (False,0) in R (ok!) 

Fin qui tutto bene. Ora dobbiamo "sollevare" la relazione in modo da lavorare sugli elenchi: ad es.

[True,False,False,False] is in relation with [1,0,0,0] 

Questa relazione estesa è quella denominata lift{[]}(R) sopra.

Infine, il teorema afferma che, per qualsiasi funzione f :: (a->a) -> [a] -> Bool dobbiamo avere

f_Bool not [True,False,False,False] = f_Int (\x->1-x) [1,0,0,0] 

cui sopra f_Bool rende semplicemente esplicita che f viene utilizzato nel caso in cui specializzata a=Bool.

Il potere di questo risiede nel fatto che non sappiamo quale sia il codice di f in realtà. Stiamo deducendo ciò che f deve soddisfare osservando solo il suo tipo polimorfico.

Da quando otteniamo tipi dall'inferenza di tipo e possiamo trasformare i tipi in teoremi, otteniamo veramente "teoremi gratis!".

Torna l'obiettivo originale

Vogliamo dimostrare che f non usa il suo primo argomento, e che non si preoccupa il suo argomento secondo elenco, sia, tranne che per la sua lunghezza.

Per questo, prendere R essere la relazione universalmente vera. Quindi, lift{[]}(R) è una relazione che mette in relazione due elenchi se hanno la stessa lunghezza.

Il teorema implica quindi:

forall t1,t2 in TYPES. 
forall p :: t1 -> t1. 
    forall q :: t2 -> t2. 
    forall z :: [t1]. 
    forall v :: [t2]. 
    length z = length v ==> f_{t1} p z = f_{t2} q v 

Quindi, f ignora il primo argomento e si preoccupa solo la lunghezza del secondo.

QED

Answer 2

Non è possibile fare nulla di interessante con x da solo.

can fare roba con [x]; ad esempio, puoi contare quanti nodi ci sono nella lista. Così, per esempio,

foo :: (a -> a) -> [a] -> Bool 
foo _ [] = True 
foo _ (_:_) = False 

bar :: x -> [a] -> Bool 
bar _ [] = True 
bar _ (_:_) = False 

Se si dispone di un e una funzione x che trasforma un x in qualcosa d'altro, si possono fare cose interessanti:

big :: (x -> Int) -> x -> Bool 
big f n = if f n > 10 then True else False 

Se x appartiene a qualche classe di tipo, quindi puoi usare tutti i metodi di quella classe su di esso. (. Questo è davvero uno speciale-caso della precedente)

double :: Num x => x -> x 
double = (2*) 

D'altra parte, ci sono un sacco di tipo firme per i quali non esistono funzioni valide:

magic :: x -> y 
magic = -- erm... good luck with that! 

ho letto da qualche parte che le firme di tipo che riguardano solo le variabili per le quali esiste una funzione reale sono esattamente i teoremi logici che sono veri. (Non so il nome per questa proprietà, ma è molto interessante.)

f1 :: (x -> y) -> x -> y 
-- Given that X implies Y, and given that X is true, then Y is true. 
-- Well, duh. 

f2 :: Either (x -> y) (x -> z) -> x -> Either y z 
-- Given that X implies Y or X implies Z, and given X, then either Y or Z is true. 
-- Again, duh. 

f3 :: x -> y 
-- Given that X is true, then any Y is true. 
-- Erm, no. Just... no.