functional programming - tipos - ¿Se debe escribir estáticamente un lenguaje que implementa mónadas?

sustancia corporea definicion

Question

Estoy aprendiendo el estilo de programación funcional. En Do not Fear the Monads , Brian Beckman hizo una presentación brillante sobre Monad. Mencionó que Monad se trata de la composición de funciones para abordar la complejidad.

Una mónada incluye una función de unit que transfiere el tipo T a un tipo amplificado M (T); y una función Bind que, dada la función de T a M (U), transforma el tipo M (T) en otro tipo M (U). (U puede ser T, pero no necesariamente).

Según entiendo, el lenguaje que implementa la mónada debe verificarse de forma estática. De lo contrario, no se pueden encontrar errores de tipo durante la compilación y "Complejidad" no se controla. Es mi entendimiento correcto?

Answer 1

Ciertamente, no es el caso que un lenguaje que implementa mónadas debe estar escrito de forma estática, como lo pide el título de su pregunta. Puede ser una buena idea, por las razones que describe, pero los errores que no se pueden detectar en tiempo de compilación nunca han detenido a nadie. Solo mira cuántas personas escriben PHP.

Answer 2

No, en php no es posible implementar mónadas. Necesitas cierres para eso. Sin embargo, el concepto de Maybe puede ser aún útil cuando simula la coincidencia de patrones con las clases:

abstract class Maybe {
abstract public function isJust();
public function isNothing(){
return !$this->isJust();
}
}
class Just extends Maybe {
protected $val = null;
public function __construct($val){
$this->val = $val;
}
public function isJust(){
return true;
}
public function getVal(){
return $this->val;
}
}
class Nothing extends Maybe {
protected $val = null;
public function __construct(){
}
public function isJust(){
return false;
}
}
function just(){
print "isJust";
}
function nothing(){
print "nothing";
}
function MaybeFunc(Maybe $arg){
if(get_class($arg) == ''Just''){
print "Just";
} else {
print "Nothing";
}
}
MaybeFunc(new Just(5));
MaybeFunc(new Nothing());

Answer 3

Necesitas cierres para la mónada estatal. Lo busqué, PHP tiene cierres desde 5.3. Entonces eso ya no sería un problema.

Answer 4

Hay muchas implementaciones de mónadas en lenguajes tipados dinámicamente:

• The Maybe Monad en Ruby
• OO Monads and Ruby (el sitio está inactivo, pero el artículo está disponible en Wayback Machine del Internet Archive )
• Mónadas en Ruby Parte 1: Identidad , Mónadas en Ruby Parte 1.5: Identidad , Mónadas en Ruby Parte 2: Tal vez (entonces otra vez Tal vez no)
• Mónadas en Ruby
• Mónadas en el Cheap I: The Maybe Monad en JavaScript , Más Mónadas en el Cheap: Inlined fromMaybe
• Mónadas en Ruby (con buena sintaxis!) , List Monad en Ruby y Python
• Haskell estilo mónada do notación para Ruby

En general, Church-Turing-Thesis nos dice que todo lo que se puede hacer en un idioma también se puede hacer en cualquier otro idioma.

Como probablemente pueda deducir de la selección de ejemplos anterior, soy (principalmente) un programador de Ruby. Entonces, solo como una broma, tomé uno de los ejemplos anteriores y lo reimplecé en un lenguaje del que no sé absolutamente nada , que generalmente se considera como un lenguaje no muy poderoso, y que parece ser el único lenguaje de programación en el planeta para el cual no pude encontrar un tutorial de Monad. Te puedo presentar ... la Identidad Monad en PHP:

<?php
class Identity {
protected $val;
public function __construct($val) { $this->val = $val; }
public static function m_return($a) { return new Identity($a); }
public static function m_bind($id_a, $f) { return $f($id_a->val); }
}
var_dump(Identity::m_bind(
Identity::m_return(1), function ($x) {
return Identity::m_return($x+1);
}
));
?>

No hay tipos de estática, ni genéricos, ni cierres necesarios.

Ahora, si realmente quiere verificar mónadas estáticamente, entonces necesita un sistema de tipo estático. Pero eso es más o menos una tautología: si desea verificar estáticamente los tipos, necesita un verificador de tipo estático. Duh.

Con respecto a su pregunta:

Según entiendo, el lenguaje que implementa la mónada debe verificarse de forma estática. De lo contrario, no se pueden encontrar errores de tipo durante la compilación y "Complejidad" no se controla. Es mi entendimiento correcto?

Tienes razón, pero esto no tiene nada que ver con las mónadas. En general, se trata de comprobación de tipos estáticos y se aplica igualmente a matrices, listas o incluso enteros aburridos.

También hay una gran confusión aquí: si busca por ejemplo implementaciones de mónada en C #, Java o C, son mucho más largas y mucho más complejas que, por ejemplo, el ejemplo de PHP anterior. En particular, hay toneladas de tipos en todas partes, por lo que ciertamente se ve impresionante. Pero la fea verdad es que: los sistemas tipo C, Java y C no son lo suficientemente poderosos como para expresar el tipo de Monad . En particular, Monad es un tipo polimórfico de rango 2, pero C # y Java solo son compatibles con el polimorfismo de rango 1 (lo llaman "genéricos", pero es lo mismo) y C no es compatible con eso.

Entonces, las mónadas de hecho no están testadas estadísticamente en C #, Java y C. (Esa es, por ejemplo, la razón por la cual las mónadas LINQ se definen como un patrón y no como un tipo: porque simplemente no se puede expresar el tipo en C #. Todo lo que hace el sistema de tipo estático es hacer la implementación mucho más compleja, sin ayudar realmente. Se requiere un sistema de tipo mucho más sofisticado como el de Haskell, para obtener una seguridad de tipo real para las mónadas.

Nota: lo que escribí arriba solo se aplica al tipo de monad genérico en sí, como señala @Porges. Sin duda, puede expresar el tipo de una mónada específica , como List o Maybe , pero no puede expresar el tipo de Monad . Y esto significa que no puede verificar el hecho de que " List IS-A Monad ", y no puede verificar el tipo de operaciones genéricas que funcionan en todas las instancias de Monad .

(Tenga en cuenta que verificar que Monad también obedezca las leyes de mónada además de conformarse con el tipo de mónada probablemente sea demasiado incluso para el sistema de tipos de Haskell. Probablemente necesite tipos dependientes y tal vez incluso un demostrador de teoremas automático completo para eso).