Una de las grandes ventajas de los lenguajes funcionales puros es que permiten ser razonados ecuacionalmente, de esta forma, se facilita su depuracion, vericacion de la correccion, reduccion, etc. Pero esta pureza impide los efectos computacionales necesarios para que este tipo de programas tengan interaccion alguna, es por esto que las funciones monadicas, que se encargan de encapsular estos efectos y asi conservar la pureza, representan una estructura importante dentro de los lenguajes funcionales tales como Haskell. Sin embargo, debido a que las monadas poseen una estructura imperativa, no se ha podido establecer una manera de poder razonar ecuacionalmente sobre estas, el lograrlo supondria un avance significativo en lo que a verificacion de programas se refiere. Por tanto, se presentan los conceptos basicos que permitan comprender como se razona sobre los programas y se muestra mediante un ejemplo la posibilidad de razonar ecuacionalmente sobre funciones monadicas.