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