Using fundeps to resolve polymorphic types to concrete types
Hi, Is there any theoretical reason that functional dependencies can't be used to resolve a polymorphic type to a concrete type? For example:
-- compile with -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
Since 'b' is uniquely determined by the fundep in DeriveType, it seems that this ought to work; ie, since the only type equation satisfying DeriveType A b is B -> B, it should reduce to that before trying to fit its type against its body. The motivation is this case:
data ComplexType a where SomeConstructor :: DeriveType a b => a -> b -> ComplexType a
specialCaseFunc :: ComplexType A -> B specialCaseFunc (SomeConstructor _ b) = b
Essentially, if I have a data structure with two types used as fields, and one uniquely determines the other, I'd like to use these instances to avoid re-stating the implied one in the type equations, if possible. Is there some theoretical reason for this not to work, or is it just a limitation of GHC's current implementation? (Note, I'm testing with GHC 6.8.2, so it's possible this might be fixed in trunk already...) Thanks, Bryan Donlan
Bryan Donlan wrote:
Hi,
Is there any theoretical reason that functional dependencies can't be used to resolve a polymorphic type to a concrete type? For example:
-- compile with -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
I'm not entirely sure what your use case is, but the reason this fails is that you gave a type signature which is more general than what the body can possibly be. Even with fundeps, the signature is claiming that the function works for *any* b provided it happens to be the right one for DeriveType A. That is, the signature is somewhat agnostic to whatever actual implementations happen to exist [though it must be consistent with them]. A true (DeriveType A b => b -> B) function would work even if we edited the instance declaration to be for DeriveType A C instead. And naturally 'id' is (a -> a) so giving a return type of B requires that the input type must also be B. It compiles just fine with (DeriveType A b => b -> b) after all, which resolves directly to (B -> B) [which I think is what you want?]. Though again, if we changed the instance then it would resolve to (C -> C) instead.
The motivation is this case:
data ComplexType a where SomeConstructor :: DeriveType a b => a -> b -> ComplexType a
specialCaseFunc :: ComplexType A -> B specialCaseFunc (SomeConstructor _ b) = b
Again the issue is that while the instance declaration says that the result happens to be B now, that's not what the "real" type of the result is-- it's (DeriveType A b => b) where b is *exactly* the one from the SomeConstructor signature, and hence the signature (DeriveType A b => ComplexType A -> b) doesn't work either since that's a different b. Since b --whatever it happens to be-- is fixed by A it seems like the (DeriveType A b => ComplexType A -> b) signature should work and consider it the same b. However, since the GADT is doing existential quantification, even though the b type is fixed we've lost that information and so we can't be certain that it *really* is the same b. If you're familiar with existential quantification then the behavior makes sense, though I agree it isn't quite what would be expected at first. I'm not sure off hand whether it should really be called a bug however. If you don't really need the existential in there, then this version works just fine:
{-# 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
data ComplexType a b where SomeConstructor :: DeriveType a b => a -> b -> ComplexType a b
specialCaseFunc :: ComplexType A b -> b specialCaseFunc (SomeConstructor _ b) = b
Essentially, if I have a data structure with two types used as fields, and one uniquely determines the other, I'd like to use these instances to avoid re-stating the implied one in the type equations, if possible.
If you do want the existential after all, you can keep it provided the context restriction [i.e. DeriveType] gives you a method to get it back. If all you're doing is type passing then an implementation like this works just fine:
class DeriveType a b | a -> b where someDestructor :: ComplexType a -> b
instance DeriveType A B where someDestructor _ = B
data ComplexType a where SomeConstructor :: DeriveType a b => a -> b -> ComplexType a
[1 of 1] Compiling Main ( fundep.hs, interpreted ) Ok, modules loaded: Main. *Main> someDestructor (SomeConstructor undefined undefined :: ComplexType A) B *Main> 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
The key to note here is that when we existentially quantify over b and loose the type information, any class dictionaries for b are packaged up with the value and can still be used to get views onto the value of b. We can only get *views* onto b but can't do anything which might recover information about the actual type of b, however [aka "existential escapes"]. So this may or may not be sufficient for your needs. The fact that existential quantification looses information which can never be recovered is one of the reasons why they can be difficult to deal with. -- Live well, ~wren
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' ... 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.
*Main> someDestructor (SomeConstructor undefined undefined :: ComplexType A) B
Why not this: *Main> someDestructor (SomeConstructor A B) B
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? P.
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|. P.
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
[0] wren@xenobia:~/test $ ghc --version The Glorious Glasgow Haskell Compilation System, version 6.8.2
I have an older version and wonder what goes wrong. Now that I think of it, other stuff that I coudn't compile might actually work in 6.8 It does make sense that |b| is resolved to |B| because of the functional dependency. P.
Hmm, I'm kind of confused by this now. I feel like the following code really should compile, but it doesn't. There's no use of existentials to hide type information at all. The functional dependency seems like it should give us the constraint (b1 ~ b2) allowing Refl to typecheck.
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, GADTs #-} module DeriveType where
class DeriveType a b | a -> b data TypeEq a b where Refl :: TypeEq a a
test :: (DeriveType a b1, DeriveType a b2) => a -> TypeEq b1 b2 test _ = Refl
But...
derivetype.hs:8:9:
Couldn't match expected type `b1' against inferred type `b2'
`b1' is a rigid type variable bound by
the type signature for `test' at derivetype.hs:7:22
`b2' is a rigid type variable bound by
the type signature for `test' at derivetype.hs:7:39
Expected type: TypeEq b1 b2
Inferred type: TypeEq b2 b2
In the expression: Refl
In the definition of `test': test _ = Refl
Is there a good reason this doesn't typecheck?
-- ryan
On Tue, Jul 29, 2008 at 10:37 AM, wren ng thornton
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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Ryan Ingram wrote:
Hmm, I'm kind of confused by this now. I feel like the following code really should compile, but it doesn't. There's no use of existentials to hide type information at all. The functional dependency seems like it should give us the constraint (b1 ~ b2) allowing Refl to typecheck.
It may be worth noting that GADTs subsume existential types. Not that that matters here.
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, GADTs #-} module DeriveType where
class DeriveType a b | a -> b data TypeEq a b where Refl :: TypeEq a a
test :: (DeriveType a b1, DeriveType a b2) => a -> TypeEq b1 b2 test _ = Refl
But...
derivetype.hs:8:9: Couldn't match expected type `b1' against inferred type `b2'
Like I was saying, contexts are only ever verified as constraints on polymorphism, they never drive the type inference algorithm. Think of them as something that happens after the fact, "delayed constraints" if you will. The constructor Refl defines a constant of type (forall t. TypeEq t t). This constrains the return type of 'test' to have the same type, namely that the two arguments to the TypeEq type constructor are both the same. The signature you gave is more polymorphic than that, it allows for the possibility that they might be different. This is the same as the previous example using 'id' and wanting to give it the type (b -> B). If we simplify the example it might be more apparent why it fails. [0] wren@xenobia:~/test $ cat wacky2.lhs && ghci wacky2.lhs > module DeriveType where > > data TypeEq a b = TE > > refl :: TypeEq a a > refl = TE > > test :: a -> TypeEq b1 b2 > test _ = refl GHCi, version 6.8.2: http://www.haskell.org/ghc/ :? for help Loading package base ... linking ... done. [1 of 1] Compiling DeriveType ( wacky2.lhs, interpreted ) wacky2.lhs:9:11: Couldn't match expected type `b1' against inferred type `b2' `b1' is a rigid type variable bound by the type signature for `test' at wacky2.lhs:8:22 `b2' is a rigid type variable bound by the type signature for `test' at wacky2.lhs:8:25 Expected type: TypeEq b1 b2 Inferred type: TypeEq b2 b2 In the expression: refl In the definition of `test': test _ = refl Failed, modules loaded: none. Prelude> In your version we'd like the fundeps to kick in and say there can be only one type paired with 'a' and so we can infer that 'b1' and 'b2' are the same, but fundeps are part of type classes and so they too are just delayed constraints.[1] At the time of determining what the principal type of the function is, we don't see the type classes or the fundeps associated with them. While inferring the principal type we build up a set of delayed constraints (i.e. requisite type class instances, based on the functions used). After we've determined the principal type, we then verify that we can fulfill all the delayed requirements if we assume the type class instances in the context actually exist. If we pass type inference and context verification, then we deem the function OK. The main use of fundeps is to assist type inference at *use* sites for the function. Say we have a function (foo :: DeriveType a b => a -> b). If somewhere we use that function in the expression (foo x), if we've already determined that x has type A, this will let us infer some type B for specializing the polymorphism of foo in this expression. Without fundeps we would have to give a type signature in order to clarify which B should be used, if it couldn't otherwise be inferred. But this is all fundeps do, they don't help in determining what the type of foo itself is when we're defining it. There are some cute tricks that can be played with fundeps in order to do type arithmetic and such, but Haskell doesn't really have dependent types and so it doesn't really use contexts to drive inference either. Sadly fundeps aren't quite as well integrated or general as they could be, but trying to resolve the MPTC/fundep/type families/... stuff into a single coherent approach is part of what the haskell' committee is trying to work out. One of the tricks in all this is to figure out how to have enough of dependent typing to do what we want, but without sacrificing decidability(/verifiability) of type inference. [1] Also, Haskell has only one way of representing that two types are identical, namely unification i.e. using the same type variable. So even if fundeps did drive type inference, that type signature would still be wrong because the principal type is (DeriveType a b => a -> TypeEq b b) since it's guaranteed that DeriveType a is defined at only one 'b'. -- Live well, ~wren
This seems like an appropriate place to use type families.
{-# LANGUAGE TypeFamilies, GADTs #-}
module DeriveType where
type family DeriveType a
data A = A
data B = B
type instance DeriveType A = B
data ComplexType a where
SomeConstructor :: a -> DeriveType a -> ComplexType a
specialCaseFunc :: ComplexType A -> B
specialCaseFunc (SomeConstructor _ b) = b
On Mon, Jul 28, 2008 at 6:32 PM, Bryan Donlan
Hi,
Is there any theoretical reason that functional dependencies can't be used to resolve a polymorphic type to a concrete type? For example:
-- compile with -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
Since 'b' is uniquely determined by the fundep in DeriveType, it seems that this ought to work; ie, since the only type equation satisfying DeriveType A b is B -> B, it should reduce to that before trying to fit its type against its body.
The motivation is this case:
data ComplexType a where SomeConstructor :: DeriveType a b => a -> b -> ComplexType a
specialCaseFunc :: ComplexType A -> B specialCaseFunc (SomeConstructor _ b) = b
Essentially, if I have a data structure with two types used as fields, and one uniquely determines the other, I'd like to use these instances to avoid re-stating the implied one in the type equations, if possible.
Is there some theoretical reason for this not to work, or is it just a limitation of GHC's current implementation? (Note, I'm testing with GHC 6.8.2, so it's possible this might be fixed in trunk already...)
Thanks,
Bryan Donlan _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Hi,
On 7/29/08, Bryan Donlan
Hi,
Is there any theoretical reason that functional dependencies can't be used to resolve a polymorphic type to a concrete type? For example:
-- compile with -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
Since 'b' is uniquely determined by the fundep in DeriveType, it seems that this ought to work; ie, since the only type equation satisfying DeriveType A b is B -> B, it should reduce to that before trying to fit its type against its body.
According to the theory of functional dependencies this function should type check but there is a bug in the current implementation (or you may view it as an incompleteness---the compiler is not smart enough to infer that "b" in this case is really "B" while checking the signature). Iavor
participants (5)
-
Bryan Donlan -
iavor.diatchki＠gmail.com -
Pablo Nogueira -
Ryan Ingram -
wren ng thornton