الأشباح المعتمدة لها انعكاس بالمجان

نقدم نظرية الأنواع الشبحية (GTT) كنظرية أنواع معتمدة موسعة بكون جديد لبيانات الأشباح التي يمكن حذفها بأمان عند تشغيل برنامج، ولكنها ليست غير ذات أهمية كما في كون (المقترحات الصارمة). بدلاً من ذلك، تحمل بيانات الأشباح معلومات يمكن استخدامها في البراهين أو لتجاهل الحالات المستحيلة في الحسابات ذات الصلة. يمكن استخدام التحويلات لاستبدال القيم الشبحية بأخرى متساوية في الصياغة، ولكن من الضروري أنه يمكن تجاهل هذه التحويلات من أجل التحويل دون المساس بالصحة. نقدم إجراء لحذف البيانات الشبحية والبراهين يحافظ على النوع، وهي خطوة يمكن استخدامها كخطوة أولى لاستخراج البرنامج. نقدم نموذجًا نحويًا لـ GTT باستخدام تحويل برنامج يشبه تحويل البرامترية وبالتالي نوضح اتساق النظرية. وبما أنه نموذج من البرامترية، يمكن أيضًا استخدامه لاستنتاج نظريات حرة حول البرامج باستخدام كود الشبح. نمد GTT أيضًا لدعم انعكاس المساواة ونظهر أنه يمكننا القضاء على استخدامه دون الحاجة لل axioms الإضافية المعتادة لامتداد الدوال وخصوصية براهين الهوية. على وجه الخصوص، نؤكد على الإحساس بأن مؤشرات النوع الاستقرائي – مثل مؤشر الطول للمتجهات – ليست مهمة للحساب ويمكن اعتبارها بأمان ضمن نظرية معينة. تم صياغة نتائج الورقة في Coq.