diff --git a/task4/3.jpg b/task4/3.jpg new file mode 100644 index 0000000..0ccb90a Binary files /dev/null and b/task4/3.jpg differ diff --git a/task4/4-5.jpg b/task4/4-5.jpg new file mode 100644 index 0000000..54afee2 Binary files /dev/null and b/task4/4-5.jpg differ diff --git a/task4/church.ml b/task4/church.ml new file mode 100644 index 0000000..e1e05f0 --- /dev/null +++ b/task4/church.ml @@ -0,0 +1,143 @@ +(* Чёрч-кодирование пар. *) + +let pair = + fun x -> fun y -> fun projection -> projection x y + +let fst = + fun p -> p (fun x -> fun y -> x) + +let snd = + fun p -> p (fun x -> fun y -> y) + +let () = + let p = pair 3 42 in + fst p + |> Printf.printf "fst p: = %i\n" + + + +(* Чёрч-кодирование вариантов. *) + +let inl = + fun x -> fun case_1 -> fun case_2 -> case_1 x + +let inr = + fun x -> fun case_1 -> fun case_2 -> case_2 x + +(* Параметр with_ здесь только для вида, чтобы синтаксис в точке использования + был похож на OCaml. *) +let match_ = + fun x -> fun with_ -> fun case_1 -> fun case_2 -> x case_1 case_2 + +let with_ = + fun x -> x + +let _ = + let x = inr 3 in + match_ x with_ + (fun y -> y + 1) + (fun z -> z - 1) + |> Printf.printf "результат match_: %i\n" + +(* Для сравнение, то похожая программа, использующая встроенные варианты + OCamlа: *) +let _ = + let x = `Inr 3 in + (match x with + | `Inl y -> y + 1 + | `Inr z -> z - 1) + |> Printf.printf "результат match: %i\n" + + + +(* Чёрч-кодирование bool. *) + +(* Мы передаём case_true и case_false ненужную функцию (fun x -> x) только для + того, чтобы задержать вычисление case_true и case_false. OCaml использует + строгое вычисление. То есть, каждый аргумент полностью вычисляется перед тем, + как вызывается фунция. Ниже приведён пример без этого дополнительного + аргумента. *) +let true_ = + fun case_true -> fun case_false -> case_true (fun x -> x) + +let false_ = + fun case_true -> fun case_false -> case_false (fun x -> x) + +let if_ = + fun condition -> fun case_true -> fun case_false -> + condition case_true case_false + +let _ = + if_ true_ + (fun then_ -> print_endline "hello"; 3) + (fun else_ -> print_endline "world"; 42) + |> Printf.printf "результат if_: %i\n" + +let t_ = fun x -> true_ +let f_ = fun x -> false_ + +let and_ = + fun p -> fun q -> p (fun x -> q t_ f_) f_ + +let or_ = + fun p -> fun q -> p t_ (fun x -> q t_ f_) + +let (&&&) = and_ +let (|||) = or_ + +let _ = + if_ (true_ &&& true_) + (fun then_ -> "T") + (fun else_ -> "F") + |> Printf.printf "T & T = %s\n";; + if_ (true_ &&& false_) + (fun then_ -> "T") + (fun else_ -> "F") + |> Printf.printf "T & F = %s\n";; + if_ (false_ &&& true_) + (fun then_ -> "T") + (fun else_ -> "F") + |> Printf.printf "F & T = %s\n";; + if_ (false_ &&& false_) + (fun then_ -> "T") + (fun else_ -> "F") + |> Printf.printf "F & F = %s\n";; + + if_ (true_ ||| true_) + (fun then_ -> "T") + (fun else_ -> "F") + |> Printf.printf "T | T = %s\n";; + if_ (true_ ||| false_) + (fun then_ -> "T") + (fun else_ -> "F") + |> Printf.printf "T | F = %s\n";; + if_ (false_ ||| true_) + (fun then_ -> "T") + (fun else_ -> "F") + |> Printf.printf "F | T = %s\n";; + if_ (false_ ||| false_) + (fun then_ -> "T") + (fun else_ -> "F") + |> Printf.printf "F | F = %s\n";; + +(* Это более стандартное Чёрч-кодирование bool, но оно работает только в языке, + который не использует строгое вычисление. В OCaml, из-за строго вычисления, + это кодирование приводит к тому, что оба аргумента к if_lazy, и case_true и + case_false, полностью вычисляются, что вызывает побочные эффекты обоих, + несмотря на то, что в итоге только один из них будет выбран. *) + +let true_lazy = + fun case_true -> fun case_false -> case_true + +let false_lazy = + fun case_true -> fun case_false -> case_false + +let if_lazy = + fun condition -> fun case_true -> fun case_false -> + condition case_true case_false + +let _ = + if_lazy true_lazy + (print_endline "hello"; 3) + (print_endline "world"; 42) + |> Printf.printf "результат if_lazy': %i\n"