I was studying Haskell and happened to know the church encoding of algebraic data types. For example, the unit type in Haskell can be encoded as a polymorphic function type. But one can also define a Unit'
type that is isomorphic to Unit
but essentially treated as a distinct type from Unit
. Then we have Unit :: Unit
and Unit' :: Unit'
as elements from different domains. How to do this in church encoding?
data Unit = Unit
type UnitChurch = forall x. x -> x
data Unit' = Unit'
type UnitChurch' = ?
I tried to search google for questions alike but did not find an answer. My guess is that maybe we can define UnitChurch'
as:
type UnitChurch' = forall u. (UnitChurch -> u) -> u
which is similar to newtype
in Haskell.