Proof/тестирование корректности общих функций

Question

(Речь не идет о доказательстве теорем о тестировании на практике, как quickCheck)

Пусть f некоторых общей функцию

f :: RESTRICTIONS => GENERICS 

с некоторыми «желательными» свойствами (т.е. является а не хак, является неизменным, ...) обычно является чистой общей функцией Haskell.

Предположим, что мы хотим, чтобы проверить это, главный вопрос

если мы имеем (а) тестирование этой функции для одного определенного типа (например, Int), мы можем предположить, что это верно для всех типов? (соответствие ограничений, конечно)

(с «хорошо протестированы» Я имею в виду «все» функция {domain X properties} была протестирована)

Theorically мы можем быть уверены, но я не уверен, что если каким-то дополнительное свойство, ограничение, ... при создании экземпляра (т.е. компиляция), возможно, имеют влияние.

Спасибо!

Примечание тесты, возможно, использовать специфические свойства определенного типа (например, Int), но эти свойства не может быть частью испытанных свойств. Например. если Monoid является ограничением, ассоциативность может быть частью проверенных свойств (но не коммутативность, если это не ограничение).

Пример

пусть f

repeatedHeader :: Eq a => [a] -> Bool 
repeatedHeader (x:y:_) = x == y 
repeatedHeader _ = False 

test1 = repeatedHeader [1,1,2] == True 
test2 = repeatedHeader [1,2,3] == False 

Answer 1

Вы можете быть уверены только в тривиальном случае, что ОГРАНИЧЕНИЯ пустые или, по крайней мере, не упоминает типичный тип, о котором идет речь.

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

Итак, это вопрос обеспечения определенных свойств в случаях. И это, как правило, слабый момент, потому что законы типа класса в основном излагаются неформально. Например, Haskell не может и не помешает вам создать ошибочный экземпляр Eq или Ord.

Реальный пример будет испытанием функции, как:

f :: Num a => a -> a 

Теперь мы знаем, у нас есть типы, которые переполняются молча, как Int. Другие нет. Это тихо переносится в классе Num, потому что, ну, жизнь такая же. Следовательно, как только вы сделали все тесты, используя Double, вы все равно можете удивиться, если используете f на Int.

Answer 2

Нет, вы не можете быть уверены.

Рассмотрим

f :: (Fractional a) => a -> a 
f x = (2 * x^2 + 2)/(x^2 + 1) 

Вы бы теперь говорят, что, по-видимому f x ≡ 2. И, конечно,

Prelude> карта е [-2, -1,6 .. 3]
[2.0,2.0,2.0,2.0,2.0,2.0,2.0,2.0,2.0,2.0,2.0,2.0 , 2.0.2.0]

На самом деле, это доказуемо выполняется для всех аргументов Rational, а также для любого не трансфинитного реального типа. Тем не менее, это легко ломаются, когда вы позволяете более общий Fractional типов:

Prelude Data.Complex> е (0 + 1)
NaN: NaN +

Важным моментом является то, что в основном все Real типы имеют дополнительные законы, в частности x^2 >= 0, которые не относятся к общему Num кейсам.

---

Лучший пример может быть

g :: Num a => a -> a 
g = (+1) 

Наглядно g x > x, и это справедливо для всех Integer с. Но это на самом деле не всегда верно ...

Prelude Data.Modular> карта (((х :: ℤ/5) -> дх> х) fromInteger.) [0 .. 10]
[Правда , True, True, True, False, True, True, True, True, False, True]

---

Disconsidering численные проблемы с, например, Double.