Es fácil representar magmas libres (árboles de hojas binarias), semigrupos libres (listas no vacías) y monoides (listas) libres, y no es difícil demostrar que realmente son lo que dicen ser. Pero los grupos libres parecen mucho más complicados. Parece que hay al menos dos enfoques para usar el habitualList (Either a) representación:

Codifique en un tipo el requisito que si tieneLeft a :: Right b :: ... entoncesNot (a = b) Y a la inversa. Parece probable que sea un poco difícil construirlos.Trabajar sobre una relación de equivalencia que permita la inserción / eliminación arbitraria deLeft a :: Right a :: ... pares (y al revés). Expresar esta relación parece horriblemente complicado.

¿Alguien más tiene una mejor idea?

Editar

Me acabo de dar cuenta de que la opción (1), que utiliza la única respuesta, simplemente no puede funcionar en la configuración más general. En particular, se hace imposible definir la operación del grupo sin imponer una igualdad decidible.

Editar 2

Debería haber pensado en Google esto primero. Parece que Joachim Breitnerlo hice en Agda Hace unos años, y según su descripción introductoria, parece que comenzó con la opción 1, pero finalmente eligió la opción 2. Creo que lo intentaré yo mismo, y si me atoro demasiado, miraré su código.