Perché utilizziamo le pieghe per codificare i tipi di dati come funzioni?

Question

O per essere precisi, perché usiamo foldr per codificare le liste e l'iterazione per codificare i numeri?

Scusate per l'introduzione a lungo termine, ma non so davvero come nominare le cose che voglio chiedere, quindi prima dovrò dare un po 'di esposizione. Questo richiama pesantemente lo this C.A.McCann post che non soddisfa proprio la mia curiosità e mi occuperò anche dei problemi con rank-n-types e infinite cose pigre.

---

Un modo per codificare tipi di dati come funzioni è quello di creare una funzione di "pattern matching" che riceve un argomento per ogni caso, ogni argomento essendo una funzione che riceve i valori corrispondenti a quel costruttore e tutti gli argomenti ritorno uno stesso tipo di risultato.

Questo tutto funziona come previsto per i tipi non-ricorsivi

--encoding data Bool = true | False 
type Bool r = r -> r -> r 

true :: Bool r 
true = \ct cf -> ct 

false :: Bool r 
false = \ct cf -> cf 

--encoding data Either a b = Left a | Right b 
type Either a b r = (a -> r) -> (b -> r) -> r 

left :: a -> Either a b r 
left x = \cl cr -> cl x 

right :: b -> Either a b r 
right y = \cl cr -> cr y 

Tuttavia, la bella analogia con il modello di corrispondenza rompe con tipi ricorsivi. Potremmo essere tentati di fare qualcosa di simile

--encoding data Nat = Z | S Nat 
type RecNat r = r -> (RecNat -> r) -> r 
zero = \cz cs -> cz 
succ n = \cz cs -> cs n 

-- encoding data List a = Nil | Cons a (List a) 
type RecListType a r = r -> (a -> RecListType -> r) -> r 
nil = \cnil ccons -> cnil 
cons x xs = \cnil ccons -> ccons x xs 

ma non siamo in grado di scrivere quelle definizioni ricorsive di tipo in Haskell! La solita soluzione consiste nel forzare il callback del caso cons/succ a essere applicato a tutti i livelli di ricorsione invece del solo primo (cioè, scrivere un fold/iteratore). In questa versione si usa il tipo di ritorno r cui il tipo ricorsiva sarebbe:

--encoding data Nat = Z | S Nat 
type Nat r = r -> (r -> r) -> r 
zero = \cz cf -> cz 
succ n = \cz cf -> cf (n cz cf) 

-- encoding data List a = Nil | Cons a (List a) 
type recListType a r = r -> (a -> r -> r) -> r 
nil = \z f -> z 
cons x xs = \z f -> f x (xs z f) 

Mentre questa versione funziona, rende definire alcune funzioni molto più difficile. Ad esempio, scrivere una funzione "coda" per gli elenchi o una funzione "predecessore" per i numeri è banale se è possibile utilizzare la corrispondenza dei modelli, ma diventa complicato se invece è necessario utilizzare le pieghe.

Così sulle mie vere domande:

1. Come possiamo essere sicuri che la codifica utilizzando pieghe è potente come il "pattern matching codifica" ipotetica? C'è un modo per prendere una definizione di funzione arbitraria tramite la corrispondenza del modello e convertirla meccanicamente in una sola utilizzando invece le piegature? (In tal caso, ciò contribuirebbe anche a rendere meno magiche definizioni come tail o foldl in termini di foldr e meno magico)

2. Perché il sistema di tipi Haskell non consente i tipi ricorsivi necessari nella "corrispondenza di modello" la codifica?. C'è una ragione per consentire solo tipi ricorsivi in ​​tipi di dati definiti tramite data? Il pattern matching è l'unico modo per consumare direttamente i tipi di dati algebrici ricorsivi? Ha a che fare con l'algoritmo di inferenza del tipo?

Answer 1

La pagina di Wikipedia su Scott encoding ha alcuni spunti utili. Il corto la versione è, quello a cui ti riferisci è la codifica di Church, e la tua "ipotetica codifica di pattern-match" è la codifica di Scott: entrambi sono modi sensati di fare le cose, ma la codifica di Church richiede macchine di tipo più leggero da usare (in particolare, non richiede tipi ricorsivi)

La prova che i due sono eq uivalent utilizza la seguente idea:

churchfold :: (a -> b -> b) -> b -> [a] -> b 
churchfold _ z [] = z 
churchfold f z (x:xs) = f x (churchfold f z xs) 

scottfold :: (a -> [a] -> b) -> b -> [a] -> b 
scottfold _ z [] = z 
scottfold f _ (x:xs) = f x xs 

scottFromChurch :: (a -> [a] -> b) -> b -> [a] -> b 
scottFromChurch f z xs = fst (churchfold g (z, []) xs) 
where 
    g x ~(_, xs) = (f x xs, x : xs) 

L'idea è che, poiché churchfold (:) [] è l'identità su liste, possiamo usare una piega Chiesa che produce la lista degli argomenti è dato, così come il risultato che dovrebbe produrre. Quindi nella catena x1 `f` (x2 `f` (... `f` xn) ...) il più esterno f riceve una coppia (y, x2 : ... : xn : []) (per alcuni non ci interessa), quindi restituisce f x1 (x2 : ... : xn : []). Ovviamente, deve anche restituire x1 : ... : xn : [] in modo che anche altre applicazioni di f funzionino.

(Questo è in realtà un po 'simile alla dimostrazione del principio matematico di strong (or complete) induction, dal "debole" o al solito principio di induzione).

A proposito, il tuo tipo Bool r è un po 'troppo grande per i veri booleani della Chiesa - ad es. (+) :: Bool Integer, ma (+) non è veramente un booleano della Chiesa. Se si abilita RankNTypes, è possibile utilizzare un tipo più preciso: type Bool = forall r. r -> r -> r. Ora è costretto a essere polimorfico, quindi ne contiene solo due (ignorando gli abitanti di seq e di fondo) - \t _ -> t e \_ f -> f. Idee simili si applicano anche agli altri tipi di Chiesa.

Answer 2

Dato un certo tipo di dati induttivo

data Nat = Succ Nat | Zero 

possiamo considerare come pattern matching su questi dati

case n of 
    Succ n' -> f n' 
    Zero -> g 

dovrebbe essere ovvio che ogni funzione del tipo Nat -> a può essere definita da dando un appropriato f e g e che l'unico modo per fare un Nat (in basso a fondo pagina) sta usando uno dei due onstructors.

---

MODIFICA: pensare a f per un momento. Se stiamo definendo una funzione e g in modo tale che f chiama in modo ricorsivo foo di quanto possiamo ridefinire f come f' n' (foo n') tale che f' non è ricorsivo. Se il tipo a = (a',Nat) di quanto possiamo invece scrivere f' (foo n). Così, senza perdita di generalità

foo n = h $ case n 
       Succ n' -> f (foo n) 
       Zero -> g 

questa è la formulazione che rende il resto del mio post ha senso:

---

Quindi, possiamo quindi pensare l'istruzione case come l'applicazione di un "dizionario distruttore "

data NatDict a = NatDict { 
    onSucc :: a -> a, 
    onZero :: a 
} 

ora la nostra istruzione case da prima può diventare

h $ case n of 
     Succ n' -> onSucc (NatDict f g) n' 
     Zero -> onZero (NatDict f g) 

dato questo possiamo derivare

newtype NatBB = NatBB {cataNat :: forall a. NatDict a -> a} 

possiamo quindi definire due funzioni

fromBB :: NatBB -> Nat 
fromBB n = cataNat n (NatDict Succ Zero) 

e

toBB :: Nat -> NatBB 
toBB Zero = Nat $ \dict -> onZero dict 
toBB (Succ n) = Nat $ \dict -> onSucc dict (cataNat (toBB n) dict) 

possiamo dimostrare queste due funzioni sono testimone di un isomorfismo (fino accelerare e perdere il ragionamento) e quindi mostrare che

newtype NatAsFold = NatByFold (forall a. (a -> a) -> a -> a) 

(che è lo stesso come NatBB) è isomorfo a Nat

Possiamo usare la stessa costruzione con altri tipi, e dimostrare che i tipi di funzione risultanti sono ciò che vogliamo solo dimostrando che i tipi sottostanti sono isomorfi con ragionamento algebrico (e induzione).

Per quanto riguarda la seconda domanda, il sistema di tipi di Haskell si basa su tipi iso-ricorsivi non equi-recursivi. Questo è probabilmente dovuto al fatto che la teoria e l'inferenza del tipo sono più facili da elaborare con i tipi iso-ricorsivi, e hanno tutto il potere che impongono un po 'più di lavoro sulla parte dei programmatori.Mi piace affermare che è possibile ottenere i tipi di iso-ricorsiva senza aeree

newtype RecListType a r = RecListType (r -> (a -> RecListType -> r) -> r) 

ma a quanto pare GHCs ottimizzatore strozzatori su quelli a volte :(.