It sounds like what you are asking for is, for a given equational system $\cal E$, to give a canonical representation for equivalence classes modulo $\cal E$.
Indeed, if your signature is the binary operation $\_\cdot\_$, and your equation is
$$ (x\cdot y)\cdot z=x\cdot(y\cdot z)$$
then you can represent any element as $a_1\cdot(a_2\cdot(\ldots\cdot a_n)\ldots)$ (where the $a_i$) are atoms. As Derek Elkins points out, a good way to do this is to apply Knuth-Bendix completion to $\cal E$, (possibly) obtaining a rewrite system $\cal R$ that is confluent and terminating and computes, for each term $t$, a unique element that is a representative of $t$'s equivalence class under $\cal E$.
Now it is useful to note that in this case, the set of canonical forms happens to be isomorphic to the data types of lists of atoms. The fact that elements of an algebraic datatype captures the equivalence classes is not obvious, and is not true in general: if you add commutativity, that is the equation
$$ x\cdot y = y\cdot x$$
then it's clear that there is no algebraic (first-order) datatype that captures exactly the normal forms, as this is isomorphic to sorted lists of atoms.
A reasonable question is to ask whether there is always such a data structure using dependent types. In particular, there is a version of sorted list using dependent types, namely:
data SortedList =
Nil : SortedList
Cons : forall x:Atom, forall l:SortedList , x <= min l -> SortedList
taking inspiration from this agda code. Note that min needs to be defined on SortedList, making this an inductive-recursive definition, but I'm pretty sure this can be avoided with a little more messiness (say, embedding list into sorted list).
I think the question needs to be made more precise though, because there is a type in extensional dependent type theory such that each element of that type represents exactly one equivalence class: namely, the type of all equivalence classes! It can be defined by
$$ \mathrm{Q}_E:=\{y|\exists x, \overline{x} = y\}$$
where $\overline{x}$ is defined by:
$$\overline{x}=\{z| z=_E x\} $$
In general, quotient types are a tricky subject in type theory though, especially without sufficient extensionality, see e.g. Pragmatic Quotient Types by Cyril Cohen.
In conclusion:
- In the naive version of your question, the answer is that it is impossible to associate an inductive data type to an equational theory such that each element of the type represents a unique class.
- It is sometimes possible to compute a rewrite system which computes a unique representative of that class if the algorithm terminates and succeeds.
- When allowing for dependent types, the question becomes more complex and is, I believe, still somewhat open, with some progress.
