تایپ و کایند

تو این پست می‌خوام در مورد ماهیت تایپ‌ها بنویسم و ببینیم چی هستن. اگه برنامه‌نویسی می‌کنید توصیه می‌کنم نیم‌نگاهی داشته باشید!

به چشم مقدمه‌ای بر اون پست‌ها که قراره بنویسم بهش نگاه کنید!

هر عمل محاسبه‌ای رو میشه با «جایگذاری» انجام داد، مثلا توی عبارت‌های

x = 3
y = x * x

می‌تونیم ابتدا x رو جایگذاری کنیم

y = 3 * 3

و بعد ضرب رو اعمال کنیم

y = 9

یا توی عبارت

x = 2
y = 4
if x == y  then 0 else 20

ابتدا متغییرها رو جایگذاری می‌کنیم:

if 2 == 4 then 0 else 20

سپس عمل تساوری

if false then 0 else 20

و در نهایت ساختار if/else رو که اعمال کنیم عدد ۲۰ رو می‌گیریم.

به نظر خیلی راحت و بدون دردسر میاد، اما خالی از مشکل نیست. مثلا این عبارت رو در نظر بگیرید:

a = "11"
a * 2

چطوری قراره یک رشته رو در یک عدد ضرب کنید؟ آیا مثل JS عمل می‌کنید و ۱۱ رو به صورت عدد می‌بینید و جوابتون ۲۲ میشه یا مثل پایتون ۱۱۱۱؟ یا شاید مثل C خطا بدید که این کار غیرقانونیه؟

این که چطوری این قضیه هندل میشه به مسئله تایپ‌ها بر می‌گرده. مستقل از این که برنامه‌نویس ازش مطلع هست یا نه، توی زبان‌های مدرن هر مقداری توی کد یک تایپ داره و برنامه با توجه به تایپ‌ها تصمیم می‌گیره چه عملیاتی براش مجازه و چه عملیاتی به چه صورتی باید انجام بشه.

از دید ریاضیات، این مفهوم رو آقای چرچ توی simply typed lambda calculus مطرح می‌کنه و به طور کلی از این نوتیشن استفاده می‌کنه (همون نوتیشنی که رومی استفاده می‌کرد!)

x:T

یعنی مقدار x تایپ T رو داره. برای جمع اعداد مثلا، ممکنه به این صورت بنویسیم:

x: Num, y: Num |- add(x,y): Num

بخونید، اگر بدونیم که x و y عدد هستن، جمعشون هم عدد هست. در واقع به زبان C داریم می‌گیم:

Num add(Num x, Num y);

گفتیم تو این زبان‌ها همه چیز باید تایپ داشته باشه، می‌دونیم که تایپ x, y و add(x,y) عدد هست، اما تایپ add چی هست؟ چرچ به این ساختار abstraction می‌گه و اسم مدرنش تابع هست، به این صورت هم بیان میشه:

add : (Num, Num) -> Num

به عبارت دیگه، add ساختاریه که اگر بهش دو عدد بدیم بهمون عدد برمی‌گردونه.

گفتیم این ساختار یک «حساب» هست، پس احتمالا بین تایپ‌هامون باید جمع و ضرب هم تعریف بشه، که همون union و struct توی زبان‌های شبه C هستن. اما اجازه بدید به موضوع دیگری نگاه کنیم.

شاید ساختارهای جنریک رو توی زبان‌های مختلف دیده باشید، تایپ این ساختارها چی میشه؟ مثلا ساختار ArrayList<T> توی جاوا؟

ArrayList : * -> *

این ساختارها بهشون kind گفته میشه که به نوعی abstraction روی تایپ‌ها هستن. توابعی که ورودیشون یک تایپ هست و خروجیشون یک تایپ دیگه. ساده‌ترین kindی که داریم * هست، یعنی هر تایپ کامل (که توی رومی با any نشونش می‌دادیم). بعد از اون ساختارهای جنریک هستن که با * -> * نشون داده میشن، یعنی یک تایپ می‌گیرن و تایپ دیگری تحویل میدن. با این تعریف، ArrayList به خودی خود یک تایپ نیست، اما ArrayList یک تایپ هست و مثلا تابع at روش به این صورت تعریف میشه:

ArrayList.at : (ArrayList <T>, Integer) -> <T>

دقت کنید که تایپ خروجی به ورودی کایندِ ArrayList بستگی داره.

پس اینطور شد که ما یک سری مقدار داریم، مثل "Sajjad"، عدد ۳ یا تابع add. یک سری تایپ داریم که میگه این مقادیر کجا می‌تونن مصرف بشن یا چی تولید می‌کنن، مثل String, String -> Integer. و در نهایت یک سری kind داریم که می‌تونه تایپ‌های جدید برامون تولید کنه. آیا از این مرحله بیشتر هم میشه رفت؟ بله، اما ساختارنهایی stable نیست و ممکنه دچار تضاد بشه.

در کل دونستن این که مقدار و تایپ و کایند چی هستن بهمون کمک می‌کنه در مورد توانایی‌های زبان‌ها و ابزارها حرف بزنیم، با هم مقایسشون کنیم و برنامه‌هامون رو اصولی‌تر طراحی کنیم.