A type signature inferred by GHCi that is rejected when written explicitly

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

A type signature inferred by GHCi that is rejected when written explicitly

Pablo Nogueira-3
I find this interesting,

GHCi accepts a function |dmap| which I show below and infers its type,
but if I annotate the function with the inferred type, GHCi's
type-checker rejects it.

I'm trying to generalise the datatype-generic dmap:

< dmap :: Bifunctor s => (a -> b) -> Fix s a -> Fix s b
< dmap f = In . bimap (dmap f) f . out

where
> data Fix s a = In { out :: s (Fix s a) a  }
>
> class Bifunctor s where
>     bimap :: (a -> c) -> (b -> d) -> s a b -> s c d

The idea is that recursive types are represented by their
(lamba-lifted) functors, eg:

> data ListF b a = NilF | ConsF a b

> instance Bifunctor ListF where
>   bimap f g NilF           =  NilF
>   bimap f g (ConsF a b)    =  ConsF (g a) (f b)

I now define two classes:

> class From a c x where
>     from :: a x -> c x
>
> class To a c y where
>     to :: c y -> a y

And a generic |gmap| which given the map for |c| and a mapping for |x|
delivers the map for |a|:

> type GMap t x y = (x -> y) -> t x -> t y
>
> gmap :: (From a c x, To a c y) => GMap c x y -> GMap a x y
> gmap gmc gmx = to . gmc gmx . from

I want to write |dmap| as a special case of |gmap|, but I can't even
get there. If I write

> dmap f = to . bimap (dmap f) f . from

GHCi infers it has type (up to renaming):

(From a1 (s (a1 x)) x,  Bifunctor s,  To  a2 (s (a2 y)) y) => (x -> y)
-> a1 x -> a2 y

But if I cut and paste the type into the code I get type errors:

   Could not deduce (From a1 (s1 (a11 x)) x) ...
    Could not deduce (From a11 (s1 (a11 x)) x, To a21 (s1 (a21 y)) y) ...
    Could not deduce (From a1 (s1 (a11 x)) x) ...

Interesting,
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A type signature inferred by GHCi that is rejected when written explicitly

Bugzilla from alfonso.acosta@gmail.com
Hi Pablo,

On Mon, Jul 7, 2008 at 10:07 AM, Pablo Nogueira
<[hidden email]> wrote:

> GHCi infers it has type (up to renaming):
>
> (From a1 (s (a1 x)) x,  Bifunctor s,  To  a2 (s (a2 y)) y) => (x -> y)
> -> a1 x -> a2 y
>
> But if I cut and paste the type into the code I get type errors:
>
>   Could not deduce (From a1 (s1 (a11 x)) x) ...
>    Could not deduce (From a11 (s1 (a11 x)) x, To a21 (s1 (a21 y)) y) ...
>    Could not deduce (From a1 (s1 (a11 x)) x) ...

I myselft  don't understand why GHCi doesn't accept the type it
infered as an explicit signature ... but your problem seems to be
caused by a lack of functional dependencies.

Redefining To and From as ..

class From a c x | a -> c where
    from :: a x -> c x

class To a c y | c -> a where
    to :: c y -> a y

... hushes GHCi. The question now is, of course, if the new
dependencies are too restrictive for your problem.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A type signature inferred by GHCi that is rejected when written explicitly

Pablo Nogueira-3
> I myselft  don't understand why GHCi doesn't accept the type it
>  infered as an explicit signature ...

I think it has to do with the following:

Looking at the type errors, they seem to indicate that the type
checker is being general and does not assume the |From| and |To|
"relations" are between
a type |t| and (s (t x) x)| but, in general, between |t| and |s (t' x) x|.

Given that

from   :: (From a1 c1 x) => a1 x -> c1 x
 to     :: (To   a2 c2 y) => c2 y -> a2 y
bimap  :: Bifunctor s => (t1 -> t3) -> (t2 -> t4) -> s t1 t2 -> s t3 t4

During type checking the following equations spring up:

c2 y   = s t3 t4
c1 x   =  s t1 t2
t2       = x
t4       = y
t1       = a1 x
t3       = a2 y

That'd give the same type as that inferred, but somehow new variables
|a11| and |a12| appear.

>  caused by a lack of functional dependencies.
>  class From a c x | a -> c where
> class To a c y | c -> a where
> ... hushes GHCi. The question now is, of course, if the new
>  dependencies are too restrictive for your problem.

They are of little avail given the instances I define:

 instance Bifunctor s => From (Fix s) (s (Fix s x)) x where
     from = out

 instance Bifunctor s => To (Fix s) (s (Fix s y)) y where
     to   = In
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

RE: A type signature inferred by GHCi that is rejected when written explicitly

Simon Peyton Jones
| > I myselft  don't understand why GHCi doesn't accept the type it
| >  infered as an explicit signature ...

I've known about this confusing behavior for some time, and the design goal that the compiler should not infer a type that it can't check seems Clearly Right.  Stupidly, though, I had not previously realized that it's all a consequence of GHC's rather relaxed approach to ambiguity.  Here's a little section from a some notes I'm working on that may clarify.  Bottom line: I intend to change GHC (I hope for 6.10) so that if a definition gets an inferred type that could not appear as a type signature, the definition will be rejected as ambiguous.

Comments welcome.  (Do cc me since I no longer guarantee to read all of the wisdom of Haskell CafĂ©.)

Simon

Consider this
\begin{code}
  class C a b where
    op :: b -> a -> a

  instance C [a] b
    op _ x = x

  instance Ord b => C (Maybe a) b
    op _ x = x

  f x = op undefined x
\end{code}
GHC currently infers the type
\begin{code}
  f :: C a b => a -> a
\end{code}
Despite the fact that @b@ is not mentioned after the @=>@, nor is
there a functional dependency, @f@ can be called unambiguously, thus
\begin{code}
  f [True]
\end{code}
This call gives rise to the constraint @(C [Bool] b)@, for some undetermined
type @b@, and the instance declaration fires happily.  However, the call
@(f Nothing)@ will give the constraint @(Ord b)@, which cannot be discharged
without knowing @b@.  Some calls are ambiguous and some are not.  GHC
defers this choice to the caller, unless it can readily see that every
call will be ambiguous.

However, this relaxed approach has a big disadvantage: \emph{you cannot
write a type signature for @f@!}:
\begin{code}
  f :: C a c => a -> a
  f x = op undefined x
\end{code}
Now GHC has no way to prove that the given constraint @(C a c)@
proves the wanted constraint @(C a b)@, using plain syntactic matching.

So we propose the following:
\begin{itemize}
\item Every inferred type (and every type written by the programmer)
must be unambiguous.
\item A type $\forall \overline{a}.C \Rightarrow \rho$ is unambiguous iff
from $C$ we can deduce $C[\overline{b'/b}]$ where $\overline{b} = \overline{a} \setminus fv(\rho)$,
and $\overline{b'}$ are fresh.  That is, freshen the variables in $C$ that
are not mentioned in the type $\rho$, and check that you can can deduce
the freshened $C'$ from $C$.
\end{itemize}
This would reject the definition @f@, either with or without a type
signature.

| -----Original Message-----
| From: [hidden email] [mailto:haskell-cafe-
| [hidden email]] On Behalf Of Pablo Nogueira
| Sent: 08 July 2008 09:03
| To: Alfonso Acosta
| Cc: Haskell-Cafe
| Subject: Re: [Haskell-cafe] A type signature inferred by GHCi that is
| rejected when written explicitly
|
| > I myselft  don't understand why GHCi doesn't accept the type it
| >  infered as an explicit signature ...
|
| I think it has to do with the following:
|
| Looking at the type errors, they seem to indicate that the type
| checker is being general and does not assume the |From| and |To|
| "relations" are between
| a type |t| and (s (t x) x)| but, in general, between |t| and |s (t' x) x|.
|
| Given that
|
| from   :: (From a1 c1 x) => a1 x -> c1 x
|  to     :: (To   a2 c2 y) => c2 y -> a2 y
| bimap  :: Bifunctor s => (t1 -> t3) -> (t2 -> t4) -> s t1 t2 -> s t3 t4
|
| During type checking the following equations spring up:
|
| c2 y   = s t3 t4
| c1 x   =  s t1 t2
| t2       = x
| t4       = y
| t1       = a1 x
| t3       = a2 y
|
| That'd give the same type as that inferred, but somehow new variables
| |a11| and |a12| appear.
|
| >  caused by a lack of functional dependencies.
| >  class From a c x | a -> c where
| > class To a c y | c -> a where
| > ... hushes GHCi. The question now is, of course, if the new
| >  dependencies are too restrictive for your problem.
|
| They are of little avail given the instances I define:
|
|  instance Bifunctor s => From (Fix s) (s (Fix s x)) x where
|      from = out
|
|  instance Bifunctor s => To (Fix s) (s (Fix s y)) y where
|      to   = In
| _______________________________________________
| Haskell-Cafe mailing list
| [hidden email]
| http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe