Esiste un caso d'uso per `newtype T = MkT (T -> T)`?

Question

Il documento "System F with Type Equality Coercions" da Sulzmann, Chakravarty, e Peyton Jones illustra la traduzione di Haskell di newtype nel Sistema FC con il seguente esempio:

newtype T = MkT (T -> T) 

A quanto mi risulta, salvo unsafePerformIO, gli unici valori possibili di questo tipo sono MkT id e MkT undefined a causa della parametrricità. Sono curioso di sapere se ci sono alcuni usi effettivi per questa (o una definizione simile).

Answer 1

La parametrricità riguarda i valori dei tipi con variabili. T non ha variabili, quindi la parametrica non si applica. Infatti, T ha molti abitanti

ap :: T -> T -> T 
ap (MkT f) t = f t 

idT :: T 
idT = MkT id 

constT :: T 
constT = MkT $ \t -> MkT $ \_ -> t 

axiom_sT :: T 
axiom_sT = MkT $ \f -> MkT $ \g -> MkT $ \a -> (g `ap` a) `ap` (f `ap` a) 

Il tipo T è un'implementazione del Untyped Lambda Calculus, un sistema universale equivalente formale di alimentazione ad una macchina di Turing. Le tre funzioni sopra (più ap) formano il calcolo dello SKI, un sistema formale equivalente.

È possibile codificare qualsiasi tipo di dati Haskell in T. Si consideri il tipo per numeri naturali

data Nat = Zero | Succ Nat 

possiamo codificare Nat in T

church :: Nat -> T 
church Zero  = MkT $ \f -> MkT $ \x -> x 
church (Succ n) = MkT $ \f -> MkT $ \x -> f `ap` (church n) 

ora, si è parzialmente corretto però. In Haskell non c'è modo di scrivere la funzione inversa di questo (per quanto ne so). Il che è davvero un peccato. Sebbene sia possibile scrivere una sorta di psuedo inverso con il tipo T -> IO Nat. Inoltre, la mia comprensione è che l'ottimizzatore di GHC può morire su newtypes ricorsivo (qualcuno mi corregga se ho torto su questo, perché mi piacerebbe tornare a usarli).

Invece, il tipo

data T = MkT (T -> T) | Failed String 

con

ap (MkT f) a = f a 
ap (Failed s) _ = Failed s 

che è lambda calcolo con eccezioni, può essere utilizzato in modo completamente invertibile.

In conclusione, in un certo senso T non è affatto un tipo utile, ma in un altro senso è il tipo più utile di tutti.