نظریه نوع
در عام ترین سطح،
نظریه نوع شاخه ای از
ریاضی و
منطق است که با دسته بندی نهادها (entity) به صورت
گروه هایی که نوع
type نامیده می شود سروکار دارد. از این نظر نظریه نوع بیشتر به
بعد متافیزیکی نوع مربوط می شود. نظریه نوع جدید تاحدودی برای پاسخ به
تناقص راسل (Russell) و خصوصیاتی که به طور برجسته در
ریاضیات پرینسیپیا«princpia)
راسل و
وایت هد «whitehead) بود اختراع شد.
با ظهور
کامپیترهای قدرتمند برنامه پذیر، و پیشرفت و توسعه زبان های برنامه نویسی، نظریه نوع کار بردی عملی در توسعه سیستم های نوع
زبان های برنامه نویسی یافته است. تعریف "سیستم نوع" در زبان های برنامه نویسی متفاوت است، اما تعریف زیر از
بنجامین سی، پیرس (benjamin C.Pierce) تقریباً با توافق کنونی مجمع نظریه نوع سازگار است:
یک سیستم نوع روشی نحوی و ظریف است که با دسته بندی جملات (phrase)، بسته به نوع مقادیری که به خود می گیرند، از حضور بعضی رفتارهای خاص در یک برنامه جلوگیری می کند.
(
نوع ها و زبان های برنامه نویسی، چاپ MIT،
2002)
به عبارت دیگر، یک سیستم نوع مقادیر برنامه را به مجموعه هایی به نام نوع تقسیم می کند (این کار"تخصیص نوع" نامیده می شود)، و بر اساس نوع هایی که به این صورت تخصیص می دهد بعضی رفتارهای برنامه را غیر مجاز می کند. برای مثال، یک سیستم نوع ممکن است مقدار "hello" را به عنوان
رشته و مقدار 5 را به عنوان
عدد دسته بندی کند و براساس تخصیص نوع مانع از جمع "hello" با 5 شود. در این نوع سیستم
"hello" + 5
غیر مجاز است. از این رو هر برنامه مجاز شمرده شده از طرف سیستم نوع از رفتار خطادار جمع کردن رشته ها و اعداد مصون خواهد بود.
طراحی و اجرای سیستم های نوع موضوعی به بزرگی خود موضوع زبان های برنامه نویسی است. در واقع، هوا داران نظریه نوع مدعی هستند که طراحی سیستم های نوع خود جوهره طراحی زبان برنامه نویسی است:
"سیستم نوع را درست طراحی کنید، زبان خود را طراحی خواهد کرد."
دقت کنید که نظریه نوع، که در این جا توصیف شده، به قوانین
نوع دهی استاتیک اطلاق می شود. سیتم ها و زبان های برنامه نویسی که از
نوع دهی پویا استفاده می کنند بررسی نمی کنند که آیا برنامه از مقادیر به درستی استفاده می کند، در عوض در هنگام اجرا، هنگامی که برنامه سعی در اجرای رفتاری دارد از مقادیر به اشتباه استفاده می کند، خطایی را اعلام می کند. به همین دلیل عده ای
نوع دهی پویا را نامی بی مسما برای آن می دانند. به هر حال این دو نبایدبا هم اشتباه گرفته شوند.
مطالعه بیشتر
- بنجامین پیرس، نوع ها و زبانهای نویسی ، چاپ MIT، 2002.
- لوکاکاردلی،" سیتم های نوع ،راهنمای علم کامپیتر و مهندسی ، آلن ب (Allen B) چاپ تاکر، بخش 103
پیوند های خارجی
گروه ها:
علم کامپیوتر |
منطق ریاضی
