A question on existential types and Church encoding
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
type CB a = forall a . a -> a -> a
ctrue :: CB a ctrue x y = x
cfalse :: CB a cfalse x y = y
cand :: CB a -> CB a -> CB a cand p q = p q cfalse
cor :: CB a -> CB a -> CB a cor p q = p ctrue q
which works. But I haven't the faintest idea why that "forall" in the type makes things work... I just don't fully understand existential type quantification. Could anyone explain to me what's going on that makes the second code work? Thanks, Cory
On Sat, May 29, 2010 at 9:28 PM, Cory Knapp
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
Jason Dagit wrote:
In Church's λ-calc the types are ignored,
Not so. Church-style lambda calculus is the one where types matter; Curry-style is the one that ignores types and evaluates as if it were the untyped lambda calculus. Church encodings are based on the untyped LC rather than Church's simply-typed LC however, which is why they don't typecheck with Hindley--Milner. -- Live well, ~wren
On Sun, May 30, 2010 at 4:08 AM, wren ng thornton
Jason Dagit wrote:
In Church's λ-calc the types are ignored,
Not so. Church-style lambda calculus is the one where types matter; Curry-style is the one that ignores types and evaluates as if it were the untyped lambda calculus.
Church encodings are based on the untyped LC rather than Church's simply-typed LC however, which is why they don't typecheck with Hindley--Milner.
Oh I see. Thanks for that correction. Jason
On Sunday 30 May 2010 12:28:36 am Cory Knapp wrote:
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
The reason these types are required is that the 'a' in your Church booleans is the result type. So, if you want to inspect a boolean and produce an 'a', you need a 'CB a', and notably, you have the result type tied to the boolean type. So 'CB a' isn't just a boolean, it's a boolean that only allows you to choose between two 'a' values. 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 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.
ctrue :: CB a ctrue x y = x
cfalse :: CB a cfalse x y = y
cand :: CB a -> CB a -> CB a cand p q = p q cfalse
cor :: CB a -> CB a -> CB a cor p q = p ctrue q
which works. But I haven't the faintest idea why that "forall" in the type makes things work... I just don't fully understand existential type quantification. Could anyone explain to me what's going on that makes the second code work?
In the new type, the parameter 'a' is misleading. It has no connection to the 'a's on the right of the equals sign. You might as well write: type CB = forall a. a -> a -> a And now, hopefully, a key difference can be seen: we no longer have the result type for case analysis as a parameter of the type. Rather, they must work 'for all' result types, and we can choose which result type to use when we need to eliminate them (and you can choose multiple times when using the same boolean value in multiple places). One may think about explicit typing and type abstraction. Suppose we have your first type of boolean at a particular type T. We'll call said type CBT. Then you have: CBT = T -> T -> T and values look like: \(t :: T) (f :: T) -> ... By contrast, values of the second CB type look like this: \(a :: *) (t :: a) (f :: a) -> ... so the values accept a type (the result type) as a parameter. When you go to write combinators: cand :: CBT -> CBT -> CBT cand p q = p q false This fails because p expects Ts, and q and false are not Ts, they are CBTs (so you need p to be a CBCBT :)). By contrast, with the second type, we write: cand :: CB -> CB -> CB cand p q = p CB q false where the first argument specifies what we want to produce. In GHC, types are not passed explicitly like this, but it's the sort of thing that's going on behind the scenes. And 'CB a' isn't restricted to just some program-wide choice of T, but from the perspective of cand and the like, 'a' is just some opaque variable it didn't get to choose, so it's in the same boat as if it were some fixed T. If we think about explicit type passing: cand (T :: *) (p :: CB T) (q :: CB T) = ... cand gets told what T is; it doesn't get to choose. Hopefully I didn't make that too over-complicated, and you can glean something useful from it. It turned out a bit longer than I expected. Cheers, -- Dan
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?
In the new type, the parameter 'a' is misleading. It has no connection to the 'a's on the right of the equals sign. You might as well write:
type CB = forall a. a -> a -> a
Ah! That makes sense. Which raises a new question: Is this type "too general"? Are there functiosn which are semantically non-boolean which fit in that type, and would this still be the case with your other suggestion (i.e. "cand p q = p (q t f) f" )?
I guess it wouldn't much matter, since Church encodings are for untyped lambda calculus, but I'm just asking questions that come to mind here. :)
And now, hopefully, a key difference can be seen: we no longer have the result type for case analysis as a parameter of the type. Rather, they must work 'for all' result types, and we can choose which result type to use when we need to eliminate them (and you can choose multiple times when using the same boolean value in multiple places).
One may think about explicit typing and type abstraction. Suppose we have your first type of boolean at a particular type T. We'll call said type CBT. Then you have:
CBT = T -> T -> T
and values look like:
\(t :: T) (f :: T) -> ...
By contrast, values of the second CB type look like this:
\(a :: *) (t :: a) (f :: a) -> ...
*snip*
cand (T :: *) (p :: CB T) (q :: CB T) = ...
cand gets told what T is; it doesn't get to choose.
I'm guessing that * has something to do with kinds, right? This is probably a silly question, but why couldn't we have (T :: *->*) ? Hopefully I didn't make that too over-complicated, and you can glean
something useful from it. It turned out a bit longer than I expected.
It was very helpful, thanks!
Cory
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
On Tue, Jun 1, 2010 at 3:40 PM, Cory Knapp
In the new type, the parameter 'a' is misleading. It has no connection to the 'a's on the right of the equals sign. You might as well write:
type CB = forall a. a -> a -> a
Ah! That makes sense. Which raises a new question: Is this type "too general"? Are there functiosn which are semantically non-boolean which fit in that type, and would this still be the case with your other suggestion (i.e. "cand p q = p (q t f) f" )?
Because the type is universally quantified, any function with that signature can only manipulate the values it's given, having no way of creating new values of that type, or inspecting them in any way. It receives two values and returns one, so (ignoring _|_) only two implementations are possible: (\x _ -> x) and (\_ x -> x), which are the Church booleans. Intuitively, observe that the function must, and may only, make a decision between two options--thus providing exactly one bit of information, no more and no less. - C.
On Tuesday 01 June 2010 3:40:41 pm Cory Knapp wrote:
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 first-class exists in GHC. If there were, it would work about the same as forall, like: foo :: (exists a. P a) -> T or what have you. There's potentially a little more of interest with how you make and take apart things with existential types, but that's about it. There are papers out there on type systems with this, and the UHC Haskell compiler has it, although it doesn't let you use it in conjunction with type classes, but I think SPJ is on record as saying it would add a lot of complexity to the current GHC type system, and I'm inclined to believe him. So, instead, GHC allows you to do existential quantification around data constructors, and somewhat confusingly, it uses the forall keyword. The idea behind this is that the type of such a constructor would be: C :: (exists a. ...) -> T which is isomorphic to: C :: forall a. ... -> T So, if you're using GADT syntax, that's exactly what you write: data T where C :: forall a. ... -> T but, if you're using normal-ish data syntax, instead of writing: data T = C (exists a. ...) you write: data T = forall a. C (...) which is supposed to suggest that C has the isomorphic type in question, but I think it just tends to confuse people who are new to this, especially since holding a universal inside a datatype looks like: data U = C (forall a. ...) and removing the constructors to attempt to make it a type alias makes them look identical: type T = forall a. ... type U = forall a. ... But the alias T here is not the same as the data type T above. To make them (roughly) the same, you'd need: type T = exists a. ... But I digress.
Ah! That makes sense. Which raises a new question: Is this type "too general"? Are there functiosn which are semantically non-boolean which fit in that type, and would this still be the case with your other suggestion (i.e. "cand p q = p (q t f) f" )?
(forall a. a -> a -> a) should type only booleans, with some caveats. The forall enforces parametricity, which means the only normal lambda terms you can write with that type are: \x y -> x \x y -> y In Haskell, you can also write stuff like: \x -> undefined \x y -> x `seq` y The first of which is arguably a boolean, if you consider _|_ to be one in Haskell (although the Church encoding contains several distinguishable bottoms, due to seq), but the second is weird. It's false, except it blows up if the true case is undefined. But if you ignore these weird corner cases (or have a language that doesn't allow them), then you get exactly the booleans.
I guess it wouldn't much matter, since Church encodings are for untyped lambda calculus, but I'm just asking questions that come to mind here. :)
By contrast to the above, I said that 'CB a' is a boolean that can be used to choose between 'a' values. However, you can construct non-booleans for special cases of this type. For instance: add :: CB Int add x y = x + y This is clearly not a boolean, but it inhabits CB Int. So, the only way you can be (reasonably) sure that v :: CB T is a boolean choice between Ts is if you got it by specializing something with the type (forall a. CB a), since that is exactly the type above that contains only boolean expressions (and the weird corner cases).
cand (T :: *) (p :: CB T) (q :: CB T) = ...
cand gets told what T is; it doesn't get to choose.
I'm guessing that * has something to do with kinds, right? This is probably a silly question, but why couldn't we have (T :: *->*) ?
* is the kind of types. So, for instance: Int :: * [Int] :: * Int -> Int :: * * -> * is the kind of functions from types to types, and so on, so: Maybe :: * -> * Either :: * -> * -> * (->) :: * -> * -> * So, in particular, if T :: * -> *, then T -> T is ill-kinded, because each side of (->) expects a *, but you're trying to give it a * -> *. Hence, CB T won't work if T :: * -> *. Cheers, -- Dan
In the new type, the parameter 'a' is misleading. It has no connection to the 'a's on the right of the equals sign. You might as well write:
type CB = forall a. a -> a -> a
On Tue, Jun 1, 2010 at 12:40 PM, Cory Knapp
Ah! That makes sense. Which raises a new question: Is this type "too general"? Are there functions which are semantically non-boolean which fit in that type
Actually, this type is *less* general, in that it has less members. Consider, what boolean is represented by this? q :: CB Int q = (+) Whereas the (forall a. a -> a -> a) must work on *any* type, so it has far less freedom to decide what to do, and therefore there are less possible implementations. In fact, if we treat all bottoms as equal, I believe these are all of the distinguishible implementations of this function: t a _ = a f _ a = a a1 = undefined a2 _ = undefined a3 _ _ = undefined a4 a b = seq b a a5 a b = seq a b a6 a = seq a (\_ -> a) a7 a = seq a (\b -> b) Without allowing bottoms, "t" and "f" are the only implementations. Here's some discriminators that are bottom if the passed in function is the first and not in the group of second: disc_t_f b = b undefined () disc_f_t b = b () undefined disc_6_t b = seq (b undefined) () disc_1_any b = seq b () disc_2_34567tf b = seq (b ()) () disc_3_4567tf b = seq (b () ()) () disc_4_6t b = b () undefined disc_5_f b = b undefined () disc_7_6 b = b () undefined disc_6_5 = seq (b undefined) () -- ryan
participants (7)
-
C. McCann -
Cory Knapp -
Dan Doel -
Daniel Fischer -
Jason Dagit -
Ryan Ingram -
wren ng thornton