دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
دانلود کتاب Qualified Types: Theory and Practice (Distinguished Dissertations in Computer Science (No. 9))
دانلود کتاب انواع واجد شرایط: تئوری و عملی (پایان نامه های ممتاز در علوم کامپیوتر (شماره 9))
مشخصات کتاب
Qualified Types: Theory and Practice (Distinguished Dissertations in Computer Science (No. 9))
ویرایش:
نویسندگان: Mark P. Jones
سری: Distinguished Dissertations in Computer Science (No. 9)
ISBN (شابک) : 9780511663086, 9780521543262
ناشر: Cambridge University Press
سال نشر: 2003
تعداد صفحات: 170
زبان: English
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود)
حجم فایل: 2 مگابایت
قیمت کتاب (تومان) : 39,000
در صورت تبدیل فایل کتاب Qualified Types: Theory and Practice (Distinguished Dissertations in Computer Science (No. 9)) به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب انواع واجد شرایط: تئوری و عملی (پایان نامه های ممتاز در علوم کامپیوتر (شماره 9)) نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
توضیحاتی در مورد کتاب انواع واجد شرایط: تئوری و عملی (پایان نامه های ممتاز در علوم کامپیوتر (شماره 9))
این کتاب استفاده از انواع واجد شرایط را برای ارائه یک چارچوب کلی برای ترکیب چندشکلی و اضافه بار توصیف می کند. به عنوان مثال، انواع واجد شرایط را می توان به عنوان تعمیم کلاس های نوع در زبان تابعی Haskell و قضیه اثبات Isabelle مشاهده کرد. اینها به نوبه خود توسعه انواع برابری در استاندارد ML هستند. سایر کاربردهای انواع واجد شرایط شامل رکوردهای قابل توسعه و تایپ فرعی است. نویسنده با استفاده از فرمول بندی کلی انواع واجد شرایط، الگوریتم استنتاج نوع Damas/Milner را برای پشتیبانی از انواع واجد شرایط گسترش می دهد، که به نوبه خود مجموعه ای از انواع ممکن را برای هر عبارت مشخص می کند. علاوه بر این، او تکنیک جدیدی را برای ایجاد شرایط انسجام مناسب توصیف می‌کند که معنایی یکسان را برای همه ترجمه‌های ممکن از یک اصطلاح معین تضمین می‌کند. مسائل عملی که در پیاده‌سازی‌های بتن ایجاد می‌شوند نیز مورد بحث قرار می‌گیرند، به ویژه بر اجرای اضافه بار در Haskell و Gofer، یک سیستم برنامه‌نویسی عملکردی کوچک که توسط نویسنده توسعه یافته است.
توضیحاتی درمورد کتاب به خارجی
This book describes the use of qualified types to provide a general framework for the combination of polymorphism and overloading. For example, qualified types can be viewed as a generalization of type classes in the functional language Haskell and the theorem prover Isabelle. These in turn are extensions of equality types in Standard ML. Other applications of qualified types include extensible records and subtyping. Using a general formulation of qualified types, the author extends the Damas/Milner type inference algorithm to support qualified types, which in turn specifies the set of all possible types for any term. In addition, he describes a new technique for establishing suitable coherence conditions that guarantee the same semantics for all possible translations of a given term. Practical issues that arise in concrete implementations are also discussed, concentrating in particular on the implementation of overloading in Haskell and Gofer, a small functional programming system developed by the author.
فهرست مطالب
Cover......Page 1
Frontmatter......Page 2
Contents......Page 6
Summary of notation......Page 10
Acknowledgements......Page 13
1.1 Type systems for programming languages......Page 14
1.2 Type inference and polymorphism......Page 15
1.3 The choice between `all\' and `one\'......Page 16
1.5 Outline of thesis......Page 17
2.1 Basic definitions......Page 19
2.2 Type classes......Page 21
2.3 Subtyping......Page 24
2.4 Extensible records......Page 26
3 - Type inference for qualified types......Page 29
3.1 An extension of ML with qualified types......Page 30
3.2 Understanding type schemes......Page 31
3.3 A syntax-directed approach......Page 36
3.4 Type inference......Page 38
3.5 Related work......Page 42
4 - Evidence......Page 44
4.1 Simple implementations of overloading......Page 45
4.2 Overloading made explicit......Page 46
4.3 Predicate entailment with evidence......Page 48
4.4 Evidence, predicates and implementations......Page 49
4.5 Type classes and dictionaries......Page 50
4.6 Subtyping and coercion......Page 52
4.7 Implementation of extensible records......Page 53
5 - Semantics and coherence......Page 56
5.1 A version of polymorphic [GREEK SMALL LETTER LAMDA]-calculus with qualified types......Page 57
5.2 Translation from OML to OP......Page 59
5.3 The coherence problem......Page 61
5.4 A definition of equality for OP terms......Page 62
5.5 Ordering and conversion functions......Page 66
5.6 Syntax-directed translation......Page 71
5.7 Type inference and translation......Page 73
5.8 Coherence results......Page 75
5.9 Comparison with related work......Page 78
6.1 Evidence parameters considered harmful......Page 80
6.2 Satisfiability......Page 86
6.3 Incorporating the rule of subsumption......Page 89
7 - Type classes in Haskell......Page 91
7.1 Context reduction......Page 92
7.2 Implementation of type classes in HTC......Page 95
7.3 The problem of repeated construction......Page 97
7.4 Repeated construction caused by recursion......Page 98
7.5 Other opportunities for shared dictionaries......Page 105
7.6 Alternative implementations of dictionary construction......Page 112
8.1 The basic principles of GTC......Page 114
8.2 The Gofer implementation of dictionaries......Page 117
8.3 A concrete implementation......Page 121
9 - Summary and future work......Page 127
9.1 Towards a categorical semantics......Page 128
9.2 Constructor classes......Page 129
9.3 Reasoning in the presence of overloading......Page 131
10.1 Constructor classes......Page 134
10.2 Template based implementations......Page 135
10.3 Making use of satisfiability......Page 136
10.5 The use of subsumption......Page 137
Appendix A - Proofs......Page 139
References......Page 161
Index......Page 168
