Jump to content

Church numerals: Difference between revisions

→‎All closures and a union for type-punning: add more extensive Church functions and comments...
(→‎{{header|F#}}: Add a more complete set of Church functions with comments...)
(→‎All closures and a union for type-punning: add more extensive Church functions and comments...)
Line 1,088:
 
===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; the following code implements more extended Church functions such as Church subtraction and division than the task requries:
 
<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
succFunc = (c:In Ch)=->((f: Fn)=>((x: In)=>f c(f)x ))
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:
exp2 = (cup: Ch(T -> T) =-> ((d:T Mc) =-> d cT)
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 tobetween ChurchFunc and int:
proc toChurch(x: int): Church =
let incr = (x: In) => (()=>x()+1)
result = zeroChurch
proc toChurch(x: int): Ch =
for _ in 1 .. x: result = zeroresult.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 toInt`$`(cch: ChChurch): intstring = c(incr)(()=>0)$(ch.toInt)
proc `$`(c: Ch): string = $(c.toInt)
 
when isMainModule:
let threethreeChurch = 3.toChurch
let fourfourChurch = threethreeChurch.succsuccChurch
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}}
<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}}==
474

edits

Cookies help us deliver our services. By using our services, you agree to our use of cookies.