Есть такая функция:

import Data.List

f :: Ord a => [a] -> Bool
f xs = minimum xs == head (sort xs)

Можете ли вы найти аргумент, для которого эта функция возвращает False, используя только предопределенные типы?

Здравствуйте, nikov, Вы писали:

N>Есть такая функция:

N>

N>import Data.List

N>f :: Ord a => [a] -> Bool
N>f xs = minimum xs == head (sort xs)
N>

N>Можете ли вы найти аргумент, для которого эта функция возвращает False, используя только предопределенные типы?

Такого быть не может, иначе надо писать баг-репорт...

N>>Можете ли вы найти аргумент, для которого эта функция возвращает False, используя только предопределенные типы?
G>Такого быть не может, иначе надо писать баг-репорт...

f [(),()]

Здравствуйте, thesz, Вы писали:

N>>>Можете ли вы найти аргумент, для которого эта функция возвращает False, используя только предопределенные типы?
G>>Такого быть не может, иначе надо писать баг-репорт...

T>f [(),()]

T>)

И кто тут выдаёт False?

Здравствуйте, thesz, Вы писали:

N>>>Можете ли вы найти аргумент, для которого эта функция возвращает False, используя только предопределенные типы?
G>>Такого быть не может, иначе надо писать баг-репорт...

T>f [(),()]

T>)

И HUGS, и GHC выдают True...

Здравствуйте, nikov, Вы писали:

N>Можете ли вы найти аргумент, для которого эта функция возвращает False, используя только предопределенные типы?

Легко могу написать

data TryThis = TryThis deriving (Ord)

instance Eq TryThis where
   _ == _ = False

Здравствуйте, Аноним, Вы писали:

А>Здравствуйте, nikov, Вы писали:

N>>Можете ли вы найти аргумент, для которого эта функция возвращает False, используя только предопределенные типы?

А>Легко могу написать
А>

А>data TryThis = TryThis deriving (Ord)

А>instance Eq TryThis where
А>   _ == _ = False
А>

Написано же вроде было только предопределенные типы или TryThis в Prelude появился?

Здравствуйте, geniepro, Вы писали:

G>Такого быть не может, иначе надо писать баг-репорт...

Может-может ;)

N>>>>Можете ли вы найти аргумент, для которого эта функция возвращает False, используя только предопределенные типы?
G>>>Такого быть не может, иначе надо писать баг-репорт...

T>>f [(),()]

T>>)

К>И кто тут выдаёт False?

Ай.

Здравствуйте, nikov, Вы писали:

N>Может-может

В report есть описание, как именно должен быть реализован sort и minimum?
Или я имею право заявить, что в моей имплементации minimum = head . sort и ответить, что таки такого быть не может (разумеется, unsafe'ы не используем)?
Или в таком случае тоже может?

Здравствуйте, VoidEx, Вы писали:

VE>Или я имею право заявить, что в моей имплементации minimum = head . sort и ответить, что таки такого быть не может (разумеется, unsafe'ы не используем)?

Если ты сделаешь такую реализацию для miminum, то конкретно эта проблема исчезнет, но останутся другие: все равно не для всех пар смежных элементов отсортированного списка будет (<=) будет возвращать True.

Здравствуйте, nikov, Вы писали:

N>Если ты сделаешь такую реализацию для miminum, то конкретно эта проблема исчезнет, но останутся другие: все равно не для всех пар смежных элементов
отсортированного списка будет (<=) будет возвращать True.

А можно узнать разгадку? Некоторые читатели форума (я, например) уже устали от саспенса.
Мне даже пришлось разобраться с Template Haskell и нагенерить тестов, но все равно не нашлось типа, для которого sort не сортирует:

{-# LANGUAGE TemplateHaskell #-}
module Main where

import Test.QuickCheck
import Data.List(sort)
import Data.Char(chr)
import GenTypes

prop_sort :: (Ord a) => [a] -> Bool
prop_sort xs = sorted (sort xs)
    where sorted xs = all (uncurry (<=)) (zip xs (tail xs))

type P a = [a] -> Bool
main = $(gentest)

instance Arbitrary Char where
    arbitrary = fmap chr (choose (0, 0x10FFFF-1))

-----------------------------------------------------------
module GenTypes where

import Language.Haskell.TH

gentest :: Q Exp
gentest = return $ DoE $ concatMap gen (take 1000 types)
    where types = concat $ iterate complicate $ map con ["()", "Char", "Bool", "Int", "Integer"] 
          complicate ts = map (AppT ListT) ts ++ 
                          [AppT (AppT (TupleT 2) t1) t2 | t1 <- ts, t2 <- ts] ++
                          [AppT (AppT (AppT (TupleT 3) t1) t2) t3 | t1 <- ts, t2 <- ts, t3 <- ts]

gen typ = [ NoBindS $ AppE (var "putStrLn") (LitE $ StringL $ show $ ppr typ),
            NoBindS $ AppE (var "quickCheck") (SigE (var "prop_sort") (AppT (con "P") typ)) ]

con = ConT . mkName
var = VarE . mkName

Здравствуйте, palm mute, Вы писали:

PM>А можно узнать разгадку? Некоторые читатели форума (я, например) уже устали от саспенса.
PM>Мне даже пришлось разобраться с Template Haskell и нагенерить тестов, но все равно не нашлось типа, для которого sort не сортирует:

import Data.List

f :: Ord a => [a] -> Bool
f xs = minimum xs == head (sort xs)

> let nan=0/0 in f [nan,0,nan,1,2,-1,nan]
False

По уму, compare для NaN должен или давать _|_, или считать их равными друг другу, но размещать их раньше других значений. Иначе появление одного NaN в списке полностью "отравляет" сортировку.

Вот, для сравнения, C# и F#. NaN-ы попадают в начало списка.

using System.Linq;
using System;
class Program
{
    static void Main() // после работы с haskell, жуткий синтаксический оверхед, который страшно раздражает :)
    {
        double nan = 0.0 / 0.0;
        foreach (var x in new[]{nan,0,nan,1,2,-1,nan}.OrderBy(x=>x,null))
        {
            Console.WriteLine(x);
        }
        
    }
}

let nan = 0.0/0.0 in List.sort_by id [nan; 0.0; nan; 1.0; 2.0; -1.0; nan];;

Здравствуйте, nikov, Вы писали:

N>

>> let nan=0/0 in f [nan,0,nan,1,2,-1,nan]
N>False
N>

Вот оно что. Про Float я совсем забыл, да и QuickCheck оказался здесь не слишком полезным, т.к. исключительные значения генерировать не умеет.

N>По уму, compare для NaN должен или давать _|_, или считать их равными друг другу, но размещать их раньше других значений. Иначе появление одного NaN в списке полностью "отравляет" сортировку.
Это обсуждалось, но безуспешно.

Здравствуйте, nikov, Вы писали:

N>По уму, compare для NaN должен или давать _|_, или считать их равными друг другу, но размещать их раньше других значений. Иначе появление одного NaN в списке полностью "отравляет" сортировку.

N>Вот, для сравнения, C# и F#. NaN-ы попадают в начало списка.

Насчёт "по уму" сложно говорить — в Си NaN-ы тоже выпадают из равенства и неравенства.
Следовательно, и qsort, и std::sort разламываются.

Ну а насчёт задницы — так, собственно, вот тебе и пример — задница может проявляться как угодно: исключением, зависанием, неверными результатами...

Здравствуйте, Кодт, Вы писали:

К>Ну а насчёт задницы — так, собственно, вот тебе и пример — задница может проявляться как угодно: исключением, зависанием, неверными результатами...

Неправильные результаты — это, конечно, задница. Но та задница, которой пользуются теоретики ЯП, никак не может проявляться неверными результатами.
Утвержение "выражение expr имеет тип T" означает, что если вычисление выражения завершится, то результат будет типа T. Если не завершится — то неважно как, исключением или зацикливанием, важен сам факт невозврата — тогда в системе типов нет дырок. Возврат неправильного результата — это не _|_.

Здравствуйте, palm mute, Вы писали:

PM>Неправильные результаты — это, конечно, задница. Но та задница, которой пользуются теоретики ЯП, никак не может проявляться неверными результатами.
PM>Утвержение "выражение expr имеет тип T" означает, что если вычисление выражения завершится, то результат будет типа T. Если не завершится — то неважно как, исключением или зацикливанием, важен сам факт невозврата — тогда в системе типов нет дырок. Возврат неправильного результата — это не _|_.

Согласен.
Получается, что NaN проковыривает дырку?
Хотя типам-то что. Типы остались на месте, а вот аксиоматика отношений поплыла.

Здравствуйте, Кодт, Вы писали:

К>Получается, что NaN проковыривает дырку?
К>Хотя типам-то что. Типы остались на месте, а вот аксиоматика отношений поплыла.

Интересно, что Haskell Report заявляет:

The Ord class is used for totally ordered datatypes.

Однако явных законов, которым его инстансы должны удовлетворять, не указано. В отличие, например, от Functor.

Еще одна проблема:

The functions abs and signum apply to any number and satisfy the law:

abs x * signum x == x

Для NaN это правило нарушается, хотя об этом ничего не сказано.

nikov,


N>

N>The functions abs and signum apply to any number and satisfy the law:
N>

abs x * signum x == x

N>Для NaN это правило нарушается, хотя об этом ничего не сказано.

Смотрим на выделенное. Утверждения выше можно эквивалентно переформулировать так: "Для любого числа x справедливо равенство abs x * signum x == x". Но NaN ::= Not A Number, то есть эта вещь находится вне условий утверждения.

Хотя возможно, число от не-чисел следовало бы отделять на уровне классов типов.

Здравствуйте, nikov, Вы писали:

N>Еще одна проблема:

The functions abs and signum apply to any number and satisfy the law:

abs x * signum x == x

N>Для NaN это правило нарушается, хотя об этом ничего не сказано.

Тогда до кучи ещё вспомним, что есть ещё -0.0:

Prelude> negate 0.0
-0.0

Здравствуйте, Lazy Cjow Rhrr, Вы писали:

LCR>Смотрим на выделенное. Утверждения выше можно эквивалентно переформулировать так: "Для любого числа x справедливо равенство abs x * signum x == x". Но NaN ::= Not A Number, то есть эта вещь находится вне условий утверждения.

Согласен. Но все же есть некоторая ирония в том, что NaN является значением типа, принадлежащего классу Num.

Здравствуйте, Lazy Cjow Rhrr, Вы писали:

LCR>Хотя возможно, число от не-чисел следовало бы отделять на уровне классов типов.

Как это? И какой тип тогда будет у операций, потенциально приводящих к NAN?
Не, конечно, можно арифметику лифтануть в Maybe, но тогда придётся туда же тащить и сравнения, а за сравнениями и логику.
Сделать это на уровне языка — это, считай, всё на свете придётся лифтить только ради избавления от UB.


В общем, есть три опции
— заменить UB на error — в местах возникновения метачисел NAN и INF (т.е. деление на 0 и т.п.) либо в местах их использования
— ввести определённость в операциях над метачислами — т.е. не нарушать аксиоматику
— предоставить пользователю самому следить за определённостью (путь языка Си)
и все эти опции не вылазят из имеющихся типов.

Определённость в аксиоматике, на самом деле, лишь отодвигает проблему.
Скажем, если мы договоримся, что числовой ряд (вещественный) устроен так: -INF -maxvalue .... -0 NAN +0 ..... +maxvalue +INF
то сортировка будет всегда определённой, но вот уже

abs_min = minimum . map abs -- если есть NAN, вернёт NAN
abs_max = maximum . map abs -- если есть ±INF, вернёт +INF
abs_max' = (1/) . abs_min . map (1/) -- если есть INF, вернёт NAN; если есть NAN и числа, опять вернёт NAN; если есть только нули, вернёт NAN

А для целых чисел получится ещё веселее — там NAN приобретает знак (оказываясь или меньше, или больше нуля).