Dlaczego typy danych indukcyjnych zakazują typów takich jak "dane Bad a = C (Bad a -> a)", gdzie rekursja typu występuje przed ->?

Question

Agda instrukcja na Inductive Data Types and Pattern Matching stanów:

Aby zapewnić normalizację, zdarzenia indukcyjne muszą pojawić się w ściśle pozytywnych pozycjach. Na przykład, następujący typ danych nie jest dozwolone: ​​

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

ponieważ nie jest negatywnym zjawiskiem wśród złe argumentu konstruktora.

Dlaczego ten wymóg jest wymagany w przypadku indukcyjnych typów danych?

Answer 1

Typ danych dałeś jest wyjątkowy w tym, że jest osadzanie z bez typu rachunku lambda.

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

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

Zobaczmy, jak. Przypomnijmy, bez typu rachunek lambda ma następujące warunki:

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

Możemy zdefiniować tłumaczenie [[e]] od bez typu rachunek lambda warunkach dla Agda względem rodzaju Bad (choć nie w Agda):

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

Teraz może użyć twojego ulubionego, nie kończącego się bez dublującego terminu lambda, aby wytworzyć nie kończący się termin typu Bad. Na przykład, możemy przetłumaczyć (\x. x x) (\x. x x) do nie kończącej wypowiedzi typu Bad poniżej:

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

Chociaż typ okazał się być szczególnie wygodna forma dla tego argumentu, to może być uogólnione z odrobiną pracy do dowolnego typ danych z ujemnymi wystąpieniami rekursji.

Answer 2

Przykład, w jaki sposób taki typ danych pozwala nam zamieszkiwać w dowolnym typie, podany jest w Turner, D.A. (2004-07-28), Total Functional Programming, sect. 3.1, strona 758 w Zasada 2: Typ rekursji musi być kowariantna „

---

Zróbmy bardziej skomplikowany przykład używając Haskell Zaczniemy z.«Złego»rekurencyjne typu danych

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

.

i skonstruować Y combinator z niego bez innej postaci rekursji. oznacza to, że posiadanie takiego typu danych pozwala skonstruować każdy rodzaj rekursji lub zamieszkują dowolnego typu nieskończoną rekursji.

Y combinator w rachunku bez typu lambda jest definiowana jako

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

Kluczem do niej jest to, że możemy zastosować x sobie w x x. W językach pisanych maszynowo nie jest to bezpośrednio możliwe, ponieważ nie ma prawidłowego typu, który może mieć x. Ale nasz typ danych Bad Pozwala to modulo dodawania/usuwania konstruktora:

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

Biorąc x :: Bad a możemy rozpakować jego konstruktora i zastosować funkcję wewnątrz do x sama. Raz wiemy, jak to zrobić, to jest łatwe do skonstruowania 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 

Zauważ, że ani selfApp ani yc są rekurencyjne, nie ma rekurencyjne wywołanie funkcji do siebie. Rekursja pojawia się tylko w naszym rekurencyjnym typie danych.

Możemy sprawdzić, czy skonstruowany kombinator rzeczywiście robi to, co powinien. Możemy wykonać nieskończoną pętlę:

loop :: a 
loop = yc id 

lub obliczyć powiedzmy 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