FunAlg - manual

(* czy juz skonczono *)
let is_work_done : bool = true;;
(* podanie typu  ^^^^^^ opcjonalne *)

// ile jest piw w lodowce
let beers_to_drink = 17;;

// ile bedzie wypite
let beers_drinked_after_hour =
  if is_work_done (* czyli czy fajrant *) then
    beers_to_drink
  else
    0;;

# is_work_done : bool = true
# beers_to_drink : int = 17
# beers_drinked_after_hour : int = 17

Typy:

• unit - produkt zerowej ilosci skladnikow, jedyna wartosc: ().
• bool - wartosci logiczne: true, false.
• int - nieograniczone liczby calkowite: 0, -10...
• rat - nieograniczone liczby wymierne: 0/1, -125/7...
• char - znaki: 'a', '!'...
• string - napisy: "", "Hello world!"...

Funkcje wbudowane

Nazwa	Typ	Opis
Numeryczne
rand	unit => rat	losowa liczba wymierna z przedzialu <0, 1)
floor	rat => int	podloga z liczby wymiernej
rat_of_int	int => rat	konwersja liczby calkowitej w wymierna
Wejscie
read_bool	unit => bool	wartosc logiczna ("y"/"n")
read_int	unit => int	liczba calkowita
read_rat	unit => rat	liczba wymierna
read_char	unit => char	znak
read_str	unit => str	napis
Wyjscie
print_newline	unit => unit	nowy wiersz
print_bool	bool => unit	wartosci logiczna
print_int	int => unit	liczba calkowita
print_rat	rat => unit	liczba wymierna
print_char	char => unit	znak
print_str	str => unit	napis

Infixowe operatory wbudowane

Symbol	Typ(y)	Opis
+, -, *, /, %	int * int => int rat * int => rat int * rat => rat rat * rat => rat	plus, minus, razy, podzielic, modulo
^	int * int => rat rat * int => rat int * rat => rat rat * rat => rat str * str => str	potegowanie / konkatenacja napisow
||, &&, $$	bool * bool => bool	or, and, xor
=, <, >, <=, >=, <>	a * a => bool	porownanie dwoch wartosci dowolnego nie funkcyjnego typu
;	unit * a => a	wykonywanie krokowe

let _denote_ = _expr1_ in
  _expr2_

let trojka_wartosci = (4, 3, (true, ()));;

let pewne_wartosci =
  let (a, _, (_, b)) = trojka_wartosci in
    (a,b);;

# trojka_wartosci : int * int * (bool * unit) = (4, 3, (true, ()))
# pewne_wartosci : int * unit = (4, ())

Semantycznie definicja let a = b in c jest rozwijana do (&lambda a . c) b, gdzie typ argumentu a jest taki jak typ wyrazenia b.

Funkcje definiuje sie w nastepujacy sposob:

fun _denote_ : _type_ -> _expr_

Przykladowa definicja funkcji, a nastepnie jej aplikacja:

let my_not =
fun b : bool ->
  if b then
    false
  else
    true;;

let my_add =
fun (a, b) : int * int ->
  a + b;;

let my_true = my_not false;;

let my_two = my_add (1, 1);;

# my_not : bool => bool = FUN
# my_add : int * int => int = FUN
# my_true : bool = true
# my_two : int = 2

Bardziej zaawansowany przyklad, gdzie odpowiednia funkcja jest zwracana jako wynik:

let my_or =
fun b1 : bool ->
  if b1 then
    fun _ : bool -> true
  else
    fun b2 : bool -> b2;;

# my_or : bool => bool => bool = FUN

• _t1_ * _t2_ * ... * _tn_ - typ produktowy.
• _t1_ => _t2_ - typ funkcyjny, funkcje z _t1_ do _t2_.

int * string => bool * bool * (unit => string)

Strzalka => sklada sie w prawa strone, wiec a => b => c, to typ funkcji, ktore biora argument typu a i zwracaja funkcje b => c.

Typy mozna nazywac - definiowac:

type int_pairs = int * int;;

type bools_times_int_pairs = bool * int_pairs;;

let compose =
fun f : int => int ->
fun g : int => int ->
fun x : int ->
  f (g x);;

let imul =
fun a : int ->
fun b : int ->
  a * b;;

let inc =
fun a : int ->
  a + 1;;

let double = imul 2;;

let add_one_mul_by_two = compose double inc;;

# compose : (int => int) => (int => int) => int => int = FUN
# double : int => int = FUN
# add_one_mul_by_two : int => int = FUN

let rec _nazwa_ : _typ_ = _cialo_;;

Przyklad:

let rec silnia : int => int =
fun n : int ->
  if n = 0 then
    1
  else
    n * (silnia (n-1));;
    
let duzo = silnia 6;;

# silnia : int => int = FUN
# duzo : int = 720

Wtedy definicja: let rec f : t = e;; zamieniana jest w let f = Y (&lambda f . e);;.
Po aplikacji mamy f = (&lambda f . e) (Y (&lambda f . e)) ≈ (&lambda f . e) f, czyli to o co nam chodzilo.

type int_list =
  | Nil : unit
  | Cons : int * int_list;;

• int_list - typ list liczb calkowitych.
• Nil - funkcja typu unit => int_list.
• Cons - funkcja typu int * int_list => int_list.

Nil () to lista pusta, a Cons (head, tail) to lista o glowie head i ogonie tail.

Kluczowa wlasnoscia typow algebraicznych jest mozliwosc jednoznacznego ,,destruowania'' ich wartosci:

match _expr_ with
| _cons1_ _denote1_ -> _expr1_
  ...
| _consn_ _denoten_ -> _exprn_

Przyklad - liczenie dlugosci listy:

let rec length : int_list => int =
fun l : int_list ->
  match l with
  | Nil _ -> 0
  | Cons (_, t) -> inc (length t);;

# length : int_list => int = FUN

Przyklad:

type list [a] =
  | Nil : unit
  | Cons : a * list [a];;

type pair [a, b] = a * b;;

let is_empty [a] =
fun l : list [a] ->
  match l with
  | Nil _ -> true
  | Cons _ -> false;;

let bool_list = Nil [bool] ();;

let prawda = is_empty [bool] bool_list;;

# is_empty [a] : list [a] => bool = FUN
# bool_list : list [bool] = Nil ()
# prawda : bool = true

• fun l : list [a],
• bool_list = Nil [bool] (),
• is_empty [bool] bool_list.

Szczegolnie wazne sa polimorficzne funkcje rekurencyjne:

let rec length [a] : list [a] => int =
fun l : list [a] ->
  match l with
  | Nil _ -> 0
  | Cons (h, t) -> inc (length t);;

let jeden = length [bool] (Cons [bool] (true, Nil [bool] ()));;

# length [a] : list [a] => int = FUN
# zero : int = 1

Ponadto w pewnych sytuacjach porownywane sa typy. Rownosc na typach prostych, to rownosc strukturalna, wiec:

type typ [a] = unit;;

// typ [int] = typ [bool]

type typ [a] =
| Nic : unit;;

// typ [int] != typ [bool]
// typ [int] = typ [int]

Ponadto dostepna jest wartosc specjalna o nie funkcyjnym dzialaniu:

# raise [a] : string => a = FUN

Przykladowe zastosowanie:

let head [a] =
fun l : list [a] ->
  match l with
  | Nil _ -> raise [a] "Taking head of empty list"
  | Cons (h, _) -> h;;

# head [a] : list [a] => a = FUN

raise jest funkcja polimorficzna, aby dawalo sie dobrze okreslic typ nastepujacego wyrazenia:

let funkcja_pusta =
fun _ : int ->
  raise [char] "Ha, ha, ha ta funkcja jest wszedzie nieokreslona";;

# funkcja_pusta : int => char = FUN  

Niektore wbudowane funkcje i operatory w pewnych sytuacjach powoduja wywolanie funkcji raise. Typowy przyklad takiej sytuacji, to dzielnie przez zero.

• operatory logiczne, tam gdzie to ma sens sa leniwe (drugi argument or i and),
• oczywiscie if - then - else i match - with sa leniwe (jako wyrazenia),
• aby rekurencja sie kiedykolwiek konczyla aplikacja operatora punktu stalego Y jest leniwa.

let leniwa_fun =
fun x : unit => _typ_ =
  if chce_wyliczyc then
    let real_x = x () in
       ...
  else
    ...;;

let leniwa_appl = leniwa_fun (fun _ : unit -> x);;