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 <[EMAIL PROTECTED]> wrote:
> 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] [EMAIL PROTECTED]:~/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] [EMAIL PROTECTED]:~/test $ ghc --version
> The Glorious Glasgow Haskell Compilation System, version 6.8.2
>
> [0] [EMAIL PROTECTED]:~/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] [EMAIL PROTECTED]:~/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] [EMAIL PROTECTED]:~/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
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
