Haskell и NaN

А лисперы в это время спокойно пишут код и не парятся.

А что сделает сортировка со списком, в котором есть NaN?

Ужас:

Prelude Data.List> sort [0/0,2,3,0/0,0/0,0/0,5,6]
[2.0,5.0,6.0,NaN,NaN,NaN,3.0,NaN]

Чем определяется порядок элементов в списке в данном случае? Я очень сильно подозреваю, что это UB.

Беспорядочным переставлением NaN'ов, видимо. Т.к.

Prelude Data.List> compare (0/0) (0/0)
GT

Prelude> let a = 0/0
Prelude> let b = 0/0
Prelude> compare a b
GT
Prelude> compare b a
GT
Prelude> 

нифига, просто на двух нанах всегда GT :)

Сортировка с NaN-ами в Common Lisp:

* (sb-ext::set-floating-point-modes :traps nil)

* (defvar a (/ 0.0 0.0))

A

* (defvar aa2 (list a 5.0 a a 2.0 a  a a  6.0 a a 3.0 a  a))

AA2

* aa2

(#<SINGLE-FLOAT quiet NaN> 5.0 #<SINGLE-FLOAT quiet NaN>
 #<SINGLE-FLOAT quiet NaN> 2.0 #<SINGLE-FLOAT quiet NaN>
 #<SINGLE-FLOAT quiet NaN> #<SINGLE-FLOAT quiet NaN> 6.0
 #<SINGLE-FLOAT quiet NaN> #<SINGLE-FLOAT quiet NaN> 3.0
 #<SINGLE-FLOAT quiet NaN> #<SINGLE-FLOAT quiet NaN>)

* (stable-sort (copy-seq aa2) #'>)

(#<SINGLE-FLOAT quiet NaN> 6.0 5.0 #<SINGLE-FLOAT quiet NaN>
 #<SINGLE-FLOAT quiet NaN> 2.0 #<SINGLE-FLOAT quiet NaN>
 #<SINGLE-FLOAT quiet NaN> #<SINGLE-FLOAT quiet NaN> #<SINGLE-FLOAT quiet NaN>
 #<SINGLE-FLOAT quiet NaN> 3.0 #<SINGLE-FLOAT quiet NaN>
 #<SINGLE-FLOAT quiet NaN>)

* (stable-sort (copy-seq aa2) #'<)

(#<SINGLE-FLOAT quiet NaN> 2.0 5.0 #<SINGLE-FLOAT quiet NaN>
 #<SINGLE-FLOAT quiet NaN> #<SINGLE-FLOAT quiet NaN> #<SINGLE-FLOAT quiet NaN>
 #<SINGLE-FLOAT quiet NaN> 6.0 #<SINGLE-FLOAT quiet NaN>
 #<SINGLE-FLOAT quiet NaN> 3.0 #<SINGLE-FLOAT quiet NaN>
 #<SINGLE-FLOAT quiet NaN>)

Всё хуже — и на одном NaN тоже.

Prelude> let a = 0/0
Prelude> compare a 0.0
GT
Prelude> compare 0.0 a
GT

Т.е. при перестановке элементов списка результат compare не изменится, что и приводит к печальным последствиям.

А что ты ожидал? Как по твоему, ноль больше, чем неопределенность или меньше?

Как такое поведение согласуется с тем, что Double относится к тайпклассам Ord и Eq?

А почему такое поведение не должно согласоваться с тем, что Double относится к тайпклассам Ord и Eq?

Я имел в виду между NaN'ами и не NaN'ами.

Получается только так:

Prelude Data.List> sort $ filter (not . isNaN) [1, 0/0, 0/0, 0/0, 3, 1, 2, 0/0]
[1.0,1.0,2.0,3.0]

Вообще, если вдуматься, то тут все логично. Вот абстрагируйся от программирования и реши чисто математическую задачу: даны две последовательности из вещественных чисел, содержащих равное количество элементов (пусть будет n, как обычно). Построим новую последовательность вещественных чисел, i-ый член которой является результатом деления i-го элемента первой последовательности на i-ый член второй последовательности. Требуется, упорядочить элементы получившейся последовательности из n элементов, представляющих собой вещественные числа. Ты же не станешь спорить, что вещественные числа являются упорядоченным множеством?

Простая логика подсказывает, что некорректные результаты (неопределенности, получающиеся при делении на 0) необходимо фильтровать и в результате будем иметь последовательность не из n элементов, а из m элементов, где m<=n, но зато все элементы точно принадлежат множеству вещественных чисел.

GHC дает вполне определенные (и неправильные) ответы: всегда GT. На самом деле эти значения несравнимы.

Вот поэтому сортировка и пр. алгоритмы должны ругаться, а не делать вид, что всё хорошо. Потому что в результате сортировки, даже если выкинуть NaN-ы, получается неупорядоченный список (примеры выше в треде).

Т.е. наличие NaN-ов нарушает абстракцию Ord, Eq.

Смотри пример выше. NaN-ы нарушают «аксиомы» Ord и Eq. Поэтому применение полимофрных функций, которые ждут инстанса Ord (типа сортировки) дает на выходе чушь: см. пример выше в треде.

В то же время, сами эти функции написаны правильно, в предположении, что тип действительно удовлетворяет нужным свойствам типа аксиом линейного упорядочения.

С этим полностью согласен. Недоработка разработчиков языков программирования. Если компилятор не в состоянии выявить ошибку, то по крайней мере рантайм должен выявить такую серьезную проблему.

А вот по поводу аксиом и тому подобного неверно. Множество вещественных числе замкнуто относительно операции деления только при условии, что из множества будет выкинут 0. Эту особенность следует учитывать при разработке алгоритмов и их реализации в виде программ.

Тут, видимо, разработчики языков попали в техническую ловушку. С одной стороны, NaN не может (и не принадлежит на самом деле) принадлежать множеству вещественных чисел, но операции над типом Double должны по спецификации языка иметь результатом тип Double. Вот и пришлось им делать выбор. С одной стороны NaN формально принадлежит к типу Double (точнее, может быть к нему приведен), но в то же время, вещественным числом NaN не является.

Думаю, вам бы не понравилось, если бы вместо Double результат деления двух вещественных чисел имел бы тип Maybe или что-то подобное. Лишняя сущность, лишние телодвижения... А ведь то же самое пришлось бы проделать и с другими числовыми типами.

Думаю, вам бы не понравилось, если бы вместо Double результат деления двух вещественных чисел имел бы тип Maybe или что-то подобное.

может просто было бы лучше сразу останавливать выполнение программы.

NaN-ы не просто так придуманы, они на равных правах могут использоваться в вычислениях, просто как маркеры выхода параметра за пределы возможностей процессора.

Я о том, что арифметика IEEE 754 не является аппроксимацией R уже хотя бы потому, что значения (специально не говорю: числа) не являются линейно упорядоченными. R удовлетворяет аксиомам линейного упорядочения, а значения типа Double — нет.

Я честно говоря не вижу, в чём здесь правильный выход. Иногда хотелось бы и Maybe. Просто неприятно, что у меня нет никаких гарантий, что правильно определенная функция (sort) даст правильный ответ на некоторых типах, формально относящихся к Ord.

Иногда нет. Есть алгоритмы, которые рассчитывают, что могут получиться NaN-ы. Например, смотри сюда: http://www.cs.utexas.edu/~inderjit/public_papers/rrrpaper.pdf

Я ничего не имею против NaN-ов, просто замечаю, что они нарушают свойство линейной упорядоченности значений типа Double, который формально относится к Ord. Т.е. «абстракция протекает».

Что мешает в Haskell создать свой тип над Double с корректной, с вашей точки зрения, обработкой значения NaN? Определите операцию деления так, чтобы она выкидывала исключения, когда получается NaN, например.

sort() с удовольствием будет работать с вашим типом данных и даже не заметит разницы.

Проще включить floating point exceptions. Исключение будет сам процессор кидать.

Другое дело, что это не универсальный выход.

Просто неприятно, что у меня нет никаких гарантий, что правильно определенная функция (sort) даст правильный ответ на некоторых типах, формально относящихся к Ord.

Такой гарантии и быть не может, потому что нельзя запретить писать неправильные инстансы. Для Sum Double еще и инстанс Monoid есть, например, а ведь сложение над плавучкой не ассоциативно.

Для плавучки не то что Ord быть не должно, но и Eq. В SML, к примеру, проверка на равенство на плавучке не определена. С другой стороны, практика требует чтоб все эти неправильные операции для плавучки работали.

Я ничего не имею против NaN-ов, просто замечаю, что они нарушают свойство линейной упорядоченности значений типа Double, который формально относится к Ord. Т.е. «абстракция протекает».

вообще-то как раз не нарушают. Ибо если они никак не соотносятся (то есть они одновременно и больше, и меньше, и равны), то список на выходе формально верен.

то список на выходе формально верен

он был бы верен, если бы после фильтрации NaN'ов получался упорядоченный список

Вроде они честно говорят, что поддержка 754 частичная. Впрочем на hackage есть отдельный пакет: ieee754.

А как ты в принципе это представляешь ?

Prelude> :i Eq
class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool
  	-- Defined in GHC.Classes

Здесь ничего не сказано о том, что

(==) = not . (/=)

Я не про философию говорил, а про код:

Prelude> compare (0/0) 5
GT
Prelude> compare 5 (0/0)
GT

Ага, про Eq я тоже заметил.

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

Но тогда возникает вопрос — что дают тайпклассы

ad-hoc полиморфизм, очевидно же.

А разве задачи тайпклассов как-то связаны с обеспечением надежности инстансов?

Кстати интересно, могли бы зависимые типы как-то справится с описанной проблемой?

то список на выходе формально верен

он был бы верен, если бы после фильтрации NaN'ов получался упорядоченный список

вот же ж shit. А я сразу и не заметил!

#include <iostream>
#include <limits>
#include <list>
using namespace std;

void sort_nan( const initializer_list<double>& in )
{
	list<double> data( in );
	data.sort();

	for( double v : data ) cout << v << ' ';
	cout << endl;	
}

int main()
{
	double nan = numeric_limits<double>::quiet_NaN();

	sort_nan( { nan, 2, 3, nan, nan, nan, 5, 6 } );
	sort_nan( { 3, nan, 2, nan, 1, nan, nan, 6, 5, 0 } );
}

nan 2 3 nan nan nan 5 6 
0 1 2 3 nan nan nan nan 5 6 

...

        sort_nan( { 2, nan, nan, nan, 1, nan, 3, nan, nan, 6, nan, nan, 5, nan, 0 } );

Увы:

1 2 nan nan nan nan 3 nan nan 0 5 6 nan nan nan 

На закуску Matlab:

sort([ 2, nan, nan, nan, 1, nan, 3, nan, nan, 6, nan, nan, 5, nan, 0 ])

ans =

0 1 2 3 5 6 NaN NaN NaN NaN NaN NaN NaN NaN NaN

они читеры :)

#include <algorithm>
#include <iostream>
#include <limits>
#include <list>
#include <vector>
using namespace std;

bool compare_nan( double a, double b )
{
	static double nan = numeric_limits<double>::quiet_NaN();

	if( a != a ) return false;
	if( b != b ) return true;

	return a < b;
}

void sort_nan( const initializer_list<double>& in )
{
	list<double> data( in );
	data.sort( compare_nan );

	for( double v : data ) cout << v << ' ';
	cout << endl;	
}

int main()
{
	double nan = numeric_limits<double>::quiet_NaN();

	sort_nan( { 2, nan, nan, nan, 1, nan, 3, nan, nan, 6, nan, nan, 5, nan, 0 } );
}

0 1 2 3 5 6 nan nan nan nan nan nan nan nan nan

Есть у меня предположение, что это не читерство, а следование современной версии IEEE 754, в которой есть специальный предикат для полного упорядочения.

Подробности: http://publib.boulder.ibm.com/infocenter/db2luw/v9r5/index.jsp?topic=/com.ibm...

ieee 754 - это тоже читерство в любом случае. Так как NaN - это не число, а значит и сравнивать его с ним нельзя. Точка.

Иногда нет. Есть алгоритмы, которые рассчитывают, что могут получиться NaN-ы.

такой алгоритм, думаю, можно 100% пределеать так, чтобы он без этого костыля обходился.

Я как-то предлагал расшифровывать аббревиатуру NaN как «Not a NaN».