[Haskell-cafe] Optimization with Strings ?

Luke Palmer lrpalmer at gmail.com
Thu Dec 3 20:03:21 EST 2009


On Thu, Dec 3, 2009 at 12:21 PM, Alberto G. Corona <agocorona at gmail.com> wrote:
> " In fact, the correct answer is that pEqualsP should produce an error and
> qEqualsQ should never terminate"
>
> ¿¿???
> should? or you want to say "actually do that so the optimization does is not
> done"?
> The correct amswer is not the sould you mention, but True (IMHO). So the
> optimization can be done anyway.

No, the correct answer is actually _|_.  Returning True would violate
referential transparency:

p = [1..]

Now suppose p == p returned True.  Then we can substitute any name for
its value, by ref trans.  So p == [1..] should also return True.  This
is reasonable.  However, it is possible to prove (outside Haskell, but
still rigoroously in terms of its semantics) that [1..] = fix (\xs ->
1 : map (+1) xs).  So p == fix (1 : map (+1) xs) should also return
True.  This is getting unreasonable.  Such an expectation would seem
to require (==) to do a comprehensive proof search.

Luke


> 2009/12/3 Neil Brown <nccb2 at kent.ac.uk>
>>
>> Emmanuel CHANTREAU wrote:
>>>
>>> Le Thu, 3 Dec 2009 13:20:31 +0100,
>>> David Virebayre <dav.vire+haskell at gmail.com> a écrit :
>>>
>>>
>>>>
>>>> It doesn't work this way : Strings are just lists of Chars. Comparison
>>>> is made recursively, Char by Char. You can have a look at the source
>>>> to make sure :
>>>>
>>>> instance (Eq a) => Eq [a] where
>>>>    []     == []     = True
>>>>    (x:xs) == (y:ys) = x == y && xs == ys
>>>>    _xs    == _ys    = False
>>>>
>>>
>>> Hello
>>>
>>> Thank you David and Bulat for your answers.
>>>
>>> I don't see the proof you see. Because GHC could store two sames
>>> objects juste once and by the definition of == on lists it could deduce
>>> that "forall x; List x => x==x". GHC have all informations to do this
>>> optimization job, because haskell functions definitions are mathematics
>>> definitions.
>>>
>>
>> Besides any other reasons, Haskell has the error function, and infinite
>> lists.  Consider:
>>
>> p :: String
>> p = error "Haha!"
>>
>> q :: String
>> q = repeat 'a'
>>
>> pEqualsP :: Bool
>> pEqualsP = p == p
>>
>> qEqualsQ :: Bool
>> qEqualsQ = q == q
>>
>> By your rule, pEqualsP and qEqualsQ should be True.  In fact, the correct
>> answer is that pEqualsP should produce an error and qEqualsQ should never
>> terminate.  Since Strings can contain such errors and infinite lists, you
>> can't know for certain that an object equals itself without checking its
>> entire length, which is what the original definition for equals did anyway.
>>  There may be strict data structures for which your optimisation might be
>> applicable, though.
>>
>> Neil.
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>


More information about the Haskell-Cafe mailing list