نوع الجلسة

في نظرية الأنواع ، تُستخدم أنواع الجلسات لضمان صحة البرامج المتزامنة . فهي تضمن أن الرسائل المرسلة والمستلمة بين البرامج المتزامنة تكون بالترتيب والنوع المتوقعين . [ ^{1 ] [ 2 ] وقد} تم تكييف أنظمة أنواع الجلسات لتناسب كلاً من أنظمة القنوات وأنظمة الممثلين . ^{[ 3 ]}

تُستخدم أنواع الجلسات لضمان الخصائص المرغوبة في الأنظمة المتزامنة والموزعة ، أي عدم وجود أخطاء في الاتصال أو حالات تعطل، والامتثال للبروتوكول. ^{[ 4 ]}

يمكن التحقق من التفاعل بين عمليتين باستخدام أنواع الجلسات الثنائية ، بينما يمكن التحقق من التفاعلات بين أكثر من عمليتين باستخدام أنواع الجلسات متعددة الأطراف . ^{[ 1 ] [ 5 ]} في أنواع الجلسات متعددة الأطراف، تُوصف التفاعلات بين جميع المشاركين باستخدام نوع عام ، والذي يُسقط بعد ذلك إلى أنواع محلية تصف الاتصال من وجهة نظر كل مشارك. ومن المهم أن النوع العام يُشفّر معلومات تسلسل الاتصال، والتي ستُفقد إذا استخدمنا أنواع الجلسات الثنائية لتشفير نفس الاتصال. ^{[ 6 ]}

يمكن وصف أنواع الجلسات الثنائية باستخدام عمليات الإرسال (${\displaystyle$ !} ), عمليات الاستقبال (${\displaystyle$ } ), الفروع (${\displaystyle \&}$), اختيارات (${\displaystyle \oplus }$), التكرار (${\displaystyle rec}$) والإنهاء (${\displaystyle end}$). ^{[ 2 ]}

على سبيل المثال،${\displaystyle S=\;!bool.?int.end}$يمثل نوع الجلسة${\displaystyle S}$الذي يرسل أولاً قيمة منطقية (${\displaystyle !bool}$ثم يستقبل عددًا صحيحًا (${\displaystyle ?int}$) قبل الإنهاء النهائي (${\displaystyle end}$).

تم تكييف أنواع الجلسات مع العديد من لغات البرمجة الموجودة، بما في ذلك:

• قنوات l ( سكالا ) ^{[ 7 ]}
• Effpi (Scala) ^{[ 7 ]}
• STMonitor (Scala) ^{[ 8 ]}
• EnsembleS ^{[ 9 ]}
• أنواع الجلسات ( راست ) ^{[ 10 ]}
• جلسة (راست) ^{[ 11 ]}
• ممثلو الجلسة ( بايثون ) ^{[ 12 ]}
• جلسة مراقبة إرلانج ( إرلانج ) ^{[ 13 ]}
• FuSe ( OCaml ) ^{[ 14 ]}
• session-ocaml (OCaml) ^{[ 15 ] [ 16 ]}
• جلسة ذات أولوية ( هاسكل ) ^{[ 17 ]}
• مدقق حالة النوع في جافا ( جافا ) ^{[ 18 ] [ 19 ] [ 20 ]}
• جلسات Swift ( Swift ) ^{[ 21 ]}