How to encode two distinct Unit types using church encoding

172 views Asked by At

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.

0

There are 0 answers