Skip to content

Instantly share code, notes, and snippets.

@safareli
Created October 17, 2020 12:37
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save safareli/71b7da77f864d17e5c6c6cb77ec8af32 to your computer and use it in GitHub Desktop.
Save safareli/71b7da77f864d17e5c6c6cb77ec8af32 to your computer and use it in GitHub Desktop.

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 any a :: Piano
  • fold (view a) === a is true for any a :: 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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment