ابتدای محتوای صفحه

۱۵ - ۱۲زندگی بهتر با QuickCheck

اثبات قوانین معمولاً خیلی زحمت می‌بره، مخصوصاً اگه وَسطای کدنویسی باشیم و دائماً کُدمون تغییر کنه. پس اگه یه راه ارزون و کم‌زحمت داشته باشیم که تا حدی معلوم کنه در یه نمونه، قوانین به احتمال زیاد رعایت میشن خیلی مفیده. ‏‎QuickCheck‎‏ یه گزینه‌ی خیلی خوب برای چنین چیزی‌ه.

تأیید ِ شرکت‌پذیری با `‏‎QuickCheck‎‏`

شرکت‌پذیری ِ بیانیه‌های ساده‌ی حساب رو میشه با استفاده از تابعِ تساوی، روی دو نوع پرانتزگذاری تو REPL چک کرد:

-- اینها رو برابر می‌دونیم
-- شرکت‌پذیراند (*) ‎‏و‏‎ (+) ‎‏چون‏‎

1 + (2 + 3) == (1 + 2) + 3

4 * (5 * 6) == (4 * 5) * 6

البته این ثابت نمی‌کنه که شرکت‌پذیری برای همه‌ی ورودی‌های ‏‎(+)‎‏ و ‏‎(*)‎‏ حاکمه، ما هم قصد داریم این رو ثابت کنیم. رفیق قدیمی‌مون از جبر لاندا – تجرید! – برای این اثبات کافیه:

\ a b c -> a + (b + c) == (a + b) + c

\ a b c -> a * (b * c) == (a * b) * c

اما آرگومان‌ها تنها چیزهایی نیستن که بشه تجرید کرد. چطور میشه مشخصه ِ شرکت‌پذیری رو به صورتِ انتزاعی برای یه تابع نشون داد؟

\ f a b c ->
  f a (f b c) == f (f a b) c
-- (infix) یا میانوندی

\ (<>) a b c ->
  a <> (b <> c) == (a <> b) <> c

سورپرایز! آرگومان‌های تابعی رو می‌تونین به اسم‌های میانوندی هم انقیاد بدین.

asc :: Eq a
    => (a -> a -> a)
    -> a -> a -> a
    -> Bool 
asc (<>) a b c =
  a <> (b <> c) == (a <> b) <> c

حالا چه جوری این تابع رو به یه مشخصه که بشه با ‏‎QuickCheck‎‏ تست کرد تبدیل کنیم؟ سریع‌ترین و آسون‌ترین‌ش شبیهِ این میشه:

import Data.Monoid
import Test.QuickCheck

monoidAssoc :: (Eq m, Monoid m)
            => m -> m -> m -> Bool 
monoidAssoc a b c =
  (a <> (b <> c)) == ((a <> b) <> c)

برای اجرای تست باید تایپ‌های تابع رو تعیین کنیم تا ‏‎QuickCheck‎‏ بدونه چه تایپ‌هایی از داده ایجاد کنه.

حالا با این میشه شرکت‌پذیری ِ تابع‌ها رو چک کرد:

-- برای خلاصه‌نویسی
λ> type S = String
λ> type B = Bool
λ> quickCheck (monoidAssoc :: S -> S -> S -> B)
+++ OK, passed 100 tests.

تابعِ ‏‎quickCheck‎‏ با استفاده از تایپکلاسِ ‏‎Arbitrary‎‏، مقادیرِ تصادفی رو به عنوانِ ورودی به تابع میده تا تست‌شون کنه. با اینکه چنین کاری رایج‌ه، شاید نخوایم به وجود داشتنِ یه نمونه ِ ‏‎Arbitrary‎‏ برای تایپِ ورودیهامون اتکا کنیم. یکی از چندتا دلیل‌ش می‌تونه این باشه که تایپ مالِ خودمون نیست و ترجیح میدیم نمونه‌ی یتیم براش ننویسیم. یا می‌تونه تایپی باشه که خودش یه نمونه از ‏‎Arbitrary‎‏ داره، ولی ما گستردگی ِ متفاوتی از مقادیرِ تصادفی‌ش می‌خوایم؛ یا می‌خوایم کاری کنیم که علاوه بر مقادیرِ تصادفی، حتماً چندتا حالت مرزی ِ خاص هم تست بشن.

حتماً باید تایپ‌های مورد نظر رو اعلام کنیم تا ‏‎QuickCheck‎‏ بدونه از کدوم یکی از نمونه‌های ‏‎Arbitrary‎‏ مقادیرِ تصادفی برای تستینگ رو بگیره. اگه با تابعِ ‏‎verboseCheck‎‏ تست کنین، مقادیری که تست شدن هم می‌بینین.^* اگه بدون اعلام ِ تایپ برای آرگومان‌ها، با این تابع تست رو اجرا کنین:

Prelude> verboseCheck monoidAssoc
Passed:
()
()
()

(۱۰۰ بار تکرار)

م. لغتِ verbose یکی از لغاتِ پرکاربرد در علمِ کامپیوتره، که میشه گفت روده‌دراز معنی میده! معمولاً برای نوشته شدنِ تک‌تکِ مراحلی که یه دستور طی می‌کنه به کار میره.

این GHCi ِه که با بکارگیری تایپ‌های پیش‌فرض گازِتون گرفت (تو فصل تستینگ هم دیدیم). این پیش‌فرضی‌سازیِ تایپ در GHCi خیلی تحمیلی‌تره، که البته برای جلسه‌های تعاملی که می‌خواین یه کُدی رو سریع اجرا کنین و REPL خودش یه برنده برای تایپکلاس‌هایی که نمیدونه چطور خبر کنه انتخاب کنه، مناسبه. اگه همین مثال رو از یه فایل منبع کامپایل می‌کردین، GHC به مبهم بودنِ تایپ گله می‌کرد.

تستِ همانی ِ چپ و راست

از طریقِ همون کاری که برای شرکت‌پذیری کردیم، همانی ِ چپ و راست هم میشه با ‏‎QuickCheck‎‏ بررسی کرد:

monoidLeftIdentity :: (Eq m, Monoid m)
                   => m
                   -> Bool
monoidLeftIdentity a = (mempty <> a) == a

monoidRightIdentity :: (Eq m, Monoid m)
                    => m
                    -> Bool
monoidRightIdentity a = (a <> mempty) == a

اجرای اینها برای یه ‏‎Monoid‎‏ این نتایج رو داره:

λ> quickCheck (monoidLeftIdentity :: String -> Bool)
+++ OK, passed 100 tests.

λ> quickCheck (monoidRightIdentity :: String -> Bool)
+++ OK, passed 100 tests.

تستِ تاب تحملِ `‏‎QuickCheck‎‏`

یه مثال با یه ‏‎Monoid‎‏ ِ نامعتبر بزنیم ببینیم ‏‎QuickCheck‎‏ چی کار می‌کنه. تو این مثال می‌خوایم نشون بدیم که چرا ‏‎False‎‏ نمی‌تونه مقدار همانی ِ یه ‏‎Bool Monoid‎‏ باشه، همیشه مقدارِ ‏‎False‎‏ برگردونه و یه ‏‎Monoid‎‏ ِ معتبر هم باشه:

-- مشخصه‌های شرکت‌پذیری، همانی چپ، و
-- .همانی راست رو اینجا نیاوردیم
-- .اونها رو به نسخه‌ی خودتون اضافه کنین

import Control.Monad
import Data.Monoid
import Test.QuickCheck

data Bull =
    Fools
  | Twoo
  deriving (Eq, Show)

instance Arbitrary Bull where
  arbitrary =
    frequency [ (1, return Fools)
              , (1, return Twoo) ]

instance Monoid Bull where
  mempty = Fools
  mappend _ _ = Fools

type BullMappend =
  Bull -> Bull -> Bull -> Bool

main :: IO ()
main = do
  let ma = monoidAssoc
      mli = monoidLeftIdentity
      mri = monoidRightIdentity
  quickCheck (ma :: BullMappend)
  quickCheck (mli :: Bull -> Bool)
  quickCheck (mri :: Bull -> Bool)

وقتی تو REPL بارگذاری کنین و ‏‎main‎‏ رو اجرا کنین، خروجیِ زیر رو می‌گیرین:

Prelude> main
+++ OK, passed 100 tests.
*** Failed! Falsifiable (after 1 test)
Twoo
*** Failed! Falsifiable (after 1 test) 
Twoo

خب این به ظاهر ‏‎Monoid‎‏ برای ‏‎Bool‎‏، تستِ شرکت‌پذیری رو گذروند، اما سَرِ تست‌های همانی شکست خورد. برای اینکه دلیل‌ش رو ببینیم، قوانین، و ‏‎mempty‎‏ و ‏‎mappend‎‏ رو کنار هم میذاریم:

-- نمونه اینطور تعریف شده
mempty = Fools
mappend _ _ = Fools

-- قوانین همانی
mappend mempty x = x
mappend x mempty = x

-- آیا از قوانین تبعیت می‌کنه؟

-- mappend به خاطر نحوه‌ی تعریفِ
mappend mempty x = Fools
mappend x mempty = Fools

-- نیست، پس در x همون Fools
-- قانون همانی شکست می‌خوره.

موردی نداره ‏‎Fools‎‏ مقدارِ همانی باشه، اما اگه ‏‎mappend‎‏ همیشه مقدارِ همانی رو برگردونه، دیگه همانی نیست. رفتارش شبیه صفر نیست؛ اصلاً قبل از برگردوندن ِ ‏‎Fools‎‏، نگاه نمی‌کنه ببینه کدوم آرگومان‌هاش ‏‎Fools‎‏ اند. یه سیاهچاله‌ست که همه‌ش یه مقدار رو برمی‌گردونه، خب مفهومی هم نداره. منظورمون از اون صفری که گفتیم رو با ضرب، که هم یک همانی داره، و هم یک صفر نشون میدیم:

-- عدد صفره Sum برای mempty دلیل اینکه
0 + x == x
x + 0 == x

-- عدد یک‌ه Product برای mempty دلیل اینکه
1 * x == x
x * 1 == x

-- Product برای mempty دلیل اینکه
-- *عدد صفر *نیست
0 * x == 0
x * 0 == 0

استفاده از ‏‎QuickCheck‎‏ راه خیلی خوب و ارزونی برای اعتبارسنجیِ نمونه‌ها نسبت به قوانین‌شون‌ه. اینها رو باز هم می‌بینیم.

تمرین: شاید یه مانوید ِ دیگه

یه نمونه ِ ‏‎Monoid‎‏ برای تایپ ‏‎Maybe‎‏ بنویسین که نیازی به ‏‎Monoid‎‏ بودنِ محتویات‌ش نداشته باشه. با همون مشخصه‌های ‏‎QuickCheck‎‏ که برای قوانینِ ‏‎Monoid‎‏ نوشتیم، نمونه‌تون رو چک کنین.

-- فراموش نکنین که یه نمونه‌ی
-- .بنویسین First' برای Arbitrary
-- .اینطور چیزها رو همیشه نمیگیم

newtype First' a =
  First' { getFirst' :: Optional a }
  deriving (Eq, Show)

instance Monoid (First' a) where
  mempty = undefined
  mappend = undefined 

firstMappend :: First' a
             -> First' a
             -> First' a
firstMappend = undefined

type FirstMappend =
     First' String
  -> First' String
  -> First' String
  -> Bool

type FstId =
  First' String -> Bool

main :: IO ()
main = do
  quickCheck (monoidAssoc :: FirstMappend)
  quickCheck (monoidLeftIdentity :: FstId)
  quickCheck (monoidRightIdentity :: FstId)

خروجی مورد نظر برای این ‏‎Monoid‎‏ که برای ‏‎Optional‎‏/‏‎Maybe‎‏ نوشتیم، در صورت وجود، اولین مورد موفق رو برمی‌گردونه. یه جورایی میشه این رو فصل ِ منطقی ("یا") ِ نمونه ِ ‏‎Monoid‎‏ دونست.

Prelude> First' (Only 1) `mappend` First' Nada
First' {getFirst' = Only 1}
Prelude> First' Nada `mappend` First' Nada
First' {getFirst' = Nada}
Prelude> First' Nada `mappend` First' (Only 2)
First' {getFirst' = Only 2}
Prelude> First' (Only 1) `mappend` First' (Only 2)
First' {getFirst' = Only 1}

۱۵ - ۱۲زندگی بهتر با QuickCheck

تأیید ِ شرکت‌پذیری با ‏‎QuickCheck‎‏

تستِ همانی ِ چپ و راست

تستِ تاب تحملِ ‏‎QuickCheck‎‏

تمرین: شاید یه مانوید ِ دیگه

تأیید ِ شرکت‌پذیری با `‏‎QuickCheck‎‏`

تستِ تاب تحملِ `‏‎QuickCheck‎‏`