Programowanie funkcyjne/Procedury jeszcze wyższych rzędów

Wstęp

Jaka jest różnica między danymi i procedurami? W programowaniu funkcyjnym to rozróżnienie rozmywa się. Dane mogą być traktowane jak procedury --- każdy interpreter czy kompilator zamienia dane (kod źródłowy programu) na procedurę (wykonywalny program). Procedury wyższych rzędów operują na innych procedurach jak na danych. Tak więc procedury mogą być również danymi. Można by powiedzieć, że dane tym różnią się od procedur, że zawsze są podmiotem obliczeń, a nigdy nie są same wykonywane. Niniejszy wykład powinien Państwa przekonać, że wcale tak nie musi być.

Używając języka programowania nie widzimy, w jaki sposób zrealizowane są struktury danych, ani jak jest zrealizowane stosowanie procedur do argumentów. Łatwo sobie wyobrazić, że procedury mogą mieć postać kodu źródłowego lub częściowo skompilowanego, który jest interpretowany. Jak zobaczymy w tym wykładzie, również dane nie muszą być biernym przedmiotem obliczeń. Poznamy jedną z możliwych implementacji danych --- całkowicie proceduralną.

Poniżej pokazujemy, jak można zaimplementować podstawowe struktury danych korzystając jedynie z procedur wyższych rzędów.

Uwaga

Niniejszy wykład ma całkowicie charakter ćwiczenia umysłowego.

Struktury danych wcale nie są implementowane w opisany sposób, ani nie jest to najlepszy sposób ich implementacji. Jednak opisany sposób ich realizacji jest możliwy.

Celem tego ćwiczenia jest zilustrowanie w pełni zamiennego traktowania danych i procedur. Zdobywszy tę umiejętność, będziemy mogli wznieść się na wyższy poziom abstrakcji i tworzyć struktury, w których dane są przemieszane z procedurami. Jest to również dobre ćwiczenie rozwijające umiejętność posługiwania się procedurami wyższych rzędów.

Pokazane tutaj konstrukcje pochodzą z $\lambda$-rachunku, gdzie faktycznie mają zastosowanie. Służą one do zaimplementowania podstawowych typów danych i operacji na nich. Robi się to w ramach dowodu, że w $\lambda$-rachunku można zapisać dowolne funkcje obliczalne.

Wartości logiczne

Aby mówić o wartościach logicznych, potrzebujemy zaimplementować następujące pojęcia i konstrukcje językowe:

• prawdę i fałsz,
• wyrażenia warunkowe if-then-else,
• operacje logiczne: koniunkcję, alternatywę i negację.

Mamy dwie wartości logiczne: prawdę i fałsz. Wartość logiczną możemy reprezentować jako procedurę dwuargumentową, której wynikiem jest jeden z jej argumentów. W przypadku prawdy wybiera pierwszy, a w przypadku fałszu drugi argument.

let prawda x y = x;;
val prawda : 'a -> 'b -> 'a = <fun>

let falsz  x y = y;;
val falsz : 'a -> 'b -> 'b = <fun>

Wyrażenia warunkowe if-then-else możemy zrealizować za pomocą trójargumentowej procedury jesli. Jej pierwszym argumentem jest wartość logiczna, a dwa pozostałe argumenty to odroczone wartości. (Używamy tu odroczonych wartości bez spamiętywania, tak jak zostały one zaimplementowane w poprzednim wykładzie.) Procedura ta, w zależności od wartości warunku, wybiera jedną z odroczonych wartości i oblicza ją.

let jesli w k a = force (w k a);;
val jesli : ('a -> 'b -> unit -> 'c) -> 'a -> 'b -> 'c = <fun>

jesli prawda (lazy 1) (lazy 2);;
- : int = 1

Implementując koniunkcję i alternatywę korzystamy z następujących tożsamości:

• prawda $\wedge x\equiv x$,
• fałsz $\wedge x\equiv$ fałsz,
• prawda $\vee x\equiv$ prawda,
• fałsz $\vee x\equiv x$.

Negacja polega na zamianie rolami dwóch argumentów wartości logicznej.

let i x y  = x y falsz;;
val i : ('a -> ('b -> 'c -> 'c) -> 'd) -> 'a -> 'd = <fun>

let lub x y = x prawda y;;
val lub : (('a -> 'b -> 'a) -> 'c -> 'd) -> 'c -> 'd = <fun>

let nie x a b = x b a;;
val nie : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c = <fun>

jesli (lub falsz prawda) (lazy 1) (lazy 2);;
- : int = 1

Produkty kartezjańskie

Zaimplementujemu tutaj produkty kartezjańskie dwóch typów. Produkty kartezjańskie większej liczby typów i rekordy nie różnią się istotnie.

Aby mówić o produkcie musimy mieć:

• konstruktor pary para: 'a -> 'b -> ('a * `b),
• rzuty na współrzędne: p1: ('a * 'b) -> 'a i p2: ('a * 'b) -> 'b.

Jak można zaimplementować parę nie używając żadnej struktury danych? Jedyna para o jakiej możemy mówić, to para argumentów procedury. Nam jednak potrzebna jest para bez procedury. Możemy jednak zdefiniować parę argumentów bez procedury -- parę argumentów czekających na procedurę, której zostaną przekazane. To bedzie nasza proceduralna implementacja pary.

let para x y = function f -> f x y;;
val para : 'a -> 'b -> ('a -> 'b -> 'c) -> 'c = <fun>

Zauważmy, że rzutowanie jest bardzo proste. Wystarczy przekazać parze procedurę, która wybierze pierwszy lub drugi z argumentów, które otrzyma. Takie procedury już znamy, są to: prawda i falsz.

let p1 p = p prawda;;
val p1 : (('a -> 'b -> 'a) -> 'c) -> 'c = <fun>

let p2 p = p falsz;;
val p2 : (('a -> 'b -> 'b) -> 'c) -> 'c = <fun>

let p x = para 1 "ala" x;;
val p : (int -> string -> 'a) -> 'a = <fun>

p1 p;;
- : int = 1

p2 p;;
- : string = "ala"

Uwaga

Tajemniczy parametr x w powyższym przykładzie jest wynikiem zastosowania eta-konwersji i ma na celu uniknięcie wprowadzenia w typie p słabych zmiennych typowych. Jeśli Czytelnik nie widzi jego celowości, nie należy się tym przejmować.

Listy

Zaimplementujemy tutaj listy nieskończone. Listy skończone można łatwo zaimplementować jako pary: długość listy + lista nieskończona.

Listy nieskończone można reprezentować jako procedury jednoargumentowe. Argumentem takiej procedury może być liczba naturalna, indeks elementu listy, a jej wynikiem jest wartość elementu listy. (To jak zaimplementować liczby naturalne pokazujemy dalej.)

Musimy zaimplementować:

• konstruktor nieskończonej listy stałej,
• dołączenie danego elementu na początku danej listy,
• procedurę zwracającą pierwszy element (głowę) danej listy,
• procedurę zwracającą ogon danej listy.

let stala x n =  x;;
val stala : 'a -> 'b -> 'a = <fun>

let sklej h t n = if n = 0 then h else t (n-1);; 
val sklej : 'a -> (int -> 'a) -> int -> 'a = <fun>

let glowa l = l 0;;
val glowa : (int -> 'a) -> 'a = <fun>

let ogon l n = l (n + 1);;
val ogon : (int -> 'a) -> int -> 'a = <fun>

Liczby naturalne Churcha

Pozostały nam jeszcze liczby naturalne. (Rozszerzenie liczb naturalnych do całkowitych pozostawiamy jako ćwiczenie dla ambitnych czytelników. :-) Będziemy utożsamiać liczbę naturalną z liczbą iteracji zadanej funkcji. Dokładniej, liczbę $n$ implementujemy jako procedurę, której argumentem jest funkcja (nazwijmy ją $f$), a wynikiem $f^n$.

$n\equiv f\to f^n$

Używając tej analogii, zero reprezentujemy jako funkcję zwracającą identyczność, a jedynkę jako identyczność (na funkcjach).

let id x = x;;
val id : 'a -> 'a = <fun>

let compose f g = function x -> f (g x);;
val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b = <fun>

let zero f = id;;
val zero : 'a -> 'b -> 'b = <fun>

let jeden f x = f x;;
val jeden : ('a -> 'b) -> 'a -> 'b = <fun>

Dodawanie i mnożenie definiujemy korzystając z poniższych toższamości:

$f^{n+1}=f^n\circ f$

let inc n f = compose (n f) f;;
val inc : (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c = <fun>

$f^{m+n}=f^m\circ f^n$

let plus m n f = compose (m f) (n f);;
val plus : ('a -> 'b -> 'c) -> ('a -> 'd -> 'b) -> 'a -> 'd -> 'c = <fun>

$f^{m\cdot n}=(f^n{)}^m=m(f^n)=m(nf)=(m\circ n)f$

let razy = compose;;

Do celów testowych możemy używać następujących procedur konwertujących liczby proceduralne na int i odwrotnie:

let ile n = n (function x -> x + 1) 0;;
val ile : ((int -> int) -> int -> 'a) -> 'a = <fun>

let rec iterate n f =
  if n = 0 then id else compose (iterate (n-1) f) f;;
val iterate : int -> ('a -> 'a) -> 'a -> 'a = <fun>

ile (iterate 1000);;
- : int = 1000
 
let dwa x = plus jeden jeden x;;
val dwa : ('a -> 'a) -> 'a -> 'a = <fun>

ile (razy dwa dwa);;
- : int = 4      

Jak moglibyśmy odróżniać od siebie liczby naturalne Churcha? Podstawową operacją porównania jest tzw. test zera --- sprawdzenie, czy dana liczba jest równa zero. Szukamy więc takiej funkcji $f$, że $f^0=\text{<mrow data-mjx-texclass="ORD">id</mrow>}$ jest czymś istotnie innym, niż $f^i$ dla $i>0$. Taką funkcją może być n.p.: $f(x)=\text{<mrow data-mjx-texclass="ORD">falsz</mrow>}$. Wówczas $f^0$ prawda = prawda, natomiast $f^i$ prawda = falsz (dla $i>0$).

let test_zera x = x (function _ -> falsz) prawda;;
val test_zera : (('a -> 'b -> 'c -> 'c) -> ('d -> 'e -> 'd) -> 'f) -> 'f = <fun>

jesli (test_zera zero) (lazy 1) (lazy 2);;
- : int = 1      

Jak zmniejszyć daną liczbę $n$ o 1? Liczba $n$ to taki obiekt, który przekształca zadaną funkcję $f$ w funkcję $f^n$. Nie mamy jednak żadnego dostępu do tego jak $n$ to robi. Problem ten można przedstawić sobie tak: mając dane $n$, $f$ i $x$ należy obliczyć $f^{n-1}(x)$.

Rozważmy funkcję:

$g(a,b)=(b,fb)$

oraz ciąg:

$(g^i(x,x){)}_{i=0,\dots ,n}=((x,x),(x,fx),(fx,f^{2}x),\dots ,(f^{n-1}x,f^{n}x))$

Wystarczy więc z ostatniej pary w ciągu, $g^n(x,x)=(f^{n-1}x,f^{n}x)$ wydobyć pierwszą współrzędną. Można to zapisać tak:

let dec n f x = 
  let g (a, b) = (b, f b)
  in let (y, _) = n g (x, x) 
     in y;;
val dec:(('a*'b->'b*'c)->'d*'d->'e*'f)->('b->'c)->'d->'e      

lub tak, wykorzystując zaimplementowane przez nas produkty kartezjańskie:

let dec n f x = p1 (n (function p -> para (p2 p) (f (p2 p))) (para x x));;
val dec : (((('a -> 'b -> 'b) -> 'c) -> ('c -> 'd -> 'e) -> 'e) -> (('f -> 'f -> 'g) -> 'g) -> ('h -> 'i -> 'h) -> 'j) -> ('c -> 'd) -> 'f -> 'j = <fun>
 
ile (dec dwa);;
- : int = 1      

Odejmowanie to wielokrotne zmniejszanie o jeden:

let minus m n = (n dec) m;;
val minus : 'a -> (((('b * 'c -> 'c * 'd) -> 'e * 'e -> 'f * 'g) -> ('c -> 'd) -> 'e -> 'f) -> 'a -> 'h) -> 'h = <fun>

ile (minus dwa jeden);;
- : int = 1      

Zwróćmy uwagę, że nie mamy liczb ujemnych, a w wyniku odjęcia od mniejszej liczby większej otrzymujemy zawsze zero. Za pomocą odejmowania i testu zera można zaimplementować porównanie:

let wieksze m n = nie (test_zera (minus m n));;
val wieksze : 'a -> (((('b * 'c -> 'c * 'd) -> 'e * 'e -> 'f * 'g) -> ('c -> 'd) -> 'e -> 'f) -> 'a -> ('h -> 'i -> 'j -> 'j) -> ('k -> 'l -> 'k) -> 'm -> 'n -> 'o) -> 'n -> 'm -> 'o = <fun>

jesli (wieksze dwa jeden) (lazy 1) (lazy 2);;
- : int = 1

Abstrakcja rekurencji

Zastanowimy się teraz nad następującym problemem. Procedury fold_left i fold_right stanowią abstrakcję rekurencyjnego przetwarzanialist. Czy istnieje abstrakcja wszelkiej rekurencji? Nasze zadanie możemy sformułować tak: czy istnieje jedna konstrukcja, za pomocą której możemy zdefiniować dowolne procedury rekurencyjne, bez (dalszego) używania rekurencji? Odpowiedź brzmi: tak.

Jak można przerobić rekurencyjną definicję procedury na nierekurencyjną --- poprzez wprowadzenie dodatkowego parametru funkcyjnego. Zobaczmy to na przykładzie procedury obliczającej silnię. Procedura rekurencyjna ma postać:

let rec factorial n = 
  if n <= 1 then 
    1 
  else
    n * factorial (n - 1);;
val factorial : int -> int = <fun>

Jeżeli usuniemy słowo kluczowe rec, to wewnątrz definicji nie będziemy mogli wywoływać procedury factorial. Możemy jednak dodać dodatkowy parametr proceduralny fac i zamiast wywołania rekurencyjnego wywoływać procedurę przekazywaną przez ten parametr.

let factorial fac n = 
  if n <= 1 then 
    1 
  else 
    n * fac (n - 1);;
val factorial : (int -> int) -> int -> int = <fun>

Przyjrzyjmy się bliżej tak zdefiniowanej procedurze. Można powiedzieć, że przetwarza ona procedurę fac, która poprawnie liczy silnię dla liczb $0,1,\dots ,n$ na procedurę, która poprawnie liczy silnię dla liczb $0,1,\dots ,n+1$. Jeżeli natomiast fac byłoby procedurą poprawnie liczącą silnię dla wszystkich liczb naturalnych, to factorial fac również byłoby taką procedurą. Tak więc chcemy skonstruować procedurę obliczającą funkcję, która byłaby punktem stałym przekształcenia factorial. Będzie ona poprawnie liczyć silnię dla wszystkich liczb.

Szukamy więc czegoś, co się nazywa operatorem punktu stałego dla procedur przekształcających procedury w procedury. Czytelnicy zaznajomieni z Semantyką i weryfikacją programów zapewne zauważyli, że szukamy (w odpowiedniej dziedzinie) kresu górnego ciągu:

(function n -> $\perp$)
factorial (function n -> $\perp$)
factorial (factorial (function n -> $\perp$))
factorial (factorial (factorial (function n -> $\perp$)))
    $⋮$

Załóżmy, że f jest procedurą przekształcającą procedurę w procedurę (takiego samego typu). W pierwszym podejściu, moglibyśmy spróbować zdefiniować operator punktu stałego następująco:

let rec y f = f (y f);;
val y : ('a -> 'a) -> 'a = <fun>
 
let f = y factorial ;;
= factorial (y factorial) = factorial (factorial (y factorial)) = ...      

Jednak ze względu na "gorliwe" obliczanie arguemntów procedur w Ocamlu, argument procedury factorial jest obliczany przed jej zastosowaniem, co powoduje zapętlenie obliczenia. Aby uniknąć zapętlenia, należy uleniwić ten argument i wyliczać go tylko na żądanie. Oto drugie podejście do implementacji operatora punktu stałego:

let factorial fac n = 
  if n <= 1 then 
    1 
  else 
    n * (force fac (n - 1));;
val factorial : (int -> int) Lazy.t -> int -> int = <fun>
 
let rec y f = f (lazy (y f));;
val y : ('a lazy_t -> 'a) -> 'a = <fun>

let fac = y factorial ;;
val fac : int -> int = <fun>

Operator punktu stałego może być zastosowany nie tylko do obliczania silni. Za jego pomocą można każdą procedurę rekurencyjną zdefiniować bez używania rekurencji. Powiedzmy, że nasza procedura rekurencyjna nazywa się p. Należy w tym celu:

• zmienić nazwę definiowanej procedury, powiedzmy na p_y,
• dodać jej dodatkowy (pierwszy) parametr, nazwijmy go f,
• każde odwołanie rekurencyjne do procedury p zastąpić przez force f,
• zdefinować p jako y p_y.

Oto przykład zastosowania tej techniki do rekurencyjnej procedury obliczającej liczby Fibonacciego:

let fib_y f n = 
  if n <= 2 then 
    1
  else'
    (force f (n-1)) + (force f (n-2));;

let fib = y fib_y;;

Ćwiczenia

Ćwiczenia