Church numerals: Difference between revisions
→{{header|OCaml}}: add extended Church functions...
m (→{{header|F Sharp|F#}}: fix heading, as suggested on the Count examples/Full list/Tier 4 talk page) |
GordonBGood (talk | contribs) (→{{header|OCaml}}: add extended Church functions...) |
||
Line 1,958:
=={{header|OCaml}}==
Original version by '''[http://rosettacode.org/wiki/User:Vanyamil User:Vanyamil]'''.
The extended Church functions as per the "RankNTypes" Haskell version have been added...
<lang OCaml>(* Using type as suggested in https://stackoverflow.com/questions/43426709/does-ocamls-type-system-prevent-it-from-modeling-church-numerals ▼
This is an
*)
(* Zero means apply f 0 times to x, aka return x *)
▲(* Using type as suggested in https://stackoverflow.com/questions/43426709/does-ocamls-type-system-prevent-it-from-modeling-church-numerals
let ch_zero : church_num = { f = fun _ -> fun x -> x }
▲ This is an explicitely polymorphic type : it says that f must be of type ('a -> 'a) -> 'a -> 'a for any possible a "at same time".
*)▼
▲type church_num = {f : 'a. ('a -> 'a) -> 'a -> 'a } ;;
(*
let
let f = fun f x -> x▼
(* The next numeral of a church numeral would apply f one more time *)
let ch_succ (
(* Adding m and n is applying f m times and then also n times *)
let ch_add (m : church_num) (n : church_num) : church_num =
(* Multiplying is repeated addition : add n, m times *)
let ch_mul (m : church_num) (n : church_num) : church_num =
(* Exp is repeated multiplication : multiply by base, exp times.
However, Church numeral n is in some sense the n'th power of a function f applied to x
So exp base = apply function base to the exp'th power = base^exp.
▲*)
▲let ch_exp (base : church_num) (exp : church_num) : church_num =
(* extended Church functions: *)
(* test function for church zero *)
let ch_is_zero (c : church_num) : church_num =
{ f = fun fn x -> c.f (fun _ -> fun _ -> fun xi -> xi) (* when argument is not ch_zero *)
(fun fi -> fi) (* when argument is ch_zero *) fn x }
(* church predecessor function; reduces function calls by one unless already church zero *)
let ch_pred (c : church_num) : church_num =
{ f = fun fn x -> c.f (fun g h -> h (g fn)) (fun _ -> x) (fun xi -> xi) }
(* church subtraction function; calls predecessor function second argument times on first *)
let ch_sub (m : church_num) (n : church_num) : church_num = n.f ch_pred m
(* church division function; counts number of times divisor can be recursively
subtracted from dividend *)
let ch_div (dvdnd : church_num) (dvsr : church_num) : church_num =
let rec divr n = (fun v -> v.f (fun _ -> (ch_succ (divr v)))
ch_zero) (ch_sub n dvsr)
in divr (ch_succ dvdnd)
(* conversion functions: *)
(* Convert a number to a church_num via recursion *)
Line 2,015 ⟶ 2,023:
then acc
else helper (n-1) (ch_succ acc)
in helper n ch_zero
(* Convert a church_num to an int is rather easy! Just +1 n times. *)
let int_of_church (n : church_num) : int = n.f succ 0
(* Now the tasks at hand: *)
Line 2,027 ⟶ 2,032:
(* Derive Church numerals three and four in terms of Church zero and a Church successor function *)
let ch_three =
let ch_four = ch_three |> ch_succ
Line 2,033 ⟶ 2,038:
let ch_7 = ch_add ch_three ch_four
let ch_12 = ch_mul ch_three ch_four
let ch_eleven = church_of_int 11
let ch_twelve = ch_eleven |> ch_succ
(* Similarly obtain 4^3 and 3^4 in terms of Church numerals, using a Church numeral exponentiation function *)
let ch_64 = ch_exp ch_four ch_three
let ch_81 = ch_exp ch_three ch_four
(* check that ch_is_zero works *)
(* Convert each result back to an integer, and return it or print it to the console *)▼
let ch_1 = ch_is_zero ch_zero
let ch_0 = ch_is_zero ch_three
[ch_three; ch_four; ch_7; ch_12; ch_64; ch_81] ▼
(* check church predecessor, subtraction, and division, functions work *)
let ch_2 = ch_pred ch_three
let ch_8 = ch_sub ch_eleven ch_three
let ch_3 = ch_div ch_eleven ch_three
let ch_4 = ch_div ch_twelve ch_three
let result = List.map (fun c -> string_of_int(int_of_church c))
ch_eleven; ch_twelve; ch_1; ch_0; ch_2; ch_8; ch_3; ch_4 ]
|> String.concat "; " |> Printf.sprintf "[ %s ]"
;;
print_endline result</lang>
{{out}}
<pre>[ 3; 4; 7; 12; 64; 81; 11; 12; 1; 0; 2; 8; 3; 4 ]</pre>
=={{header|Octave}}==
| |||