Perché i tipi di dati induttivi vietano tipi come "data Bad a = C (Bad a -> a)" dove la ricorsione del tipo si verifica davanti a ->?

Question

manuale Agda su Inductive Data Types and Pattern Matching paese:

Per garantire la normalizzazione, occorrenze induttivi deve apparire in posizioni strettamente positivi. Ad esempio, il seguente tipo di dati non è consentito:

data Bad : Set where 
    bad : (Bad → Bad) → Bad 

poiché non v'è un evento negativo di Bad nell'argomento al costruttore.

Perché è necessario questo requisito per i tipi di dati induttivi?

Answer 1

Il tipo di dati che hai dato è speciale in quanto si tratta di un radicamento del non tipizzata lambda calcolo.

data Bad : Set where 
    bad : (Bad → Bad) → Bad 

unbad : Bad → (Bad → Bad) 
unbad (bad f) = f 

Vediamo come. Ricordiamo, il lambda calcolo tipizzato ha questi termini:

e := x | \x. e | e e' 

possiamo definire una traduzione [[e]] da non tipizzata lambda termini di calcolo ai termini agda di tipo Bad (anche se non in Agda):

[[x]]  = x 
[[\x. e]] = bad (\x -> [[e]]) 
[[e e']] = unbad [[e]] [[e']] 

Ora puoi usare il tuo termine lambda non terminato preferito per produrre un termine non terminante di tipo Bad. Ad esempio, si potrebbe tradurre (\x. x x) (\x. x x) all'espressione non fatale di tipo Bad seguito:

unbad (bad (\x -> unbad x x)) (bad (\x -> unbad x x)) 

Anche se il tipo è accaduto a essere una forma particolarmente conveniente per questo argomento, può essere generalizzato con un po 'di lavoro a qualsiasi tipo di dati con occorrenze negative di ricorsione.

Answer 2

Un esempio di come un tipo di dati di questo tipo ci consente di abitare qualsiasi tipo viene fornito in Turner, D.A. (2004-07-28), Total Functional Programming, sez. 3.1, pagina 758 in Regola 2: Tipo di ricorsione deve essere covarianti "

---

Facciamo un esempio più elaborato utilizzando Haskell Inizieremo con una. 'Cattivo' ricorsivo tipo di dati

data Bad a = C (Bad a -> a) 

.

e costruire il Y combinator da esso senza qualsiasi altra forma di ricorsione. Ciò significa che avere un tale tipo di dati permette di realizzare qualsiasi tipo di ricorsione, o abitare qualsiasi tipo per una ricorsione infinita.

Il combinatore Y nel lambda calcolo tipizzato è definito come

Y = λf.(λx.f (x x)) (λx.f (x x)) 

La chiave è che applichiamo x a se stesso in x x. Nelle lingue digitate questo non è direttamente possibile, perché non esiste un tipo valido x. Ma il nostro tipo di dati Bad permette questo modulo aggiunta/rimozione costruttore:

selfApp :: Bad a -> a 
selfApp (x@(C x')) = x' x 

Facendo x :: Bad a, possiamo scartare suo costruttore e applicare la funzione all'interno di x stessa. Una volta che sappiamo come fare questo, è facile costruire il Combinator Y:

yc :: (a -> a) -> a 
yc f = let fxx = C (\x -> f (selfApp x)) -- this is the λx.f (x x) part of Y 
     in selfApp fxx 

Nota che né selfApp né yc sono ricorsivo, non v'è alcuna chiamata ricorsiva di una funzione a se stesso. La ricorsione appare solo nel nostro tipo di dati ricorsivo.

Possiamo controllare che il combinatore costruito faccia effettivamente ciò che dovrebbe. Possiamo fare un ciclo infinito:

loop :: a 
loop = yc id 

o calcolare diciamo GCD:

gcd' :: Int -> Int -> Int 
gcd' = yc gcd0 
    where 
    gcd0 :: (Int -> Int -> Int) -> (Int -> Int -> Int) 
    gcd0 rec a b | c == 0  = b 
        | otherwise = rec b c 
     where c = a `mod` b