Tipo de sesión

En la teoría de tipos , los tipos de sesión se utilizan para garantizar la corrección en programas concurrentes . Garantizan que los mensajes enviados y recibidos entre programas concurrentes estén en el orden esperado y sean del tipo esperado . ^[1]^[2] Los sistemas de tipo de sesión se han adaptado tanto para sistemas de canal como de actor . ^[3]

Los tipos de sesión se utilizan para garantizar propiedades deseables en sistemas concurrentes y distribuidos , es decir, ausencia de errores de comunicación o bloqueos y conformidad con el protocolo. ^[4]

Tipos de sesiones binarias versus multipartidistas

La interacción entre dos procesos se puede comprobar utilizando tipos de sesión binarios , mientras que las interacciones entre más de dos procesos se pueden comprobar utilizando tipos de sesión multipartidista . ^[5] En los tipos de sesión multipartidista, las interacciones entre todos los participantes se describen utilizando un tipo global , que luego se proyecta en tipos locales que describen la comunicación desde la vista local de cada participante. Es importante destacar que el tipo global codifica la información de secuenciación de la comunicación, que se perdería si utilizáramos tipos de sesión binarios para codificar la misma comunicación. ^[6]

Definición formal de los tipos de sesiones binarias

Los tipos de sesiones binarias se pueden describir utilizando operaciones de envío ( ), operaciones de recepción ( ), ramas ( ), selecciones ( ), recursión ( ) y terminación ( ). ^[2] ${\estilo de visualización !}$ ${\estilo de visualización ?}$ ${\estilo de visualización \&}$ $\oplus$ $rec$ $fin$

Por ejemplo, representa un tipo de sesión que primero envía un booleano ( ), luego recibe un entero ( ) antes de terminar finalmente ( ). $S=\;!bool.?int.end$ ${\estilo de visualización S}$ $!bool$ ${\estilo de visualización ?int}$ $fin$

Implementaciones

Los tipos de sesión se han adaptado para varios lenguajes de programación existentes, incluidos:

lcanales ( Scala ) ^[7]
Efipio (Scala) ^[7]
Monitor ST (Scala) ^[8]
Conjuntos ^[9]
Tipos de sesión ( Rust ) ^[10]
sesión (óxido) ^[11]
Actores de sesión ( Python ) ^[12]
Sesión Monitoreada Erlang ( Erlang ) ^[13]
FuSe ( OCaml ) ^[14]
sesión-ocaml (OCaml) ^[15]^[16]
Sesión prioritaria ( Haskell ) ^[17]
Comprobador de estado de tipo de Java ( Java ) ^[18]^[19]^[20]
Sesiones rápidas ( Swift ) ^[21]

Referencias

^ Hüttel, Hans; Lanese, Iván; Vasconcelos, Vasco T.; Caires, Luis; Carbone, Marco; Deniélou, Pierre-Malo; Mostrous, Dimitris; Padovani, Luca; Ravara, Antonio; Tuosto, Emilio; Vieira, Hugo Torres; Zavattaro, Gianluigi (5 de abril de 2016). "Fundamentos de los tipos de sesiones y contratos de comportamiento". Encuestas de Computación ACM . 49 (1): 3:1–3:36. doi :10.1145/2873052. hdl : 2381/38761 . ISSN 0360-0300. S2CID 3580137.
^ ab Ancona, Davide (2016). Tipos de comportamiento en lenguajes de programación. Hanover, Massachusetts: Now Publishers. ISBN 978-1-68083-135-1.OCLC 1053840486 .
^ Fowler, Simon; Lindley, Sam; Wadler, Philip (10 de mayo de 2017). "Mezcla de metáforas: actores como canales y canales como actores (versión extendida)". arXiv : 1611.06276 [cs.PL].
^ Scalas, Alceste; Yoshida, Nobuko (junio de 2018). "Tipos de sesiones multipartidistas, más allá de la dualidad". Revista de métodos lógicos y algebraicos en programación . 97 : 55– 84. doi : 10.1016/j.jlamp.2018.01.001 . hdl : 10044/1/56777 . S2CID 48360420.
^ Honda, Kohei; Yoshida, Nobuko; Carbone, Marco (2008). "Tipos de sesiones asincrónicas multipartidarias". Actas del 35.º simposio anual ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación. págs. 273– 284. doi :10.1145/1328438.1328472. hdl :10044/1/26368. ISBN 9781595936899. Número de identificación del sujeto 53038488.
^ Yoshida, Nobuko; Gheri, Lorenzo (2019). Una introducción muy sencilla a los tipos de sesiones multipartidistas . ICDCIT 2020. doi :10.1007/978-3-030-36987-3_5.
^ ab "Programación de sesiones en Scala". alcestes.github.io . Consultado el 2 de noviembre de 2021 .
^ "STMonitor". chrisbartoloburlo.github.io . Consultado el 2 de noviembre de 2021 .
^ Harvey, Paul; Fowler, Simon; Dardha, Ornela; Gay, Simon J. (2021). "Tipos de sesiones multipartitas para una adaptación segura del entorno de ejecución en un lenguaje de actores". 35.ª Conferencia Europea sobre Programación Orientada a Objetos (ECOOP 2021) . 194 : 10:1–10:30. doi : 10.4230/LIPIcs.ECOOP.2021.10 . S2CID 234681015.
^ Jespersen, Thomas Bracht Laumann; Munksgaard, Philip; Larsen, Ken Friis (30 de agosto de 2015). "Tipos de sesiones para Rust". Actas del 11º Taller ACM SIGPLAN sobre programación genérica . WGP 2015. Asociación de Maquinaria de Computación. págs. 13 a 22. doi :10.1145/2808098.2808100. ISBN 9781450338103.S2CID18320631 .
^ Kokke, Wen (12 de septiembre de 2019). "Variación de Rusty: sesiones sin interbloqueos con fallos en Rust". Actas electrónicas en informática teórica . 304 : 48– 60. arXiv : 1909.05970 . doi :10.4204/EPTCS.304.4. ISSN 2075-2180. S2CID 198166990.
^ Yoshida, Nobuko; Neykova, Rumyana (29 de marzo de 2017). "Actores de sesión multipartidista". Métodos lógicos en informática . 13 (1). doi :10.23638/LMCS-13(1:17)2017. S2CID 65240382.
^ Fowler, Simon (10 de agosto de 2016). "Una implementación Erlang de actores de sesión multipartidistas". Actas electrónicas en informática teórica . 223 : 36– 50. arXiv : 1608.03321 . doi :10.4204/EPTCS.223.3. ISSN 2075-2180. S2CID 418549.
^ Padovani, Luca (2017). "Una implementación de biblioteca simple de sesiones binarias". Revista de programación funcional . 27 : e4. doi :10.1017/S0956796816000289. hdl : 2318/1634956 . ISSN 0956-7968. S2CID 19776781.
^ Imai, Keigo; Yoshida, Nobuko; Yuen, Shoji (marzo de 2019). "Session-ocaml: una biblioteca basada en sesiones con polaridades y lentes". Ciencia de la programación informática . 172 : 135– 159. doi : 10.1016/j.scico.2018.08.005 . hdl : 10044/1/63748 . ISSN: 0167-6423. S2CID : 69673075.
^ Imai, Keigo. "Sesión OCaml". www.ct.info.gifu-u.ac.jp . Consultado el 2 de noviembre de 2021 .
^ Kokke, Wen; Dardha, Ornela (26 de marzo de 2021). "Tipos de sesiones sin interbloqueo en Haskell lineal". arXiv : 2103.14481 [cs.PL].
^ "Comprobador de estado de tipo de Java". GitHub .
^ Bacchiani, Lorenzo; Bravetti, Mario; Giunti, Marco; Mota, João; Ravara, António (2022). "Un verificador de estado de tipos de Java que admite la herencia". Ciencia. Computadora. Programa . 221 : 102844. doi : 10.1016/j.scico.2022.102844 . hdl : 10362/145315 . S2CID 250940803.
^ Mota, João; Giunti, Marco; Ravara, António (2021). "Comprobador de estado tipográfico de Java". Actas de COORDINACIÓN 2021 . Apuntes de conferencias sobre informática. vol. 12717. págs. 121– 133. doi :10.1007/978-3-030-78142-2_8. ISBN 978-3-030-78141-5. Número de identificación del sujeto 235383301.
^ Rubicini, Alessio; Padovani, Luca (2023). "Swift Sessions: una implementación de biblioteca de tipos de sesión binarios en Swift". GitHub .

[1] Hüttel, Hans; Lanese, Iván; Vasconcelos, Vasco T.; Caires, Luis; Carbone, Marco; Deniélou, Pierre-Malo; Mostrous, Dimitris; Padovani, Luca; Ravara, Antonio; Tuosto, Emilio; Vieira, Hugo Torres; Zavattaro, Gianluigi (5 de abril de 2016). "Fundamentos de los tipos de sesiones y contratos de comportamiento". Encuestas de Computación ACM . 49 (1): 3:1–3:36. doi :10.1145/2873052. hdl : 2381/38761 . ISSN 0360-0300. S2CID 3580137.

[behavioraltypes-2] Ancona, Davide (2016). Tipos de comportamiento en lenguajes de programación. Hanover, Massachusetts: Now Publishers. ISBN 978-1-68083-135-1.OCLC 1053840486 .

[3] Fowler, Simon; Lindley, Sam; Wadler, Philip (10 de mayo de 2017). "Mezcla de metáforas: actores como canales y canales como actores (versión extendida)". arXiv : 1611.06276 [cs.PL].

[4] Scalas, Alceste; Yoshida, Nobuko (junio de 2018). "Tipos de sesiones multipartidistas, más allá de la dualidad". Revista de métodos lógicos y algebraicos en programación . 97 : 55– 84. doi : 10.1016/j.jlamp.2018.01.001 . hdl : 10044/1/56777 . S2CID 48360420.

[5] Honda, Kohei; Yoshida, Nobuko; Carbone, Marco (2008). "Tipos de sesiones asincrónicas multipartidarias". Actas del 35.º simposio anual ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación. págs. 273– 284. doi :10.1145/1328438.1328472. hdl :10044/1/26368. ISBN 9781595936899. Número de identificación del sujeto 53038488.

[6] Yoshida, Nobuko; Gheri, Lorenzo (2019). Una introducción muy sencilla a los tipos de sesiones multipartidistas . ICDCIT 2020. doi :10.1007/978-3-030-36987-3_5.

[alcestes-7] "Programación de sesiones en Scala". alcestes.github.io . Consultado el 2 de noviembre de 2021 .

[8] "STMonitor". chrisbartoloburlo.github.io . Consultado el 2 de noviembre de 2021 .

[9] Harvey, Paul; Fowler, Simon; Dardha, Ornela; Gay, Simon J. (2021). "Tipos de sesiones multipartitas para una adaptación segura del entorno de ejecución en un lenguaje de actores". 35.ª Conferencia Europea sobre Programación Orientada a Objetos (ECOOP 2021) . 194 : 10:1–10:30. doi : 10.4230/LIPIcs.ECOOP.2021.10 . S2CID 234681015.

[10] Jespersen, Thomas Bracht Laumann; Munksgaard, Philip; Larsen, Ken Friis (30 de agosto de 2015). "Tipos de sesiones para Rust". Actas del 11º Taller ACM SIGPLAN sobre programación genérica . WGP 2015. Asociación de Maquinaria de Computación. págs. 13 a 22. doi :10.1145/2808098.2808100. ISBN 9781450338103.S2CID18320631 .

[11] Kokke, Wen (12 de septiembre de 2019). "Variación de Rusty: sesiones sin interbloqueos con fallos en Rust". Actas electrónicas en informática teórica . 304 : 48– 60. arXiv : 1909.05970 . doi :10.4204/EPTCS.304.4. ISSN 2075-2180. S2CID 198166990.

[12] Yoshida, Nobuko; Neykova, Rumyana (29 de marzo de 2017). "Actores de sesión multipartidista". Métodos lógicos en informática . 13 (1). doi :10.23638/LMCS-13(1:17)2017. S2CID 65240382.

[13] Fowler, Simon (10 de agosto de 2016). "Una implementación Erlang de actores de sesión multipartidistas". Actas electrónicas en informática teórica . 223 : 36– 50. arXiv : 1608.03321 . doi :10.4204/EPTCS.223.3. ISSN 2075-2180. S2CID 418549.

[14] Padovani, Luca (2017). "Una implementación de biblioteca simple de sesiones binarias". Revista de programación funcional . 27 : e4. doi :10.1017/S0956796816000289. hdl : 2318/1634956 . ISSN 0956-7968. S2CID 19776781.

[15] Imai, Keigo; Yoshida, Nobuko; Yuen, Shoji (marzo de 2019). "Session-ocaml: una biblioteca basada en sesiones con polaridades y lentes". Ciencia de la programación informática . 172 : 135– 159. doi : 10.1016/j.scico.2018.08.005 . hdl : 10044/1/63748 . ISSN: 0167-6423. S2CID : 69673075.

[16] Imai, Keigo. "Sesión OCaml". www.ct.info.gifu-u.ac.jp . Consultado el 2 de noviembre de 2021 .

[17] Kokke, Wen; Dardha, Ornela (26 de marzo de 2021). "Tipos de sesiones sin interbloqueo en Haskell lineal". arXiv : 2103.14481 [cs.PL].

[18] "Comprobador de estado de tipo de Java". GitHub .

[19] Bacchiani, Lorenzo; Bravetti, Mario; Giunti, Marco; Mota, João; Ravara, António (2022). "Un verificador de estado de tipos de Java que admite la herencia". Ciencia. Computadora. Programa . 221 : 102844. doi : 10.1016/j.scico.2022.102844 . hdl : 10362/145315 . S2CID 250940803.

[20] Mota, João; Giunti, Marco; Ravara, António (2021). "Comprobador de estado tipográfico de Java". Actas de COORDINACIÓN 2021 . Apuntes de conferencias sobre informática. vol. 12717. págs. 121– 133. doi :10.1007/978-3-030-78142-2_8. ISBN 978-3-030-78141-5. Número de identificación del sujeto 235383301.

[21] Rubicini, Alessio; Padovani, Luca (2023). "Swift Sessions: una implementación de biblioteca de tipos de sesión binarios en Swift". GitHub .