On Tue, Jun 1, 2010 at 12:40 PM, Cory Knapp
Thanks! That was exactly the sort of response I was looking for.
This explains why you need to double up for your current definitions. To
choose between two booleans (which will in turn allow you to choose between 'a's), you need a CB (CB a). You can eliminate the asymmetric type, though, like so:
cand :: CB a -> CB a -> CB a cand p q t f = p (q t f) f
Right. When he was working on it, I thought of that, and seemed to have completely forgotten when I reworked it.
You can probably always do this, but it will become more tedious the more complex your functions get.
type CB a = forall a . a -> a -> a
Note: this is universal quantification, not existential.
As I would assume. But I always see the "forall" keyword used when discussing "existential quantification". I don't know if I've ever seen an "exists" keyword. Is there one? How would it be used?
There is no exists keyword, in GHC at least. See for example this page: http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/data-type-extensions... When the forall appears in certain places it behaves differently. For example: * In a function signature it is universal, but where it appears matters. Putting it on the left side of function arrows increases the rank of the type. This leads to Rank N types. * In the case of data constructors it can behave as existential quantification when it introduces a type variable on the right-hand side of the equal sign in the data declaration. At least, that's my understanding. Also, haskell prime has a proposal for an exists keyword: http://hackage.haskell.org/trac/haskell-prime/wiki/ExistentialQuantification Jason