firma di tipo difficile per le coppie di coppie invertite

Question

Diciamo che ho il seguente tipo di dati:

data D a b = D (a,b) (b,a) 

e voglio definire la seguente funzione su di esso:

apply f (D x y) = D (f x) (f y) 

Qual è la firma di tipo di apply?

Ecco alcuni esempi di f che sono a posto:

f :: a -> a -- OK 
f :: (a, b) -> (b, a) -- OK 
f :: (a, b) -> ((a, c), (b, c)) -- OK 

In tutti i casi di cui sopra, si finisce con un tipo valido D.

Ma questo non va bene:

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

Perché quando inviamo tale funzione tramite apply finiamo per dover tentare di costruire D (a,a) (b,b) che non è valido a meno che a = b.

Non riesco a trovare un tipo di firma per esprimere tutto questo? Inoltre, in generale, c'è un modo per fare in modo che GHC mi dica quali dovrebbero essere queste firme?

Fori tipizzati Edit:

Nel tentativo di trovare il tipo con fori digitati, ho provato la seguente:

x = apply _ (D (1::Int,'a') ('b',2::Int)) 

e ottenuto:

Found hole ‘_’ with type: (Int, Int) -> (b, b) 
Where: ‘b’ is a rigid type variable bound by 
      the inferred type of x :: D b b 

che sembra il fatto che io abbia delle sciocchezze come f :: (Int, Int) -> (b, b) chiaramente non funzionerà qui.

Answer 1

Più tipi si adattano a apply, ma l'((t, t) -> (b, b)) -> D t t -> D b b dedotto è il più ragionevole e utilizzabile. Le alternative stanno per essere più alto rango, quindi cerchiamo di consentire che l'estensione lingua:

{-# LANGUAGE RankNTypes #-} 

In primo luogo, possiamo fare apply id lavoro:

apply :: (forall a. a -> a) -> D a b -> D a b 
apply f (D x y) = D (f x) (f y) 

Tuttavia, ora id è l'solo funzione con che funziona con apply (tutte le funzioni totali di tipo forall a. a -> a sono uguali a id).

Ecco un altro tipo:

apply :: (forall a. a -> (c, c)) -> D a b -> D c c 
apply f (D x y) = D (f x) (f y) 

Ma anche questo ha un prezzo. Ora il f -s può essere solo funzioni costanti che ignorano i precedenti campi di D. Quindi, apply (const (0, 0)) funziona, ma non abbiamo modo di esaminare l'argomento di f.

Al contrario, il tipo dedotto è piuttosto utile. Possiamo esprimere trasformazioni con esso che guardano i dati reali contenuti in D.

A questo punto, potremmo chiederci: perché GHC deduce ciò che deduce? Dopo tutto, alcune funzioni funzionano con i tipi alternativi, ma non funzionano con il tipo predefinito. Potrebbe essere meglio talvolta dedurre tipi di livello superiore? Bene, questi tipi sono spesso estremamente utili, ma dedurli non è fattibile.

L'inferenza di tipo per i tipi di rango 2 è piuttosto complicata, e non molto pratica, perché non è possibile dedurre i tipi più generali. Con inferenza di grado 1, possiamo dedurre un tipo che è più generale di tutti gli altri tipi validi per la stessa espressione. Non c'è una simile garanzia con i tipi rank-2. E l'inferenza per i tipi di rango 3 e sopra è solo undecidable.

Per questi motivi, GHC si attacca all'inferenza di classifica 1, quindi non deduce mai i tipi con gli argomenti delle funzioni di forall-s.

Answer 2

Prendere le cose agli estremi di generalità, vogliamo un tipo che assomiglia

apply :: tf -> D a b -> D c d 

dove tf rappresenta il tipo di f. Al fine di applicare f-(a,b) e ottenere (c,d), abbiamo bisogno

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

Al fine di applicare f-(b,a) per ottenere (d,c), abbiamo bisogno

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

Se accendiamo TypeFamilies (o GADTs) abbiamo ottenere il vincolo magico di cui abbiamo bisogno per esprimere quello:

{-# LANGUAGE TypeFamilies #-} 

apply :: (((a,b) -> (c,d)) ~ tf, 
      ((b,a) -> (d,c)) ~ tf) => 
     tf -> D a b -> D c d 

Sospetto che questo sia uno dei tipi più generali disponibili. Sfortunatamente, è piuttosto selvaggio; il fatto di capire se una determinata applicazione supererà il controllo del tipo non è sempre così facile. Si noti inoltre che per ragioni che personalmente non capisco, non è possibile definire in modo affidabile utilizzando specializzazioni

apply' :: ... 
apply' = apply 

Al contrario, è a volte necessario utilizzare

apply' f = apply f