Church numerals: Difference between revisions
Content added Content deleted
GordonBGood (talk | contribs) (→{{header|F#}}: Add a more complete set of Church functions with comments...) |
GordonBGood (talk | contribs) (→All closures and a union for type-punning: add more extensive Church functions and comments...) |
||
Line 1,088: | Line 1,088: | ||
===All closures and a union for type-punning=== |
===All closures and a union for type-punning=== |
||
Everything is an anonymous function, we dereference with a closure instead of a pointer,and the type-casting is hidden behind a union instead of behind a macro |
Everything is an anonymous function, we dereference with a closure instead of a pointer,and the type-casting is hidden behind a union instead of behind a macro; the following code implements more extended Church functions such as Church subtraction and division than the task requries: |
||
<lang nim>import sugar |
<lang nim>import sugar |
||
type |
|||
In = ()->int |
|||
Fn = In->In |
|||
Ch = Fn->Fn |
|||
Mc = Ch->Ch |
|||
MMc = Mc->Mc |
|||
Pun[T]{.union.} = object |
|||
down: T->T |
|||
up: (T->T)->(T->T) |
|||
#automatic type conversions: |
|||
func lift[T](f: T->T): (T->T)->(T->T) = |
|||
Pun[T](down: f).up |
|||
converter once(c: Ch): Mc = c.lift |
|||
converter twice(c: Ch): MMc = c.lift.lift |
|||
type # use a thunk closure as a data type... |
|||
let |
|||
In = () -> int # a lazy thunk producing an int |
|||
zero = proc(f: Fn): Fn {.closure.} = (x: In)=>x |
|||
Func = In -> In |
|||
ChurchFunc = Func -> Func |
|||
add = (c: MMc) => ((d: Ch) => c(succ)d) |
|||
MetaChurchFunc = ChurchFunc -> ChurchFunc |
|||
mul = (c: MMc) => ((d: Ch) => c(add d)zero) |
|||
MetaMetaChurchFunc = MetaChurchFunc -> MetaChurchFunc |
|||
Church = object # wrapping solves ambiquous infinite type problems! |
|||
chf: ChurchFunc |
|||
PredicateChurchFunc = ChurchFunc -> (ChurchFunc -> Func) |
|||
func makeChurch(chf: ChurchFunc): Church = Church(chf: chf) |
|||
func unChurch(ch: Church): ChurchFunc = ch.chf |
|||
type # type Kind conversions to/from... |
|||
one = zero.succ |
|||
Pun[T] {.union.} = object # does safer casting... |
|||
exp1 = (c: Ch) => ((d: MMc) => d(mul c)one) |
|||
down: T -> T |
|||
#alternatively: |
|||
up: (T -> T) -> (T -> T) |
|||
Wrap {.union.} = object |
|||
wrapped: ChurchFunc |
|||
preded: PredicateChurchFunc -> PredicateChurchFunc |
|||
func lift[T](f: T -> T): (T -> T) -> (T -> T) = Pun[T](down: f).up |
|||
func lower[T](f: (T -> T) -> (T -> T)): (T -> T) = |
|||
Pun[T](up: f).down |
|||
func liftpred(f: ChurchFunc): PredicateChurchFunc -> PredicateChurchFunc = |
|||
Wrap(wrapped: f).preded |
|||
let |
|||
zeroChurch: Church = makeChurch(func(_: Func): Func = ((t: In) => t)) |
|||
oneChurch: Church = makeChurch(func(f:Func): Func = f) |
|||
succChurch = func(ch: Church): Church = |
|||
result = makeChurch((f: Func) => ((x: In) => f(ch.unChurch()(f)x))) |
|||
addChurch = func(ach, bch: Church): Church = |
|||
#[ alternate... |
|||
let succ = proc(chf: ChurchFunc): ChurchFunc = |
|||
chf.makeChurch().succChurch().unChurch() |
|||
makeChurch(ach.unChurch.lift.lift()(succ)(bch.unChurch)) |
|||
# ]# |
|||
makeChurch((f: Func) => ((x: In) => |
|||
((ach.unChurch()f)(bch.unChurch()(f)x)))) |
|||
multChurch = func(ach, bch: Church): Church = |
|||
makeChurch((f: Func) => ach.unChurch()(bch.unChurch()(f))) |
|||
expChurch = proc(basech, expch: Church): Church = |
|||
makeChurch(expch.unChurch().lift()(basech.unChurch)) |
|||
isZeroChurch = proc(ch: Church): Church = |
|||
let zerof = proc(_: ChurchFunc): ChurchFunc = zeroChurch.unChurch |
|||
makeChurch(ch.unChurch.lift.lift()(zerof)(oneChurch.unChurch)) |
|||
predChurch = func(ch: Church): Church = |
|||
makeChurch(func(f: Func): Func = |
|||
# magic is here, reduces by one function... |
|||
let prd = (gf: ChurchFunc) => ((hf: ChurchFunc) => hf(gf(f))) |
|||
((x: Func) => |
|||
ch.unChurch.liftpred()(prd)((_: Func) => x)((t: Func) => t)).lower) |
|||
minusChurch = proc(ach, bch: Church): Church = |
|||
let pred = proc(chf: ChurchFunc): ChurchFunc = |
|||
chf.makeChurch().predChurch().unChurch() |
|||
makeChurch(bch.unChurch.lift.lift()(pred)(ach.unChurch)) |
|||
# recursively counts times divisor can be subtracted from dividend... |
|||
divChurch = proc(dvdndch, dvsrch: Church): Church = |
|||
let succ = func(chf: ChurchFunc): ChurchFunc = |
|||
(f: Func) => ((x: In) => f(chf(f)x)) |
|||
let pred = proc(chf: ChurchFunc): ChurchFunc = |
|||
chf.makeChurch().predChurch().unChurch() |
|||
proc divr(n: ChurchFunc; d: MetaMetaChurchFunc): ChurchFunc = |
|||
((vchf: ChurchFunc) => |
|||
((vchf.lift.lift())( # a isnotZeroChurch test |
|||
((_: ChurchFunc) => (divr(vchf, d)).succ))( # not zero recurse |
|||
zeroChurch.unChurch) # else terminate with zero |
|||
))(d(pred)(n)) # each recursive loop tests n minus d |
|||
makeChurch( |
|||
divr(dvdndch.unchurch.succ, dvsrch.unchurch.lift.lift)) |
|||
#conversions |
# conversions between ChurchFunc and int: |
||
proc toChurch(x: int): Church = |
|||
let incr = (x: In) => (()=>x()+1) |
|||
result = zeroChurch |
|||
proc toChurch(x: int): Ch = |
|||
result = |
for _ in 1 .. x: result = result.succChurch |
||
let incr = (x: In) => (() => x() + 1) |
|||
for i in 1..x: |
|||
proc toInt(ch: Church): int = ch.chf(incr)(() => 0)() |
|||
result = result.succ |
|||
proc |
proc `$`(ch: Church): string = $(ch.toInt) |
||
proc `$`(c: Ch): string = $(c.toInt) |
|||
when isMainModule: |
when isMainModule: |
||
let |
let threeChurch = 3.toChurch |
||
let |
let fourChurch = threeChurch.succChurch |
||
let elevenChurch = 11.toChurch |
|||
echo [(add three)four, (mul three)four, (exp1 three)four, (exp2 four)three] |
|||
let twelveChurch = elevenChurch.succChurch |
|||
</lang> |
|||
echo [ threeChurch.addChurch(fourChurch) |
|||
, threeChurch.multChurch(fourChurch) |
|||
, threeChurch.expChurch(fourChurch) |
|||
, fourChurch.expChurch(threeChurch) |
|||
, zeroChurch.isZeroChurch, oneChurch.isZeroChurch |
|||
, elevenChurch.minusChurch(threeChurch) |
|||
, elevenChurch.divChurch(threeChurch) |
|||
, twelveChurch.divChurch(threeChurch) |
|||
]</lang> |
|||
{{out}} |
{{out}} |
||
<pre>[7,12,81,64]</pre> |
<pre>[7, 12, 81, 64, 1, 0, 8, 3, 4]</pre> |
||
Note that the division function uses internal proc recursion instead of resorting to use of the Y-combinator since Nim supports direct proc recursion. |
|||
=={{header|OCaml}}== |
=={{header|OCaml}}== |