منو
 کاربر Online
1065 کاربر online

نظریه مدل

تازه کردن چاپ
علوم ریاضی > علو م رایانه
(cached)




نظریه نوع

img/daneshnameh_up/8/87/compics0075.jpg

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



مطالعه بیشتر

  • بنجامین پیرس، " نوع ها و زبانهای نویسی "، چاپ MIT، 2002.
  • لوکاکاردلی،" سیتم های نوع ،راهنمای علم کامپیتر و مهندسی ، آلن ب (Allen B) چاپ تاکر، بخش 103

پیوند های خارجی





تعداد بازدید ها: 9760


ارسال توضیح جدید
الزامی
big grin confused جالب cry eek evil فریاد اخم خبر lol عصبانی mr green خنثی سوال razz redface rolleyes غمگین smile surprised twisted چشمک arrow



از پیوند [http://www.foo.com] یا [http://www.foo.com|شرح] برای پیوندها.
برچسب های HTML در داخل توضیحات مجاز نیستند و تمام نوشته ها ی بین علامت های > و < حذف خواهند شد..