[Haskell-cafe] Using fundeps to resolve polymorphic types to concrete types

wren ng thornton wren at freegeek.org
Tue Jul 29 13:37:17 EDT 2008


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 at 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 at xenobia:~/test $ ghc --version
The Glorious Glasgow Haskell Compilation System, version 6.8.2

[0] wren at 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 at 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 at 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





More information about the Haskell-Cafe mailing list