[Haskell-cafe] A question on existential types and Church encoding

[Jason Dagit]

On Sat, May 29, 2010 at 9:28 PM, Cory Knapp <cory.m.knapp at gmail.com> wrote:

> Hello,
>
> A professor of mine was recently playing around during a lecture with
> Church booleans (I.e., true = \x y -> x; false = \x y -> y) in Scala and
> OCaml. I missed what he did, so I reworked it in Haskell and got this:
>
> >type CB a = a -> a -> a
>
> >ct :: CB aC
> >ct x y = x
>
> >cf :: CB a
> >cf x y = y
>
> >cand :: CB (CB a) -> CB a -> CB a
> >cand p q = p q cf
>
> >cor :: CB (CB a) -> CB a -> CB a
> >cor p q = p ct q
>
> I found the lack of type symmetry (the fact that the predicate arguments
> don't have the same time) somewhat disturbing, so I tried to find a way to
> fix it. I remembered reading about existential types being used for similar
> type-hackery, so I added quantification to the CB type and got
>

By the way, I looked on wikipedia and their definitions vary slightly from
yours:
cand p q = p q p
cor p q = p p q

I think yours are equivalent though and for the rest of this reply I use the
ones from wikipedia.

I think the reason the it doesn't type check with the types you want is
because in cand we need to apply p at two different types for the type
variable 'a'.  In Haskell this requires you to do something different.  What
you did works (both the CB (CB a) and the rank n type).  As does this:
\begin{code}
type CB a = a -> a -> a

ct :: CB a
ct x y = x

cf :: CB a
cf x y = y

cand :: (forall a. CB a) -> CB a -> CB a
cand p q = p q p
\end{code}

And in fact, it still works as we'd hope:
*Main> :t cand ct
cand ct :: CB a -> a -> a -> a

In Church's λ-calc the types are ignored, but in Haskell they matter, and in
a type like cand :: CB a -> CB a -> CB a, once the type of 'a' is fixed all
uses of p must have the same 'a'.  In the type, (forall a1. CB a1) -> CB a
-> CB a, then p can be applied at as many instantiations of a1 as we like
inside of cand.

I hope that helps,
Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100530/1c333747/attachment.html