[Haskell-cafe] Well-typed functions with nonexisting signatures
[Was: type variable question]
oleg at pobox.com
oleg at pobox.com
Fri Dec 15 00:06:22 EST 2006
Nicolas Frisby wrote
> The commented out signature is the signature that GHC infers for the
> function. When I uncomment that signature, it will no longer type
> check. Why does this happen? Even with the forall and the explicit
> signatures in the where clause, it chokes.
Alas, this is the property of Haskell, even of Haskell98. Half a year
ago I even wanted to write a message on the Haskell' list, pointing
out the embarrassment. One one hand, writing signatures is highly
recommended. On the other hand, there exist, even in Haskell98,
well-typed functions for which signatures simply do not exist. The
number of such exceptions multiply when we move to higher-rank types
(where such anomalies are to be expected).
The reason for the anomalies is the difference between the 'internal'
language that expresses inferred types and the external type language.
> Is there a canonical example example that exhibits this behavior?
Yes, it was discussed back in 2003. Here's the canonical form:
g::(Show a,Show b) => a->b
g = undefined
--h :: Show a => b -> a
h x = g(h x)
Both Hugs and GHC (in the pure Haskell98 mode!) are happy with h.
Both compilers infer the type for h, shown in the comment. If you give
h the type signature -- the one that is inferred by the compilers
themselves -- both compilers complain.
This example has been distilled from practical problems (the earliest
one was by Levent Erkok reported back on 2000)
http://www.mail-archive.com/haskell@haskell.org/msg06754.html
The following thread gives more detail and discussion:
http://www.haskell.org/pipermail/haskell/2003-May/011730.html
The final solution to the problem is in
http://www.haskell.org/pipermail/haskell/2003-May/011762.html
I have actually managed to give h the type signature.
The following message indicates that the problem is actually quite
common:
http://www.haskell.org/pipermail/haskell-cafe/2003-May/004302.html
Here's an example of an anomaly with higher-rank types:
http://www.haskell.org/pipermail/haskell-cafe/2004-October/007207.html
http://www.haskell.org/pipermail/haskell-cafe/2004-October/007212.html
we can define functions Foo and Bar (data constructors are functions)
such that we can write
> myFoo :: Int -> Foo
> myFoo i = Foo (Bar run op) where
> run :: Monad m => StateT Int m a -> m a
> run prog = do (a, s) <- runStateT prog i
> return a
> op :: Monad m => StateT Int m Int
> op = get
but we cannot write the composition of Foo and Bar more directly:
> foo run op = Foo (Bar run op)
The latter is not accepted: it must have a signature but no signature
can ever be given to this function.
More information about the Haskell-Cafe
mailing list