Anamorfism
Inom datorprogrammering är en anamorfism en funktion som genererar en sekvens genom upprepad tillämpning av funktionen på dess tidigare resultat. Du börjar med något värde A och applicerar en funktion f på det för att få B. Sedan tillämpar du f på B för att få C, och så vidare tills något avslutande villkor uppnås. Anamorfismen är den funktion som genererar listan över A, B, C, etc. Du kan tänka på anamorfismen som att det initiala värdet utvecklas till en sekvens.
Ovanstående lekmans beskrivning kan anges mer formellt i kategoriteorin : anamorfismen av en koduktiv typ betecknar tilldelningen av en koalgebra till dess unika morfism till en endofunctors slutliga koalgebra . Dessa objekt används i funktionell programmering när de utvecklas .
Den kategoriska dubbla (aka motsatsen) av anamorfismen är katamorfismen .
Anamorfismer i funktionell programmering
Inom funktionell programmering är en anamorfism en generalisering av begreppet utspelar sig på koduktiva listor . Formellt är anamorfismer generiska funktioner som kan korkursivt konstruera ett resultat av en viss typ och som parametriseras av funktioner som bestämmer nästa steg i konstruktionen.
Datatypen i fråga definieras som den största fixpunkten ν X . FX för en funktion F . Genom den universella egenskapen hos slutliga koalgebra finns det en unik koalgebramorfism A → ν X . FX för vilken annan F -koalgebra som helst a : A → FA . Således kan man definiera funktioner från en typ A _till_ en koduktiv datatyp genom att specificera en koalgebrastruktur a på A .
Exempel: Potentiellt oändliga listor
Som ett exempel anges typen av potentiellt oändliga listor (med element av ett fast typvärde ) som fixpunkten [värde] = ν X . värde × X + 1 , dvs en lista består antingen av ett värde och en ytterligare lista, eller så är den tom. En (pseudo-) Haskell -Definition kan se ut så här:
data [ värde ] = ( värde : [ värde ]) | []
Det är den fixerade punkten för funktions F-värdet
, där:
data Kanske a = Bara en | Ingenting data F värde x = Kanske ( värde , x )
Man kan enkelt kontrollera att typen [värde] verkligen
är isomorf till F-värde [värde]
, och därför är [värde]
den fasta punkten. (Också observera att i Haskell sammanfaller de minsta och största fasta punkterna för funktorer, därför är induktiva listor desamma som koduktiva, potentiellt oändliga listor.)
Anamorfismen för listor (då vanligtvis känd som unfold ) skulle bygga en (potentiellt oändlig ) lista från ett tillståndsvärde. Vanligtvis tar utvikningen ett tillståndsvärde x
och en funktion f
som ger antingen ett par av ett värde och ett nytt tillstånd, eller en singelton för att markera slutet på listan. Anamorfismen skulle sedan börja med ett första frö, beräkna om listan fortsätter eller slutar, och i händelse av en icke-tom lista, lägga det beräknade värdet i förväg till det rekursiva anropet till anamorfismen.
En Haskell-definition av en unfold, eller anamorfism för listor, kallad ana
, är följande:
ana :: ( tillstånd -> Kanske ( värde , tillstånd )) -> tillstånd -> [ värde ] ana f stateOld = case f stateOld of Nothing -> [] Just ( värde , stateNew ) -> värde : ana f stateNew
Vi kan nu implementera ganska allmänna funktioner med ana , till exempel en nedräkning:
0
f :: Int -> Kanske ( Int , Int ) f current = låt enSmaller = ström - 1 in om enSmaller < då Inget annat Bara ( enSmaller , enSmaller )
Denna funktion kommer att minska ett heltal och mata ut det samtidigt, tills det är negativt, då det markerar slutet på listan. På motsvarande sätt ana f 3
att beräkna listan [2,1,0]
.
Anamorfismer på andra datastrukturer
En anamorfism kan definieras för vilken rekursiv typ som helst, enligt ett generiskt mönster, som generaliserar den andra versionen av ana för listor.
Till exempel utvecklas för träddatastrukturen
dataträd a = Blad a | _ Gren ( Träd a ) a ( Träd a )
enligt följande
ana :: ( b -> Antingen a ( b , a , b )) -> b -> Träd a ana spola upp x = fall lossa x av Vänster a -> Blad a Höger ( l , x , r ) -> Gren ( ana unspool l ) x ( ana unspool r )
För att bättre se förhållandet mellan den rekursiva typen och dess anamorfism, notera att träd
och lista
kan definieras så här:
newtype Lista a = Lista { unCons :: Kanske ( a , List a )} newtype Träd a = Träd { unNode :: Antingen a ( Träd a , a , Träd a ))}
Analogin med ana
visas genom att döpa om b
i sin typ:
newtype Lista a = Lista { unCons :: Kanske ( a , List a )} anaList :: ( list_a -> Kanske ( a , list_a )) -> ( list_a -> Lista a ) newtype Tree a = Träd { unNode :: Antingen a ( Tree a , a , Tree a ))} anaTree :: ( tree_a -> Antingen a ( tree_a , a , tree_a )) -> ( tree_a -> Träd a )
Med dessa definitioner har argumentet till konstruktören av typen samma typ som returtypen för det första argumentet av ana
, med de rekursiva omnämnandena av typen ersatta med b
.
Historia
En av de första publikationerna som introducerade begreppet anamorfism i programmeringssammanhang var uppsatsen Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire, av Erik Meijer et al. , som var i sammanhanget med programmeringsspråket Squiggol .
Ansökningar
Funktioner som zip
och iterate
är exempel på anamorfismer. zip
tar ett par listor, säg ['a','b','c'] och [1,2,3] och returnerar en lista med par [('a',1),('b',2 ),('c',3)]. Iterate
tar en sak, x, och en funktion, f, från sådana saker till sådana saker, och returnerar den oändliga listan som kommer från upprepad tillämpning av f, dvs listan [x, (fx), (f (fx)), (f (f (fx))), ...].
zip ( a : as ) ( b : bs ) = if ( as == [ ] ) || ( bs == [] ) -- || betyder 'eller' sedan [( a , b )] annars ( a , b ) : ( zip som bs ) iterera f x = x : ( iterera f ( f x ))
För att bevisa detta kan vi implementera både med vår generiska unfold, ana
, med en enkel rekursiv rutin:
zip2 = ana unsp fin där fin ( as , bs ) = ( as == [] ) || ( bs == [] ) unsp (( a : as ), ( b : bs )) = (( a , b ),( as , bs )) iterate2 f = ana ( \ a -> ( a , f a ) ) ( \ x -> False )
I ett språk som Haskell är även de abstrakta funktionerna fold
, unfold
och ana
bara definierade termer, som vi har sett från definitionerna ovan.
Anamorfismer i kategoriteori
I kategoriteorin är anamorfismer den kategoriska dualen av katamorfismer (och katamorfismer är den kategoriska dualen av anamorfismer).
Det betyder följande. Antag att ( A , fin ) är en slutlig F -koalgebra för någon endofunktor F av någon kategori i sig själv. Således fin en morfism från A till FA , och eftersom den antas vara slutgiltig vet vi att närhelst ( X , f ) är en annan F -kolgebra (en morfism f från X till FX ), kommer det att finnas en unik homomorfism h från ( X , f ) till ( A , fin ), det vill säga en morfism h från X till A så att fin . h = Fh . f . Sedan för varje sådant f betecknar vi med ana f den unikt specificerade morfismen h .
Med andra ord har vi följande definierande samband, givet några fasta F , A och fin som ovan:
Notation
En notation för ana f som finns i litteraturen är . De använda fästena är kända som linsfästen , varefter anamorfismer ibland kallas linser .
Se även
- Morfism
- Morfismer av F-algebras
- Från en initial algebra till en algebra: Katamorfism
- En anamorfism följt av en katamorfism: Hylomorfism
- Utvidgning av idén om katamorfismer: Paramorfism
- Utvidgning av idén om anamorfismer: Apomorfism