Desde hace ya un tiempo he pensado que la enseñanza de las Matemáticas Discretas puede aprovechar muy positivamente usar un lenguaje funcional puro como Haskell. Claro, no se usaría a efectos de las demostraciones (quizá como notación, pero no más), pero si sería muy útil para mostrar conceptos y propiedades de diferentes construcciones interesantes. En particular, sería sencillo mostrar que una cierta colección de objetos admite alguna estructura algebraica como un monoide, un grupo, etc.
¡Alabado sea Haskell, todopoderoso!
Tradicionalmente, estas estructuras algebraicas se construyen a partir de un conjunto llamado "carrier". Es mi opinión que tal construcción sería mucho más clara y útil si se hiciera a partir de tipos. Esto es, el carrier sería un tipo y las operaciones serían funciones sobre este tipo. ¡La cláusula de operación cerrada desaparece! Ya no hace falta, pues la declaración de tipos no permite operaciones mal formadas.
Por ejemplo, se podría definir un monoide como una tupla (T, +, e), donde:
- + : T → T → T
- e : T
- ∀ a, b, c : T (a + (b + c) = (a + b) + c)
- ∀ a : T (a + e = a ∧ e + a = a)
Y no hizo falta mencionar que el operador (+) es cerrado, ya que es obvio por su tipo (creo que el uso funciones currificadas da más flexibilidad a la hora de continuar explicando los conceptos en un futuro).
A continuación les dejo un enlace a un programa en Haskell que escribí con los conceptos básicos de grupoide, semigrupo, monoide y grupo implementados como clases de tipos. Así como 3 ejemplos: enteros, Z4 (hecho a mano) y grupos de permutaciones.
Enlace: algebra.hs
Creo que quedó bastante bonito y claro, aunque quizá sea que ya estoy acostumbrado a leer Haskell, jajaja (que no es muy lejano a leer matemática). ¿Que opinan? Mi intención es que algún día se incorporen nociones así a la práctica de las materias Estructuras Discretas I, II y III de la USB (y equivalentes de otras universidades, si se animan). Esto, creo yo, cumpliría dos objetivos fundamentales:
- El estudiante tendrá un mejor entendimiento de los conceptos al tener la oportunidad de jugar con ellos, equivocarse y contar con un entorno de compilación/ejecución que lo ayude y motive a mejorar.
- A veces los conceptos en Matemáticas Discretas quedan muy en el aire, demostraciones secas sin ningún motivo aparente. Claro, forman el pensamiento, pero realmente es mucho más que eso. Muchas de las construcciones que se ven en estas materias son la base de estructuras de datos complejas y sumamente eficientes usadas actualmente. Ver la relación desde temprano puede ayudar a que se le vea el queso a la tostada y haya una mayor motivación por entender y aprender.
Y bueno, esto es lo que quería compartir por ahora. Otro post gallito como para que no digan, jajaja. Cualquier sugerencia u opinión es más que bienvenida. ¡Hasta una próxima entrada! :D
tl;dr: para esto, Coq o Idris > Haskell. Prove all the things!
ResponderEliminarEstoy total y enfáticamente de acuerdo con que se use teoría de tipos para esos cursos. Yo iría aún más allá: debería usarse una teoría de tipos *también* en lógica simbólica, y por lo tanto una lógica constructiva en vez de una clásica.
Ahora, sobre usar específicamente Haskell…
«¡La cláusula de operación cerrada desaparece! Ya no hace falta, pues la declaración de tipos no permite operaciones mal formadas.»
Sí y no. Si te limitas al sublenguaje de Haskell que se comporta bien —es decir, si programas sin equivocarte y con cuidado—, sí, en efecto esta clase de malformación se excluye directamente por la firma de la clase, y hay un gran beneficio en usar una teoría de tipos de esta manera, incluso para la parte teórica de la materia. Pero Haskell no está basado en una lógica consistente y admite absurdos, por lo cual no creo que sea una buena idea usarlo con este fin. En efecto,
data Max a = Max a deriving (Eq, Ord)
instance Ord a => Grupoide (Max a) where (<.>) = max
instance (Ord a, Eq a) => SemiGrupo (Max a)
instance Ord a => Monoide (Max a) where e = e
Max no forma monoides a menos que el tipo tenga un valor máximo, así que esa instancia no debería ser definible. El análisis de tipos de Haskell no rechazará este error y admitirá la definición a pesar de que el objetivo pedagógico de todo esto tiene mucho que ver con la exclusión por construcción —pun intended— de cosas que no tienen sentido. Esto es lamentable y creo que resta mérito a este esfuerzo de pedagogía tan necesario. Claro que este ejemplo es bastante trivial, pero al trabajar con estructuras algebraicas más complejas, hay más oportunidades para que la declaración del tipo de la operación dé más garantías de exclusión de ideas mal formadas, más allá del tema del carrier: de hecho, con suficiente parametricidad (léase: cuantificación), el tipo con frecuencia determina o guía la implantación.
Una parte significativa de este problema se evita si se trabaja con herramientas similares en espíritu a Haskell, pero que hayan tomado decisiones de diseño más alejadas de su pragmatismo y más apegadas a la teoría — en particular, que fundamenten su análisis de tipos en una lógica consistente. Eso tiene una consecuencia directa: se debería usar un lenguaje total!
Entiendo que sería lindo usar Haskell directamente a pesar de este detalle problemático relativamente pequeño, ya que ese mismo pragmatismo es lo que permite que sea de inmensa utilidad para trabajo práctico en computación. Introducirlo temprano en la carrera podría ser una excelente manera de desmitificarlo. Sería interesante estudiar si ese objetivo se descarrilaría significativamente si se usa un lenguaje muy similar a Haskell, solo que total.
No pretendo sugerir que este no sea un problema potencialmente grande: sería triste que todo esto se percibiera al final como de utilidad puramente académica, como lo era con GaCeLa. Tampoco pretendo sugerir que se adopte un compromiso práctico y se sacrifique en exceso la correspondencia de «la prueba es correcta» con «el programa compila».
Entiendo que hacer fuerte esta correspondencia *no* es el objetivo de la idea sugerida en este post: tú sugieres únicamente que deberíamos usar Haskell como lenguaje para ilustrar los conceptos y quizá como notación informal. Yo digo que vayamos más allá: usemos una herramienta que no solo nos sirva para ilustrar la idea de estructuras algebraicas, sino también para hacer razonamiento formal sobre ellas!
Tú y otros entienden mejor el lado pedagógico de estas decisiones — mi contribución a la discusión podría resumirse a darle consideración a Coq o al menos Idris, no solo a Haskell.
PS: Un recurso relacionado: una prueba de las leyes de Monoide para Maybe en Idris con su modo interactivo que se parece igualito a lo que ya se hace de deducción natural en Lógica Simbólica en la USB: https://www.youtube.com/watch?v=P82dqVrS8ik
Bueno, me habían borrado el comentario anterior que había hecho. Intentaré reproducirlo como pueda, jeje.
Eliminar¡Gracias por el comentario man! Me parece excelente investigar alternativas con sistemas de tipos más adecuados. En un principio planteaba Haskell, ya que es el lenguaje funcional puro que mejor manejo (de los otros había escuchado hablar y había visto código, pero nunca he programado en ellos).
Acerca de lo de la cláusula de operación cerrada, me refería a considerar el carrier como un tipo en general, no necesariamente como un tipo de Haskell, jeje. Aunque el ejemplo que propones es interesante. El compilador no se queja, palantemarik, pero al ejecutar si muere. Algo tan sencillo como "e :: Max Bool" se queda pegado. Esto es porque el monoide necesita algo más que Ord, en realidad le hace falta Bounded y definir la instancia de monoide como "e = minBound". Sería genial que el compilador pudiera darse cuenta de esto, pero tienes razón, no lo hace.
En el video que me pasaste de monoides en Idris casi me da un nerdgasm, jajaja. ¡Que GENIALMENTE GENIAL poder verificar simbólicamente propiedades asistido por el sistema de tipos! Sin embargo, hay algo que creo que puede afectar negativamente el esfuerzo pedagógico de una estrategia así. Por lo que vi en el video, el sistema de tipos de Idris permite calificar los tipos y tener tipos dependientes (y cosas extrañas en donde expresiones pueden aparecer como parte de un tipo). Esto puede tornarse confuso para una persona que nunca ha sido expuesto a un sistema de tipos tan complejo. Imagínate, si ya les cuesta en Haskell donde la distinción Expresión/Tipo es clara (en su mayoría), aquí es posible que se vuelvan un ocho total.
Igual creo que es una excelente propuesta y una que hay que considerar y estudiar a más profundidad. Termino este comentario con una de las cosas que, en mi opinión, es de las más difíciles al dedicarse a la docencia. Muchas veces algo que nos parece sencillo y natural puede ser solamente un reflejo de nuestra propia experiencia. Saber equilibrar el crecimiento profesional personal con lo que se puede exigir a una persona recién expuesta a un tema dado es sumamente complicado. Algo tipo que uno diseñe un parcial y lo puedas resolver en 15mins., quizá no implique que sea posible para un chamo en 2 horas (a pesar de la regla heurística *4). Esto es algo realmente complicado y con lo que tenemos que tener cuidado al diseñar esta propuesta de cambio. Sin embargo, creo que de verdad vamos a terminar generando algo bien bonito y útil. :D