Church encoding tutorial, part 5b: Existential types

This is part 5b of the tutorial series about the Church encoding. I'm following my book (just finished) "Programming in System Fω using Dhall". Church encoding of existential types are based on the idea that the function type (∃t. P t) → q is equivalent to the simpler function type ∀t. P t → q. I call this a "function extension rule". This rule is proved in the appendix of the book. The Church encoding of the existential type ∃t. P t is then written as: ∀r. (∀t. Pt → r) → r I motivate existential types and explain how they are created and used in Haskell and Scala. Then I show how existential types are defined in Dhall via the Church encoding. I compare types ∃t. P t and ∀t. P t and show that both are covariant with respect to P, allowing us to implement higher-kinded "fmap" functions of suitable types. Links: A tutorial on functional programming in System F-omega, the chapter on Church encodings for more complicated types: https://github.com/winitzki/scall/blo... Book page on Leanpub: https://leanpub.com/f-omega Book page (paper copy) on Lulu.com: https://www.lulu.com/shop/sergei-wini...