[Haskell-cafe] Non-existant existential?
Consider the following: data SimpExist a = SimpExist (forall x . x - a) f :: SimpExist Bool f = SimpExist (const True) g = SimpExist id What is the type of g? In a similar example, GHC tells me it is of type SimpExist c. Yet, I can't unify it with any other SimpExist c'. It seems to me that this is something like exists x . SimpExist x, and is similar to: data ExistWrap = forall a . ExistWrap (forall x . x - a) Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-existant existential?
Hello, Consider the following: data SimpExist a = SimpExist (forall x . x - a) f :: SimpExist Bool f = SimpExist (const True) g = SimpExist id What is the type of g? In a similar example, GHC tells me it is of type SimpExist c. Yet, I can't unify it with any other SimpExist c'. Have you tried to type check this example (the g)? It does not type check in my GHC. There are not many functions with the type forall x . x - a when a is also polymorphic --- it is the type of unsafeCoerce. It seems to me that this is something like exists x . SimpExist x, and is similar to: data ExistWrap = forall a . ExistWrap (forall x . x - a) Sure, you should read a forall on the left side of a constructor as exists. Look at section 7.4.1.4.1 of: http://www.haskell.org/ghc/docs/6.4.2/html/users_guide/type-extensions.html The design decision here was to avoid introducing a new exist construct. I believe that the justification for this option is that in Logic a forall in a contravariant position has the same effect as an existential. Cheers, Bruno ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-existant existential?
On 9/21/06, Bruno Oliveira [EMAIL PROTECTED] wrote: Have you tried to type check this example (the g)? No. Please excuse me, as I wasn't by my GHC at the time. Let's try: data SimpExist a = Base a | SimpExist (SimpExist (forall x . x - a)) g :: SimpExist (forall a . a - a) g = Base id h = SimpExist g data WrapExist = forall a . WrapExist (SimpExist a) i = WrapExist h I'm familiar with the use for forall to mean exists, but I am baffled by h's ineffable type! Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-existant existential?
When I look at the generated core, I see that both h and same = Base undefined have the same type: %forall a . main:Fonly.SimpExist a I'm using GHC 6.5.20060819. If this is a bug, I actually find it kind of useful, for reasons I can elaborate later. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
