1 回答
No such encoding is Unique
As you posed the question the answer is obviously "no"
a = forall r. (a -> r) -> r
a = forall s. ((forall r. (a -> r) -> r) -> s) -> s
as to which encoding is the smallest...well the underlying type is almost certainly!
Codensity might not be what you want
whats more, although Codensity is fascinating, I don't believe it is isomorphic to the underlying type. from . to = id is the easy direction.
to . from
= \x -> to (from x)
= \x -> C $ \f -> (from x) >>= f
= \x -> C $ \f -> (unC x return) >>= f
= \(C g) -> C $ \f -> (g return) >>= f
but then you get kinda stuck. The same thing happens when you try to prove a = forall r. (a -> r) -> r but you get saved by the "theorem for free" (there might be a way to do it without this, but the free theorem makes it easy). I know of no corresponding argument for Codensity, and what most papers I have read prove is rather that it preserves >>= and return, that is, if you only construct your C m a using the monadic operations and what you call to then the call to to . from is identity.
If we try hard enough we can even come up with a counter example to the isomorphism
evil :: C Maybe Int
evil = C $ \h -> case h 1 of
Nothing -> h 2
Just x -> Nothing
to . from $ evil
= (\(C g) -> C $ \f -> (g return) >>= f) evil
= C $ \f -> ((\h -> case h 1 of
Nothing -> h 2
Just x -> Nothing) return) >>= f
= C $ \f -> Nothing >>= f
so are these the same?
test 1 = Nothing
test n = Just n
unC evil test
= Just 2
unC (C $ \f -> Nothing >>= f) test
= Nothing >>= test
= Nothing
I might have made a mistake in that derivation. I have not really checked it, but suffice it to say that right now I don't think C m a = m a
Another Kind of CPS
All data can be encoded as untyped lambda functions, a property discovered by Church about 70 years ago. Often we talk about "Church encoding" data structures, although Oleg has suggested that instead, at least in a typed setting, we should talk about "Boehm-Beraducci" encodings. Regardless of what you call it, the idea is
(a,b) = forall r. (a -> b -> r) -> r
Either a b = forall r. (a -> r) -> (b -> r) -> r
at least up to fast and loose reasoning. It should be obvious that this encoding provides a way to encode any ADT as a System F type. This also reveals a way of implementing functional languages: treat everything as closures under the hood, and have pattern matching just be implemented as function application.
Actually, System F even has a way of encoding existential types as universal types
exists a. f a = forall r. (forall a'. f a' -> r) -> r
which turns out to be a very important identity. Among other things, this helps us to think about the relation between type inference for higher rank types and for existential types. Since type inference is decidable up to rank 2 types, type inference is also decidable in a system with rank 1 universals and existentials. Since existential quantification is the basis for modules, this is important stuff.