Talk:Church numerals

From Rosetta Code

Created a stub for a Church Numerals

Not sure if this needs the addition of a more stretching task ? It may already not be all that easy to implement in languages with limited support for higher-order functions. In AppleScript, for example, my first sketches of churchMultiply all produce a stack overflow. Hout (talk) 22:09, 21 August 2018 (UTC)

@Hout, I wonder if this task should be extended somewhat to include the Church isZero function, the Church predecessor function, the Church subtraction function that uses the predecessor function, and the Church division that uses the principles of subtraction, succession, branching, recursion, and subtraction to implement division as the number of times the divisor can be subtracted from the dividend until it reaches Church zero. While it is much more difficult to implement these extended Church functions, it pushes the type system, especially for statically-typed languages, much more than just the existing task functions. If it is possible to implement these extended Church functions, then it it almost certain that any Church function can be implemented, indicating that the given language is type complete and Church and therefore Turing complete.
Most current languages implementations that have the full set of existing functions should be able to implement the extra functions as long as they support functions (including captured environment variables as closures) as first-class values in some form (which is required for existing functions, even if implementing closures requires modeling them as objects with the captured values as fields); any extra limitations will be due to the restrictions on statically-typed type systems, especially with strong type inference. In some languages, they can be effectively dynamically typed languages by raw casting or "punning" using tagged unions of "Kind's" of functions, in some languages the generics systems related to generic classes/interfaces will be able to handle it, or in some languages a type "softening" extension can be used (such as Haskell with the "RankNTypes" extension that can be used instead of the raw casting of "unsafeCoerce"). Only a few languages such as Elm won't be able to implement the full set of extended functions due to language design decisions related to language type safety. Still, it would be instructive for RosettaCode viewers to know which languages have these restrictions and why.
For example, and as a model of how the full set of Church Numeral functions can be implemented, following is an implementation of them in Haskell using raw casting ("unsafeCoerce"), including type signatures which aren't required by the program but to show the external strong static typing:

<lang haskell>import Unsafe.Coerce (unsafeCoerce)

type Church a = (a -> a) -> (a -> a)

churchZero :: Church a churchZero = const id -- or \ _ -> \ x -> x

churchOne :: Church a churchOne = id -- or \ f -> f, where f is a Church a

succChurch :: Church a -> Church a succChurch = (<*>) (.) -- add one recursion or \ ch -> \ f -> f ch f

addChurch :: Church a -> Church a -> Church a addChurch = (<*>) . fmap (.) -- or \ cha chb -> \ f -> cha f . chb f

multChurch :: Church a -> Church a -> Church a multChurch = (.) -- or \ cha chbf -> \ f -> cha . chb f

expChurch :: Church a -> Church a -> Church a expChurch chbs chexp = unsafeCoerce chexp chbs

isZeroChurch :: Church a -> Church a isZeroChurch ch = unsafeCoerce ch (const churchZero) churchOne

predChurch :: Church a -> Church a predChurch ch f x = unsafeCoerce ch (\ g h -> h (g f)) (const x) id

subChurch :: Church a -> Church a -> Church a subChurch cha chb = unsafeCoerce chb predChurch cha

divChurch :: Church a -> Church a -> Church a divChurch chdvdnd chdvsr =

 let divr n d =
       let tstloop =
             \ v -> unsafeCoerce v (const $ succChurch $ divr v d) churchZero
       in tstloop $ subChurch n d
 in divr (succChurch chdvdnd) chdvsr

CONVERSIONS --------------------------------

churchFromInt :: Int -> Church a -- Or Recursively: -- churchFromInt 0 = churchZero -- churchFromInt n = succChurch $ churchFromInt (n - 1) -- not tail recursive!

-- Or as a (lazy) list fold - strict due to foldr: -- churchFromInt n = foldr (.) id . replicate n

-- Or as an iterated (lazy) list application: -- better -> lazy recursion... churchFromInt n = iterate succChurch churchZero !! n

intFromChurch :: Church Int -> Int intFromChurch ch = ch succ 0

TEST -------------------------------------

main :: IO () main = do

 let [ c3, c4 ] = map churchFromInt [ 3, 4 ]
 print $ map intFromChurch [ succChurch churchZero
                           , addChurch c3 c4
                           , multChurch c3 c4
                           , expChurch c3 c4
                           , expChurch c4 c3
                           , isZeroChurch churchZero
                           , isZeroChurch c3
                           , predChurch c4
                           , subChurch c4 c3
                           , divChurch c3 c4
                           , divChurch c4 c4
Note that alternate implementations are suggested for those languages that don't have Haskell's full set of built-in functions and functional concepts.--GordonBGood (talk) 03:18, 30 December 2021 (UTC)
Nice variant ! Do add it to the main page. Late in the day, and really no need, I think, to start expanding requirements, but also no reason at all for individual contributions not to go an extra mile, as you have done so interestingly here. Many thanks ! Hout (talk) 09:25, 30 December 2021 (UTC)
@Hout, I have contributed two different Haskell variants implementing the extended Church functions as well as C#, F#, and Nim equivalents for your perusal.--GordonBGood (talk) 13:01, 1 January 2022 (UTC)

Worker-wrapper transformation in Haskell

In response to Spoon!'s query – "not sure why `go` helper is necessary": the worker-wrapper transform is a useful reflex whenever recursion is needed. – (recursive name found in a more local namespace – often a smaller frame pushed to stack etc. etc) but no particular view on it here. Your edit looks fine. Hout (talk)

Phix disclaimer

Disclaimer: this all feels a bit silly to me, but the intention (I am no expert on this lambda stuff) is that it shows how "closures" (or whatever) can be simulated quite easily with routine_ids and data. Petelomax (talk)

:-) It could certainly seem like a laborious route to integer arithmetic, but Peano numbers and Church encoding have an interest of their own in the history of computing theory (and even in the implementation of Smalltalk). In the Rosetta context, they can reveal the different routes which each language takes to manipulating higher-order functions.
(I moved your comment here – given the essentially anonymous/collective character of contributions, the talk page seems the more natural home for it) Hout (talk) 17:39, 13 September 2018 (UTC)
OK Pete Lomax (talk) 19:02, 13 September 2018 (UTC)

RankNTypes & coercion

This is a nice task, it is good at showing different type systems. Several examples refers to Haskell's RankNTypes. What does it do? Does it make all Church numerals the same type? In the C++ implementation of division, I had trouble with 4-2 and 3-1 being different types even though they are both 2. Is that the cause of needing coercion? Garbanzo (talk) 21:14, 23 December 2022 (UTC)


Also, it is amazing that 0^0 works out to 1. Still trying to wrap my head around that one. Garbanzo (talk) 21:17, 23 December 2022 (UTC)

0^0 is (generally) defined to be 1, which is not necessarily what you might expect, as you note... As a justification, consider x^n: x^n = x(x^(n-1)), so 2^3 = 2(2^2), 2^2 = 2(2^1) and so 2^1 must be 2(2^0). As 2^1 is 2, 2^0 must be 1 and similarly, every integer to the power 0 must be 1. If you imagine drawing a graph of y = x^0, it would be the straight line y = 1. If 0^0 isn't 1, there would be a discontinuity at x = 0. --Tigerofdarkness (talk) 23:21, 23 December 2022 (UTC)
Yes, it is amazing that it works out naturally with Church numerals too which seem to come at it from a different angle. Garbanzo (talk) 08:05, 27 December 2022 (UTC)