So church encoding of Piano numbers is like this:
type PianoC = (z) -> (z -> z) -> z
zero
just grabs "on zero handler" and returns that
zero :: PianoC
zero = \z i -> z
inc
on the other hand return new PianoC
number that would call first delegate all handlers to it's argument and plus call the "on inc handler" just once more.
inc :: PianoC -> PianoC
inc p = \z i -> i (p z i)
If we were not using functions we would have represented Piano numbers like this
data Piano = Zero | Inc Piano
Zero :: Piano
Inc :: Piano -> Piano
If we were to implement fold
for it it's type would look like this:
fold :: Piano -> (z) -> (z -> z) -> z
If you look closely you would notice that last parts is same as the PianoC
so type of fold
can be written like this:
fold :: Piano -> PianoC
fold (Zero ) z i = z
fold (Inc x) z i = i (fold x z i)
We can implement it's inverse too, which given the PianoC
converts it to function-less encoding.
view :: PianoC -> Piano
view p = p Zero Inc
Because we have implemented fold
and view
it can be used to proves that both encodings are fully equivalent i.e. they are isomorphic:
view (fold a) === a
is true for anya :: Piano
fold (view a) === a
is true for anya :: PianoC
Piano
is defunctionalized version of PianoC
. In haskell because of laziness
data types implemented using church encoding can be as useful as once with defunctionalized encoding.
But in strict languages church encoding is less useful. Especially because of stack size limitations, if you
have 100,000 represented using PianoC
and you want to fold it down to Integer
for example,
you would blow the stack and there is nothing you can do as it' can't be introspected.
While in haskell there is no stack size issues and you are all good.
For example A while ago I was porting FreeApplicative
structure which had good asymptotics in Haskell to JS.
But it was implemented using church like encoding and direct JS port was blowing the stack when the structure was moderately big.
I had to instead defunctionalize the structure (i.e. not use functions in it's representation - just use records/objects)
and then implement stack safe fold for it with was implemented using while loop and used array as manual stack.