Programowanie funkcyjne/Funktory: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Przemek (dyskusja | edycje)
Przemek (dyskusja | edycje)
Nie podano opisu zmian
Linia 176: Linia 176:
    '''end''';;
    '''end''';;
        
        
Możemy sobie wyobrazić trywialne morfizmy sygnatur <math>\sigma : S_1 \to S</math> i <math>\sigma' : S_2 \to S</math> oraz redukty
Możemy sobie wyobrazić trywialne morfizmy sygnatur <math> \sigma : S_1 \to S</math> i <math> \sigma' : S_2 \to S</math> oraz redukty
<math>\_{}_{|\sigma}:S \to S1</math> i <math>\_{}_{|\sigma'}:S \to S2</math>.
<math> \_{}_{|\sigma}:S \to S1</math> i <math> \_{}_{|\sigma'}:S \to S2</math>.
        
        
W pierwszym podejściu możemy zrobić to tak:
W pierwszym podejściu możemy zrobić to tak:

Wersja z 08:54, 27 lip 2006

Wstęp

Funktory to moduły sparametryzowane. Często jeden moduł importuje inne moduły.Skoro rozdzieliliśmy pojęcia interfejsu (sygnatury) i implementacji (struktury), to możemy zapisywać moduły korzystające z innych modułów w bardziej abstrakcyjny sposób. Jeżeli spojrzymy na sygnaturę jak na specyfikację wykorzystywanego modułu, to zgodnie z zasadą ukrywania informacji information hiding, istotne powinny być jedynie specyfikacjewykorzystywanych modułów, a nie ich implementacje. Podstawienie dowolnej implementacji spełniającej zadaną specyfikację/sygnaturę powinno dać pożądane rezultaty. Moduł taki możemy zapisać w postaci sparametryzowanej --- podajemy sygnatury parametrów, po podstawieniu w ich miejsce odpowiednich implementacji otrzymujemy wynikowy moduł.

Na funktory możemy też patrzeć jak na funkcje na strukturach --- przetwarzają one moduły parametry w moduły wynikowe.

Przykład: Kolejka priorytetowa. Na elementach kolejki musi być określony porządek liniowy.

type porownanie = Mniejsze | Rowne | Wieksze;;
  
module type PORZADEK_LINIOWY = 
  sig
    type t
    val porownaj : t -> t -> porownanie
  end;;
     

Kolejka priorytetowa powinna mieć sygnaturę postaci:

module type PRI_QUEUE_FUNC = functor (Elem : PORZADEK_LINIOWY) -> 
  sig
    exception EmptyQueue
    type elem = Elem.t
    type queue
    val empty : queue 
    val put : elem -> queue -> queue
    val min : queue -> elem
    val removemin : queue -> queue
  end;;
     

Zwróćmy uwagę na to, że typ queue jest abstrakcyjny,a elem nie.Ukrywamy w ten sposób strukturę kolejki. Natomiast cokolwiek będzie wiadome o typie Elem.tbędzie nadal wiadome o typie elem.Jest to konieczne z tego powodu, że inaczej nie bylibyśmy włożyć żadnego elementu do kolejki. Implementację kolejki priorytetowej możemy zrealizować w następujący sposób:

module PriQueue : PRI_QUEUE_FUNC =
  functor (Elem : PORZADEK_LINIOWY) -> 
  struct
    type elem = Elem.t
    exception EmptyQueue
    type queue = elem list
    let empty = []
    let rec put x q = 
      match q with 
        [] -> [x] |
        h::t -> if Elem.porownaj x h = Mniejsze then 
          x :: q
        else
          h::(put x t)
    let min q =
      match q with 
        [] -> raise EmptyQueue |
        h::_ -> h
    let removemin (q:queue) = 
      match q with 
        [] -> raise EmptyQueue |
        _::t -> t
  end;;
      

Kolejka priorytetowa liczb całkowitych może być zrealizowana w taki sposób:

module IntOrder : PORZADEK_LINIOWY = 
  struct
    type t = int
    let porownaj (x:int) (y:int) = 
      if x < y then Mniejsze else
      if x > y then Wieksze else Rowne
  end;;
  
module IntQueue = PriQueue (IntOrder);;
     

W module IntOrder struktura typu t jest jawna. Dzięki temu będzie wiadomo, że elementy kolejki są typu int. Innym podstawowym pojęciem związanym z porządkami liniowymi jest sortowanie.

module type SORTING = functor (Elem : PORZADEK_LINIOWY) -> 
  sig
    type elem = Elem.t
    val sortuj : elem list -> elem list
  end;;
     

Jeden z algorytmów sortowania, to heap-sort.

module HeapSort (PrQ : PRI_QUEUE_FUNC): SORTING = 
  functor (Elem : PORZADEK_LINIOWY) -> 
    struct
      type elem = Elem.t
      module PQ = PrQ (Elem)
      open PQ
      let rec wkladaj l =
        fold_left (fun h x -> put x h) empty l
      let rec wyjmuj q a = 
        if q = empty then 
          List.rev a 
        else
          wyjmuj (removemin q) (min q :: a)
      let sortuj l = wyjmuj (wkladaj l empty) []
    end;;
  
module Sortowanie = HeapSort (PriQueue);;
  
module S = Sortowanie (IntOrder);;
  
S.sortuj [1;7;3;6;5;2;4;8];;
      

Jak widać z powyższego przykładu, jeżeli będziemy zapisywać moduły w postaci funktorów, to będziemy z nich tworzyć łatwo wymienne elementy.

Funktory wyższych rzędów

Tak jak istnieją procedury wyższych rzędów, istnieją również funktory wyższych rzędów. Są to funktory, których parametrami i/lub wynikiem są funktory. Oto przykład, stanowiący kontynuację poprzedniego przykładu:

Przykład: Opierając się na sortowaniu możemy wprowadzić obliczanie mediany. Potrzebujemy do tego porządku liniowego i jakiegoś algorytmu sortowania.

module type MEDIANA = 
  functor (Elem : PORZADEK_LINIOWY) -> 
    sig
      type elem = Elem.t
      exception PustaLista
      val mediana : elem list -> elem
    end;;
  
module Mediana : functor (Sort : SORTING) -> MEDIANA = 
  functor (Sort : SORTING) -> 
    functor (Elem : PORZADEK_LINIOWY) -> 
      struct
        type elem = Elem.t
        exception PustaLista
        module S = Sort (Elem)
        let mediana l = 
          let s = S.sortuj l
          and n = List.length l
          in 
            if n = 0 then 
              raise PustaLista 
            else 
              List.nth s (n / 2)
      end;;
  
module M = Mediana (HeapSort (PriQueue)) (IntOrder);;
  
M.mediana [4;3;5;6;2;1;7];;
       

Przykład: Pomysł: Przestrzenie metryczne i grona przestrzeni.Funktory sklejające przestrzenie w grona oraz funktory określające sposoby łączenia gron w złożone przestrzenie metryczne.

Uzupełnić.


Morfizmy sygnatur i redukty

[Pominąć]

Morfizmy sygnatur, a w zasadzie związane z nimi kowariantnie redukty, możemy zapisać w postaci funktorów. Załóżmy, że mamy dane trzy sygnatury:

module type S1 = 
  sig
    type t1
    type t2
    val a : t1
    val b : t2
    val f : t1 -> t2
  end;;
  
module type S2 =
  sig
    type s1
    type s2
    val x : s1
    val y : s2
    val p : s1 -> s2
  end;;
  
module type S = 
  sig
    type t
    val v : t
    val m : t -> t
  end;;
      

Możemy sobie wyobrazić trywialne morfizmy sygnatur σ:S1S i σ:S2S oraz redukty _|σ:SS1 i _|σ:SS2.

W pierwszym podejściu możemy zrobić to tak:

module type M1 = functor (Sig : S) -> S1;;
module type M2 = functor (Sig : S) -> S2;;
  
module F1 : M1 = functor (Mod : S) ->
  struct
    open Mod
    type t1 = t
    type t2 = t
    let a = v
    let b = v
    let f = m
  end;;
  
module F2 : M2 = functor (Mod : S) ->
  struct
    open Mod
    type s1 = t
    type s2 = t
    let x = v
    let y = v
    let p = m
  end;;
      

Wówczas jednak tracimy część informacji. W szczególności, jeżeli złączymy dwa moduły będące wynikami zastosowania powyższych funktorów do tej samej struktury, to stracimy informację o tym, jakie składowe są sobie równe.

module Suma = functor (M : S) -> 
  struct
    include F1(M)
    include F2(M)
  end;;
  
module Test = 
  Suma(struct
    type t = int
    let v = 42
    let m i = i
  end);;
  
Test.a = Test.x;;
This expression has type Test.s1 but is here used with type Test.t1      

Uzyskaliśmy sumę rozłączną, w której te same elementy, ale pochodzące z różnych funktorów są całkowicie od siebie oddzielone.

Spróbujmy trochę inaczej zapisać powyższe funktory, tak, aby te same składowe były sobie równe. Dodatkowo, niech każdy funktor wprowadza też coś nowego.

module F1 = functor (Mod : S) ->
  struct
    open Mod
    type t1 = t
    type t2 = t
    let a = v
    let b = v
    let f = m
    let nowe1 = "42"
  end;;
  
module F2 = functor (Mod : S) ->
  struct
    open Mod
    type s1 = t
    type s2 = t
    let x = v
    let y = v
    let p = m
    let nowe2 = 42.0
  end;;
      

Teraz złączenie wyników obydwu funktorów nie będzie sumą rozłączną, ale "pushoutem".

module Pushout = functor (M : S) -> 
  struct
    include F1(M)
    include F2(M)
  end;;
  
module Test = 
  Pushout(struct
    type t = int
    let v = 42
    let m i = i
  end);;
  
Test.a = Test.x;;
- : bool = true      

Zastanówmy się chwilę o co bogatsza jest sygnatura tak zdefiniowanych funktorów. Czy sygnatura wynikowa jest bogatsza? W zasadzie nie, bo nie wiadomo nic konkretnego o strukturze wynikowych typów, czy wartości. Wiadomo natomiast jaki jest związek między argumentem funktora, a strukturą wynikową. Sam funktor jest mniej abstrakcyjny.

Laboratoria i ćwiczenia

Laboratoria i ćwiczenia do wykładu