[Haskell-cafe] Problem with haskell types

[Job Vranish]

Yeah I recently ran into this myself. (
http://osdir.com/ml/haskell-cafe@haskell.org/2010-07/msg00020.html). It's
not a bug, just a limitation of haskell's inference algorithm for mutually
recursive groups of functions.

The problem is that haskell infers groups (the strongly connected
components) of mutually recursive functions monomorphically. This means that
all uses of the function in the group, and the definition, must all have the
same type. In haskell 98, there was no way to get around this (not even
with explicit type signatures), hence the rule that Russell pointed out in
haskell 98 report:
``If the programmer supplies explicit type signatures for more than one
variable in a declaration group, the contexts of these signatures must be
identical up to renaming of the type variables."
There was no meaningful way for this not be to be case with the old haskell
98 rules (since inferring such types was impossible).

However,

Most implementations of haskell now have a (non Haskell 98 compliant) rule
that breaks a function out of a mutually recursive group if it already has a
type signature. Usually GHC requires the explicit enabling of extensions
when functionality breaks with the haskell 98 standard, but in this case it
lets you get away with it. However, GHC _does_ require the RelaxedPolyRec
extension if you want to specify different contexts on your mutually
recursive function group.

I imaging this is mostly just because allowing it without
the extension would be contradicting an explicit rule in the haskell 98
standard. But there might be some monomorphism restriction like performance
issues with it too, I'm not sure.


There has also been some work on alternative algorithms that solve this
problem without the need for explicit type signatures. The mercury language
supports full polymorphic recursion. And there is a paper on a better
algorithm, that could potentially be used by haskell, here:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.98.4930

Phew, I think I got that all right, though I just learned this stuff myself
only a month ago, so I'm mostly just passing it on :)
Hope that helps clear things up :)

- Job

On Fri, Jul 30, 2010 at 5:34 PM, <roconnor at theorem.ca> wrote:

> I was one of the people on #haskell discussing this with Anupam.
>
> Note that that when you remove the signature of d, the result complies and
> ghci will state the inferred type of d is exactly the signature that you are
> not allowed to write.
>
> In my opinion, this is a bug in the Haskell 98 report where it says
>
> ``If the programmer supplies explicit type signatures for more than one
> variable in a declaration group, the contexts of these signatures must be
> identical up to renaming of the type variables.
>
> The problem is that we cannot give a type signature to d with exactly the
> constraints of d_test because d doesn't have any type variable in its type
> signature.
>
> At the very least the Haskell report should allow type checking to proceed
> if everything in a declaration group has a signature even if the signatures
> don't have identical constraints.
>
> A trac ticket is needed for Haskell 2011, if one doesn't already exist.
>
>
> On Sat, 31 Jul 2010, Anupam Jain wrote:
>
>  Hi,
>> I am having trouble getting a small program to compile. The helpful folks
>> at #haskell created a version of the
>> program that does compile -
>> http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28406#a28408 but it is not
>> very clear
>> to them (and to me) why the original program wouldn't type compile in the
>> first place.
>>
>> Here's the program that refuses to compile -
>>
>> module Delme () where
>>
>> data DecisionState = A | B | C | D
>>
>> d_test :: Eq b => b -> b -> DecisionState -> DecisionState -> ()
>> d_test test testVal trueState falseState =
>>    if (test == testVal)
>>     then d trueState
>>     else d falseState
>>
>> d :: DecisionState -> ()
>> d A = d_test True True B C
>> d B = d_test 1 2 C D
>> d C = d_test True False A B
>> d D = ()
>> I get an error like -
>>
>> Delme.hs:13:0:
>>     Contexts differ in length
>>       (Use -XRelaxedPolyRec to allow this)
>>     When matching the contexts of the signatures for
>>       d_test :: forall b.
>>                 (Eq b) =>
>>                 b -> b -> DecisionState -> DecisionState -> ()
>>       d :: DecisionState -> ()
>>     The signature contexts in a mutually recursive group should all be
>> identical
>>     When generalising the type(s) for d_test, d
>>
>> Putting in the extension does get the program to type check but the
>> original program should have type compiled
>> in the first place.
>>
>> The ironic thing we discovered is that if we remove the type declaration
>> for 'd', the program type checks, and
>> GHC then derives the exact same type which we removed!
>>
>> Can some of the smarter people in the room please shed more light on this?
>>
>> -- Anupam
>>
>>
>>
>>
> --
> Russell O'Connor                                      <http://r6.ca/>
> ``All talk about `theft,''' the general counsel of the American Graphophone
> Company wrote, ``is the merest claptrap, for there exists no property in
> ideas musical, literary or artistic, except as defined by statute.''
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100730/add6fde2/attachment.html