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 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  <  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

externa länkar