۱۶ - ۱۵اگه بخوایم کار متفاوتی انجام بدیم چطور؟

گفتیم از ‏‎Functor‎‏ برای لیفت کردنِ توابع از روی ساختار‌ها استفاده می‌کنیم تا بدونِ دست زدن به اون ساختار، فقط محتویات‌ش رو تغییر بدیم. حالا اگه بخوایم فقط ساختار رو تغییر بدیم و آرگومانِ تایپیِ اون ساختار یا نوع‌ساز رو دست نزنیم چطور؟ با این موضوع، می‌رسیم به تبدیلات طبیعی. میشه سعی کنیم و تایپی بنویسیم که خواسته‌مون رو بیان کنه:

nat :: (f -> g) -> f a -> g a

چنین تایپی غیرممکنه، چون نمیشه برای یه تایپِ تابع، از تایپ‌های گونه‌بالا به عنوانِ آرگومان‌های تایپی‌ش استفاده کرد. ولی مشکل کجاست؟ خیلی شبیهِ تایپ سیگنچر ِ ‏‎fmap‎‏ شده، اینطور نیست؟ با این تفاوت که ‏‎f‎‏ و ‏‎g‎‏ در ‏‎f -> g‎‏ تایپ‌های گونه‌بالا اند. باید باشن، چون اینها همون ‏‎f‎‏ و ‏‎g‎‏ هستن که آخرِ تایپ سیگنچر آرگومان می‌گیرن. اما اونجا به آرگومان‌هاشون اعمال شدن و دیگه کایند ِ ‏‎*‎‏ دارن.

پس با یه تغییرِ کوچیک درست‌ش می‌کنیم.

{-# LANGUAGE RankNTypes #-}

type Nat f g = forall a . f a -> g a

میشه گفت داریم برعکسِ ‏‎Functor‎‏ رو انجام میدیم. ساختار رو تغییر میدیم و مقادیر رو دست‌‌نخورده حفظ می‌کنیم. اینجا کامل توضیح نمیدیم، اما سور ِ ‏‎a‎‏ در سمت راستِ تعریف، باعث میشه همه‌ی توابع با این تایپ، به محتویاتِ ساختار‌های ‏‎f‎‏ و ‏‎g‎‏ بی‌تفاوت باشن، خیلی شبیهِ تابع همانی که هیچ کاری با آرگومان‌ش نمی‌تونه انجام بده، غیر از اینکه دست‌نخورده پس‌ش بده.

از لحاظ گرامری، با این روش میشه از تعریفِ ‏‎a‎‏ در تایپِ ‏‎Nat‎‏ اجتناب کرد – که همون کاریه که لازم داریم، اصلاً قرار نیست هیچ اطلاعاتِ بخصوصی از محتویاتِ ‏‎f‎‏ و ‏‎g‎‏ داشته باشیم، چون فقط می‌خوایم ساختار رو تغییر بدیم، نمی‌خوایم فولد کنیم.

اگه سعی کنین ‏‎a‎‏ رو از آرگومان‌های تایپ، بدونِ سور کردن حذف‌ش کنین، خطا می‌گیرین:

Prelude> type Nat f g = f a -> g a

Not in scope: type variable ‘a’
-- a م. در گستره نیست: متغیرِ تایپیِ

بدونِ روشن کردنِ ‏‎RankNTypes‎‏ (یا ‏‎Rank2Types‎‏) هم نمیشه سورکننده رو اضافه کنیم:

Prelude> :{
*Main| type Nat f g =
*Main|        forall a . f a -> g a
*Main| :}

Illegal symbol '.' in type
Perhaps you intended to use RankNTypes or a
similar language extension to enable
explicit-forall syntax:
  forall <tvs>. <type>

-- م. علامت غیرمجازِ '.' در تایپ
-- RankNTypes شاید قصد داشتین از
-- یا یه توسعه‌ی زبانیِ مشابه برای
-- .صریح استفاده کنین forall فعال کردنِ گرامرِ

اگه توسعه ِ ‏‎RankNTypes‎‏ رو روشن کنیم، درست کار می‌کنه:

Prelude> :set -XRank2Types
Prelude> :{
*Main| type Nat f g =
*Main|        forall a . f a -> g a
*Main| :}
Prelude>

برای اینکه ببینیم این سور از چه جور چیزی جلوگیری می‌کنه، مثالِ زیر رو در نظر بگیرین:

type Nat f g = forall a . f a -> g a

-- این کار می‌کنه
maybeToList :: Nat Maybe []
maybeToList Nothing = []
maybeToList (Just a) = [a]

-- .کار نمی‌کنه، اجازه نیست
degenerateMtl :: Nat Maybe []
degenerateMtl Nothing = []
degenerateMtl (Just a) = [a+1]

یه نسخه از ‏‎Nat‎‏ که ‏‎a‎‏ رو در تایپ‌ش معرفی می‌کنه چطور؟

module BadNat where

type Nat f g a = f a -> g a

-- این کار می‌کنه
maybeToList :: Nat Maybe []
maybeToList Nothing = []
maybeToList (Just a) = [a]

-- a این هم اگه بهش بگیم
-- .هست، کار می‌کنه Num a => a
degenerateMtl :: Num a => Nat Maybe [] a
degenerateMtl Nothing = []
degenerateMtl (Just a) = [a+1]

اون مثال آخر در واقع نباید کار کنه، و اصلاً روشِ خوبی برای فکر کردن به تبدیلات طبیعی نیست. اینجا چیزهایی که نمی‌خوایم و چیزهایی که می‌خوایم رو در یه جایگاه گذاشتیم و به هردوشون دسترسی داریم. تبدیلات طبیعی این دوچیز رو صراحتاً از هم جدا می‌کنن و کاری می‌کنن که تابع اصلاً نتونه هیچ کاری با مقادیر انجام بده. اگه می‌خواین مقادیر رو تغییر بدین، یه فولد ِ معمولی بنویسین!

در فصلِ بعدی به مبحثِ تبدیلات طبیعی برمی‌گردیم، پس فعلاً جَوگیر نشین!