Pablo Nogueira wrote:
wren ng thornton wrote:
It compiles just fine with (DeriveType A b => b -> b) after all, which resolves directly to (B -> B)
That's not the case:
simpleNarrow :: DeriveType A b => b -> b simpleNarrow = id
Couldn't match expected type `b' (a rigid variable) against inferred type `B' `b' is bound by the type signature for `simpleNarrow' ... When using functional dependencies to combine DeriveType A B, arising from the instance declaration ... DeriveType A b, arising from is bound by the type signature for `simpleNarrow' ...
[0] wren@xenobia:~/test $ cat fundep.hs {-# OPTIONS_GHC -fglasgow-exts #-} class DeriveType a b | a -> b data A = A data B = B instance DeriveType A B simpleNarrow :: DeriveType A b => b -> b simpleNarrow = id [0] wren@xenobia:~/test $ ghc --version The Glorious Glasgow Haskell Compilation System, version 6.8.2 [0] wren@xenobia:~/test $ ghci fundep.hs GHCi, version 6.8.2: http://www.haskell.org/ghc/ :? for help Loading package base ... linking ... done. [1 of 1] Compiling Main ( fundep.hs, interpreted ) Ok, modules loaded: Main. *Main> :t simpleNarrow simpleNarrow :: B -> B
I think Bryan got the order in which type inference/checking works wrong. The dependency is not "resolved" before calculating the type as he suggested.
Indeed. "Resolved" was a sloppy word choice on my part, but the point is that after all the inference is done you do end up with (B -> B) because B just so happens to be (DeriveType A b => b). However, the function's actual type is indeed (DeriveType A b => b -> b) since contexts are only a constraint on polymorphism and never take part in driving the inference.
*Main> :t someDestructor (SomeConstructor undefined undefined :: ComplexType A) B
Why not this:
*Main> someDestructor (SomeConstructor A B) B
That works too, I just didn't have deriving Show in place at the time.
But if you have actual values rather than just unit types, note that this won't work:
instance DeriveType A B where someDestructor (SomeConstructor _ b) = b
I couldn't understand the sentence "actual values rather than unit types". What do you have in mind? [...] I didn't pay attention to the |b| value returned. So what you meant was that only a constant function will do, not a function that returns the value |b|.
Yeah, pretty much. The types A and B given were both unit types, i.e. they have only one value each namely A and B. Hence we could do the other version with someDestructor _ = B since we're throwing away the old value of type (b quantified by SomeConstructor) and constructing a new value of type (forall b. DeriveType A b => b). This is safe because we're never actually peeking into the existential. And yet, since there's only one value of the type we can safely reconstruct it knowing that we're not leaking any information about SomeConstructor's internals. But what happens if there's more than one value of type B? If we tried the version above in order to return the second field of the ComplexType, that would allow the existential to escape. Hence my comments that the methods of DeriveType can only be used to gain views onto the value b but never to recover its actual type. If we had some non-dependent type that we could convert the existential into, then we can still safely use that view as below: [0] wren@xenobia:~/test $ cat fundep2.hs {-# OPTIONS_GHC -fglasgow-exts #-} class DeriveType a b | a -> b, b -> a where someDestructor :: b -> Int data A = A deriving Show data B = B1 | B2 deriving Show instance DeriveType A B where someDestructor B1 = 1 someDestructor B2 = 2 simpleNarrow :: DeriveType A b => b -> b simpleNarrow = id data ComplexType a where SomeConstructor :: DeriveType a b => a -> b -> ComplexType a unComplexType :: ComplexType a -> Int unComplexType (SomeConstructor _ b) = someDestructor b [0] wren@xenobia:~/test $ ghci fundep2.hs GHCi, version 6.8.2: http://www.haskell.org/ghc/ :? for help Loading package base ... linking ... done. [1 of 1] Compiling Main ( fundep.hs, interpreted ) Ok, modules loaded: Main. *Main> unComplexType (SomeConstructor A B1) 1 *Main> The thing to bear in mind with all of this is what should the type signature of unComplexType be? If someDestructor returned the second field directly then there would be no way for us to give a type signature to unComplexType. The "b" it would return is only scoped in the type of SomeConstructor and so we have no way of referring to that exact variable. What we can do however is return a monomorphic type or a non-dependent polymorphic type [e.g. (forall a. Num a => a) is just fine, even rank-2 types are fine, just not ones that depend on the existential b]. You'll also notice that we had to add a fundep from b back to a in order to get this to type check. Otherwise we can't be sure that the type a for the existential b is the same as the a (namely A) from ComplexType. This might be too restrictive for the application in question however. Again, I'm not sure any of this really helps the OP. If Ryan Ingram's type families code works, then I'd say to go for that. The whole point of existentials is that they loose information (that's how ST ensures safety). If loosing information in order to block introspection isn't the goal, then existential types really aren't what you want. If the whole goal is just to reduce the size of type signatures that need to be written out, then type aliases could also be used in order to save on the, er, typing without even resorting to any sort of sexy types. -- Live well, ~wren