É fácil representar magmas livres (árvores de folhas binárias), semigrupos gratuitos (listas não vazias) e monoides livres (listas), e não é difícil provar que eles realmente são o que afirmam ser. Mas grupos livres parecem muito mais complicados. Parece haver pelo menos duas abordagens para usar o método usualList (Either a) representação:

Codifique em um tipo o requisito de que, se você tiverLeft a :: Right b :: ... entãoNot (a = b) e o contrário. Parece provável que seja um pouco difícil construí-los.Trabalhe sobre uma relação de equivalência que permita a inserção / exclusão arbitrária deLeft a :: Right a :: ... pares (e vice-versa). Expressar essa relação parece terrivelmente complicado.

Alguém tem uma ideia melhor?

Editar

Acabei de perceber que a opção (1), que a única resposta usa, simplesmente não pode funcionar na configuração mais geral. Em particular, torna-se impossível definir a operação do grupo sem impor igualdade decidível!

Editar 2

Eu deveria ter pensado no Google primeiro. Parece que Joachim Breitnerfiz isso na Agda alguns anos atrás, e a partir de sua descrição introdutória, parece que ele começou com a opção 1, mas finalmente escolheu a opção 2. Acho que vou tentar por conta própria e, se ficar muito travado, examinarei seu código.