Tipi Haskell per funzioni

Hm, beh per il primo è perché diciamo che f f era ben digitato. Stiamo applicando f quindi deve essere una funzione. Le funzioni hanno il tipo f : A -> B per alcuni A e B . Poiché f è anche l'argomento, deve essere anche il caso che f : A . Ciò significa che A = A -> B . Inoltre, poiché f = f f , il tipo di f f è anche il tipo di f . Poiché f f : B significa f : B . Ciò significa che A = B e quindi f : A -> A e A -> A = A come richiesto.

Per il secondo, qual è il tipo di * ? Questa è la chiave per comprendere il tipo di queste funzioni poiché applichiamo * all'input. In Haskell * :: Num a => a -> a -> a , che deve significare che le nostre funzioni hanno il tipo Num a -> a -> B per qualche B . Ti lascio capire da lì:)

Ci sono un paio di livelli alla tua prima domanda. Per inciso, tuttavia, ti consiglio di imparare a conoscere unification se non sei già familiare con esso in quanto è una parte fondamentale della comprensione del controllo di tipo e dell'inferenza di tipo.

Per digitare check selfApply fornisci provvisoriamente f il tipo a che risolviamo per. (A questo punto è solo una variabile di unificazione, la differenza chiave tra il controllo del tipo di Hindley-Milner e il controllo del tipo per i tipi semplici è che generalizzeremo (quantificeremo sopra) tutte le variabili non associate alla fine.) Poiché stiamo usando f come funzione sappiamo a = b -> c per le nuove variabili b e c . Poiché applichiamo f a qualcosa di tipo a , ovvero f stesso, sappiamo b = a . Non c'è alcun vincolo su c , quindi è corretto essere confusi sulla risposta fornita poiché f non è richiesto per essere a e a -> a e potrebbe effettivamente essere a e a -> a -> a o a e a -> Bool pure. Naturalmente, come sicuramente capisci, il problema è risolvere l'equazione a = a -> c . Nel tentativo di unificare questi con unificazione tradizionale, falliremo ciò che è noto come il controllo dei casi. Questo controllo è per evitare termini infiniti. L'unificazione razionale degli alberi è, tuttavia, un modo per affrontare questo problema e porta a tipi equi-ricorsivi. Haskell non supporta intenzionalmente i tipi equi-ricorsivi, ma O'Caml, ad esempio, fa con il flag -rectypes . Per convalidare che c è gratuito, possiamo usare un tipo iso -recursive, cioè:

data X c = X (X c -> c)
selfApply f = f (X f)

che scriverà check, e, in particolare, selfApply :: (X c -> c) -> c .

Ci sono due ragioni per cui Haskell (e quasi tutti i linguaggi polimorfici) non supportano i tipi equi-recursivi. Innanzitutto, in modo pragmatico, molti errori di tipo si presentano come tipi infiniti e se i tipi equi-recursivi erano supportati (tacitamente), si sarebbero trasformati in guasti ma avrebbero scritto programmi corretti. Più filosoficamente, la messa al bando dei tipi equi-recursivi e di cose simili era esattamente il motivo per cui i sistemi di tipo furono originariamente inventati risalendo fino a Bertrand Russell.