Table Of Links Mesa de la izquierda ABSTRACT Abstracción 1 INTRODUCTION 1 Introducción 2 DEPENDENTLY-TYPED OBJECT-ORIENTED PROGRAMMING 2 Programación orientada a objetos 3 CASE STUDY 3 Estudio de casos 4 DESIGN CONSTRAINTS AND SOLUTIONS 4 Condiciones y soluciones de diseño 5 FORMALIZATION 5 Formalización 6 DE/REFUNCTIONALIZATION 6 DE/REFUNCIONALIZACIÓN 7 FUTURE WORK 7 Trabajo futuro 8 RELATED WORK 8 Trabajo relacionado 9   CONCLUSION AND REFERENCES 9 Conclusión y referencias Programación orientada a objetos de tipo dependiente Los programas típicos escritos en lenguajes orientados a objetos y funcionales tienen muchas diferencias.Vamos a mirar ahora cómo aparecen estas diferencias cuando consideramos los programas escritos en el estilo orientado a objetos. 2.1 Method Call Syntax and Self Parameters Los programadores orientados a objetos están familiarizados con el método de llamada sintaxis o.f(e) para invocar un método f tomando un argumento e en un objeto o. Esto a veces se presenta bajo el nombre de "sintaxis de llamada de función uniforme" como una notación alternativa para la llamada f(o, e), donde el primer argumento del método f se llama el parámetro propio. Como punto de partida, tomamos la prueba de Agda de la Figura 4.En esa prueba, los booleanos se definen como un tipo de datos, la negación se define como una función no dependiente de los booleanos a los booleanos, y neg_- inverso se define como una función dependiente de un booleano x a una prueba de que x es igual a neg(neg x). En nuestro sistema, queremos expresar tanto neg como neg_inverso sin utilizar funciones no dependentes o dependentes. def Bool.neg: Bool {True => False => True } Si queremos expresar la función dependiente neg_inverse como una observación en los booleanos de una manera similar, entonces tenemos que añadir una característica, autoparámetros. def (self: Bool.neg_inverse: Eq(Bool, self, self.neg) { True => Refl(Bool, True), False => Refl(Bool, False) } La refuncionalización de estos métodos con autoparámetros dicta la primera característica de los tipos de codata dependientes: autoparámetros en destructores. codata Bool { neg: Bool, (self: Bool).neg_inverse: Eq(Bool, self, self.neg) } Son los auto-parámetros en las declaraciones de codata los que nos dan el poder expresivo para representar adecuadamente las interfaces y clases verificadas en un estilo orientado a objetos. 2.2 Verified Interfaces and Classes Cuando verificamos estructuras de datos y algoritmos en lenguajes de tipo dependiente, podemos elegir entre dos enfoques generales: verificación intrínseca y extrinsica. Usando verificación intrínseca, definimos la estructura de datos o algoritmo junto con sus pruebas de corrección. Para verificar intrínsecamente estructuras de datos, comúnmente expresamos propiedades usando índices de tipo, como el número de elementos contenidos en una lista indexada de longitud. Podemos emplear un enfoque similar en un estilo orientado a objetos utilizando tipos de codata indexados [Thibodeau et al. 2016]. Usando índices de tipo, podemos asegurarnos de que las observaciones se llaman sólo en objetos que están en el estado correcto. codata Buffer(m: Nat) {Buffer(S(n)).read(n: Nat): Pair(Bool, Buffer(n)) } codef EmptyBuffer: Buffer(Z) {read(n) absurd } codef Singleton(b: Bool): Buffer(S(Z)) {read(n) => MkPair(Bool, Buffer(Z), b, EmptyBuffer) } Podemos ver que, como es habitual para la coincidencia de patrones dependientes, pueden surgir coincidencias de patrones imposibles que deben ser marcadas como absurdas. Es decir, cuando implementamos la interfaz de buffer para el buffer vacío no tenemos que implementar el método de lectura ya que nunca se puede llamar. Sin embargo, en este trabajo, vamos más allá de los tipos de codata indexados, que admiten un estilo de verificación intrínseco. También queremos apoyar el enfoque extrínseco, donde queremos separar nuestros objetos de sus especificaciones. Jacobs [1995] nos proporciona un concepto inicial de cómo alcanzar ese objetivo. Él propone un sistema de especificaciones coalgebraicas que se pueden utilizar para verificar clases orientadas a objetos. Como ejemplo, la Figura 5a muestra una especificación coalgebraica para un buffer de un elemento que muestra comportamiento de lectura persistente (PR): Después de que un elemento se haya almacenado, no puede ser reemplazado usando el método de la tienda. En su lugar, uno necesita llamar el método vacío para vaciar explícitamente el buffer. La lectura del buffer vacío devuelve un error. Esta especificación del buffer se da como un conjunto de afirmaciones que se refieren al estado del buffer. En nuestro sistema, podemos realizar este concepto utilizando autoparámetros en destructores, permitiéndonos expresar especificaciones como observaciones sobre tipos de codata. El tipo de codata en la Figura 5 define la interfaz verificada para buffers de lectura persistentes en nuestro sistema. 2.3 Dependent Functions A diferencia de la mayoría de las otras teorías de tipo dependiente, el tipo π de las funciones dependentes no es parte de nuestra teoría central, sino que puede ser definido en una biblioteca.El tipo π se define como un tipo de codata indexado sobre un tipo de familia p, para el cual utilizamos el tipo de función ordinario no dependiente: Los diseñadores de Java decidieron seguir este enfoque cuando introdujeron las abstracciones de lambda como ejemplos de interfaces funcionales [Goetz et al. 2014; Setzer 2003] en Java 8. Además de reducir la complejidad del lenguaje de núcleo, simplifican la situación si tenemos más de un tipo de función. Esto es el caso en sistemas subestructurales donde tenemos funciones lineales y no lineales. Por ejemplo, en el lenguaje de programación Rust, hay tres diferentes rasgos de función integrados Fn, FnOnce y FnMut, que difieren en la modalidad del receptor3. 2.4 Weak and Strong Dependent Pairs En la sección anterior, mostramos cómo definir el tipo π. Para el tipo π no teníamos otra opción que definirlo como un tipo codata4, pero para el tipo Σ podemos elegir si modelarlo como un tipo de datos o codata. Esta elección distingue los tipos Σ débiles y fuertes [Howard 1980]: Los tipos Σ fuertes se definen como un tipo de codata con dos proyecciones, donde la segunda proyección menciona el resultado de la primera proyección en su tipo de retorno; los tipos Σ débiles, por el contrario, se definen como un tipo de datos con un constructor que empareja el primer y el segundo elemento. Esta diferencia es más evidente si primero consideramos el caso de pares no dependientes, que también se puede escribir como un tipo de datos o codata. Estas dos representaciones se pueden obtener entre sí por defuncionalización y refuncionalización. Esto es aún el caso cuando generalizamos pares no dependientes al tipo Σ. Al igual que el tipo π en la Sección 2.3, el tipo Σ es indexado por una familia de tipos T. Como tipo de datos, es definido por un par constructor que toma el tipo familia T , un elemento x del tipo A y un testigo w como argumentos. Como un tipo de codata, todavía tenemos dos proyecciones π1 y π2 como en el caso de los pares no dependientes. Pero la segunda proyección ahora utiliza el autoparámetro para garantizar que un elemento de tipo T aplicado a selfπ .1 es devuelto. De hecho, Agda ya puede representar Σ-tipos de ambas maneras. Pero hay una advertencia: Agda no fue diseñado originalmente con los tipos de codata en mente, y sus tipos de codata se implementan sobre registros dependientes, lo que limita qué tipo de tipos de codata son posibles. Por ejemplo, el orden de los destructores en un tipo de codata se refiere a Agda, por lo que no podemos reordenar la primera y la segunda proyección. En nuestro sistema los destructores de un tipo de codata no están ordenados y pueden referirse mutuamente unos a otros, lo que refleja exactamente cómo las definiciones son recursivas mutuamente en el tapiz. Pero ¿por qué debemos preocuparnos por estas dos codificaciones alternativas del tipo Σ? Tomemos, por ejemplo, Eisenberg et al. [2021] que discutieron la adición de tipos existenciales a Haskell. Dado que Haskell es tanto perezoso como soporta la eliminación de tipos, Eisenberg et al. están impulsados a un diseño que utiliza tipos existenciales fuertes. Pensamos que usando el marco de los tipos de datos y codata podemos hacer que estos tipos de diferencias sean aún más claras. 2.5 Codata Encodings of Natural Numbers Desde el comienzo del cálculo de lambda, los investigadores han estado interesados en la codificación funcional de tipos de datos como booleanos, números naturales y listas. Ejemplos clásicos de codificación funcional son la codificación de tipos de datos de Church, Scott y Parigot (cf. Geuvers [2014]; Koopman et al. [2014]). Las funciones son desde nuestra perspectiva sólo una instancia particular de un tipo de codata, por lo que estamos interesados en el problema más general de codificación de codata en lugar de codificación funcional. Que la codificación de la Iglesia se puede obtener de la refuncionalización de un programa con números de Peano y una función iter ya ha sido observado por Ostermann y Jabs [2018]; reiteramos este ejemplo en la Figura 6. Podemos observar que el tipo codata en la Figura 6b que representa la codificación de la Iglesia de los números naturales no es recursivo. Esto corresponde al teorema bien conocido de que las codificaciones de la Iglesia pueden ser tipificadas en el sistema puro F. Si aplicamos el mismo método para obtener la codificación de Scott o Parigot de los números naturales, entonces podemos observar que el tipo codata resultante es recursivo. Esto corresponde al otro teorema bien conocido de que estas codificaciones no pueden ser tipificadas en el sistema puro F y requieren tipos recursivos. Geuvers [2001] mostró que estas codificaciones anteriores no pueden expresar la inducción o la eliminación dependiente. Una forma de obtener codificaciones funcionales tipificadas que pueden expresar la inducción es agregar una forma de auto-tipos al sistema; este tipo de codificación fue introducido por Fu y Stump [2014]. Aunque es difícil probar una correspondencia exacta, pensamos que la idea esencial de la codificación de Fu y Stump puede expresarse en nuestro sistema en la Figura 7 y Figura 8. En la Figura 7 hemos codificado la inducción utilizando un tipo de codata auxiliar StepFun que codifica el paso de inducción para un dado predicado P en números naturales. La inducción se expresa entonces como la observación ind sobre un número natural n que espera el caso base y el paso de inducción de la inducción como argumentos. El argumento n sobre el que definimos la observación ocurre en sí mismo en el tipo de retorno. Creemos que esto es otra evidencia de que los autoparámetros que introducimos en el sistema ocurren de forma natural cuando pasamos del no dependiente al dependiente. 
 
 
 Los autores: 
 
 
 
 
 David Binder Grupo Ingo Tim Süberkrüb Klaus Ostermann Authors: 
 
 
 
 
 David Binder Grupo Ingo Tim sobrecargado Klaus Ostermann 
 
 Este artículo está disponible en archivo bajo la licencia CC 4.0. Este artículo está disponible en archivo bajo la licencia CC 4.0. Xiv

Part of HackerNoon's growing list of open-source research papers, promoting free access to academic material.

Read My Stories

Why was the 'Hello' afraid to meet 'World'? Because every time they got concatenated, they lost their space!

Concatenation

Este audio es producido en el idioma original de la historia!

Repensar OOP a través de tipos y codificaciones dependientes

About Author

COMENTARIOS

ETIQUETAS

ESTE ARTÍCULO FUE PRESENTADO EN

Related Stories

La fuga rápida del sistema Claude Sonnet 3.5: un análisis forense

Nómadas digitales escuchen: lo que necesitan saber sobre la nueva visa DTV de Tailandia

Las capas invisibles: por qué las entrevistas con los usuarios son un activo irremplazable

Navegando por las aguas: desarrollo de aplicaciones RAG de nivel de producción con lagos de datos

La fuga rápida del sistema Claude Sonnet 3.5: un análisis forense

Nómadas digitales escuchen: lo que necesitan saber sobre la nueva visa DTV de Tailandia

Las capas invisibles: por qué las entrevistas con los usuarios son un activo irremplazable

Navegando por las aguas: desarrollo de aplicaciones RAG de nivel de producción con lagos de datos

Light-Mode

Classic

Newspaper

Minty

Dark-Mode

Neon Noir

Minty

HN StartUps