<br><br><div class="gmail_quote">On Sat, May 29, 2010 at 9:28 PM, Cory Knapp <span dir="ltr"><<a href="mailto:cory.m.knapp@gmail.com">cory.m.knapp@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hello,<br><br>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:<br>
<br>>type CB a = a -> a -> a<br><br>>ct :: CB aC<br>>ct x y = x<br><br>>cf :: CB a<br>>cf x y = y<br><br>>cand :: CB (CB a) -> CB a -> CB a<br>>cand p q = p q cf<br><br>>cor :: CB (CB a) -> CB a -> CB a<br>
>cor p q = p ct q<br><br>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<br>
</blockquote><div><br></div><div>By the way, I looked on wikipedia and their definitions vary slightly from yours:</div><div>cand p q = p q p</div><div>cor p q = p p q</div><div><br></div><div>I think yours are equivalent though and for the rest of this reply I use the ones from wikipedia.</div>
<div><br></div><div>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:</div>
<div>\begin{code}</div><div><div>type CB a = a -> a -> a</div><div><br></div><div>ct :: CB a</div><div>ct x y = x</div><div><br></div><div>cf :: CB a</div><div>cf x y = y</div><div><br></div><div>cand :: (forall a. CB a) -> CB a -> CB a</div>
<div>cand p q = p q p</div></div><div>\end{code}</div><div><br></div><div>And in fact, it still works as we'd hope:</div><div><div>*Main> :t cand ct</div><div>cand ct :: CB a -> a -> a -> a</div></div><div>
<br></div><div>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.</div>
<div><br></div><div>I hope that helps,</div><div>Jason</div></div>