Nel pacchetto recursion-schemes possiamo esprimere il fatto che un (rigorosamente positivo) algebrico tipo di datiPerché un tipo algebrico dovrebbe essere solo un'algebra iniziale (o viceversa)?
- ha un funtore firma,
f - è l'iniziale
f-algebra e - è finale
f-coalgebra
per esempio, siamo in grado di farlo per [a] con il seguente codice
In particolare, per qualsiasi tipo in cui abbiamo (1), (2) e (3) dovremmo avere che (project, embed) testimoni di un isomorfismo.
Sono a conoscenza del fatto che i tipi di dati in generale (o almeno quelli strettamente positivi) sono sempre co/algebre finali/iniziali di qualche funzione di firma, infatti sono sempre entrambi.
Quindi la mia domanda è: perché avere Foldable e come classi separate? Quando un tipo di dati dovrebbe essere solo uno o l'altro?
Attualmente posso immaginare che questo potrebbe essere utile per i tipi di dati astratti che desiderano solo fornire un'interfaccia di piegatura o di apertura, ma ci sono anche altre volte?
Dobbiamo necessariamente definire algebra e coalgebra reciproca per qualsiasi tipo? Potrebbe essere possibile che per qualche tipo si voglia definire un'algebra che costruisce i valori e una coalgebra per elaborarli (e non solo decostruirli 'dualmente')? – didierc
Si potrebbe sicuramente, questo significherebbe che i tuoi dispieghi si dispiegano in un sottoinsieme di valori possibili e le pieghe "vedono" un sottoinsieme dei possibili dati - questo quasi certamente si verificherebbe in un tipo di dati astratto (altrimenti perché astratto?) . La mia lettura sui significati previsti di 'Foldable' /' Unfoldable' è che il functor 'Base' dovrebbe essere esattamente il funtore di firma del tipo e quindi sono reciproci. –
Mi sembra che 'Foldable' e' Unfoldable' stiano per esporre i tipi di dati come algebre e coalgebre rispettivamente, non necessariamente iniziali o finali. (Questo è probabilmente anche ciò che stava dicendo @didierc.) –