I tipi di dati haskell sono co-algebre di default?

Question

Sto cercando di ottenere la mia testa intorno F-algebre, e this article fa un buon lavoro. Comprendo la nozione di una teoria della doppia categoria, ma sto facendo fatica a capire come le F-coalgebre (il doppio delle algebre F) si riferiscono a strutture dati pigre in Haskell.

F-algebre sono descritti con un endofunctor con la funzione: F a -> A, che ha un senso se si pensa di F a come espressione, e come il risultato della valutazione che l'espressione, come l'articolo collegato spiega esso.

Essendo il duale di F-algebre, la funzione corrispondente di un F-coalgebra sarebbe un -> F a. Wikipedia dice che F-coalgebras può essere usato per creare strutture dati infinite e pigre. In che modo la funzione a>> F consente di creare strutture dati infinite e pigre? Inoltre, dato che Haskell si trova nel suo nucleo più pigro, la maggior parte dei tipi di dati sono in haskell F-coalgebras anziché in F-algebre? Le algebre F non sono ponderate?

Se i tipi di dati (o almeno quelli che sono capace di dati infinito) si basano su F-coalgebre a Haskell, qual è la a -> F una funzione per gli elenchi, per esempio? Qual è il terminale F-coalgebra per le liste?

Fare una lista infinita [1,2,3,4 ...] potrebbe apparire come questo in Haskell:

list = 1 : map (+ 1) list 

Questo uso F-coalgebre in qualche modo? Le strutture di dati infiniti richiedono una nozione di valutazione e ricorsione pigri oltre all'uso di F-coalgebras? Mi sto perdendo qualcosa qui?

Answer 1

Un coalgebra A -> F A può essere usato per staccarsi lo strato esterno di un (possibilmente infinito) struttura dati. Per le liste di X, il funtore è F a = Maybe (X, a), lo stesso che nella vista algebrico. In haskell la funzione per l'coalgebra è

headView :: [a] -> Maybe (a, [a]) 
headView [] = Nothing 
headView (x:xs) = Just (x,xs) 

unfoldr è il dispiegarsi corrispondente a questa coalgebra, proprio come foldr è la piega corrispondente a questo algebra.

Se si considera [a] non come il tipo di liste, ma come un tipo di descrizioni di liste o programmi, allora questo consente di costruire (apparentemente) valori infiniti, solo con una descrizione necessariamente finito.

Come si può vedere, un elenco Haskell sembra sia un F-algebra e un F-coalgebra. Questo è possibile perché Haskell non è realmente coerente. Puoi piegare uno spiegamento e ottenere un ciclo infinito. Linguaggi come coq e agda rendono esplicita la distinzione tra tipi di dati (algebre F) e tipi di codifica (F-coalgebre). In queste lingue ci sono due tipi di elenco, un algebriche List e coalgebraic Colist.