---
tag: 86144NHH59
kind: concept
name: Abstract data type as an algebra
msc: [68Q65, 08A70]
sources:
  - url: https://en.wikipedia.org/wiki/Abstract_data_type
---

## Summary

In the algebraic approach to programming, an abstract data type is described by its operations and their equations.
It does not depend on a concrete memory layout.
Such a description is an algebraic specification: a [[many-sorted signature|WAQJJ5GX68]] together with a set of equations.
The data type itself is the [[initial algebra|R76EC56V9R]] of the specification, which is unique up to isomorphism.
So any two correct implementations behave in the same way.
This view, worked out in the 1970s, makes the correctness of an implementation a question about homomorphisms of algebras.

## Explanations

### L1 human

A programmer who uses a stack only needs to know what push, pop and top do, not how the stack is stored.
The algebraic view writes down these operations and the rules between them, such as "pop after push gives back the old stack".
Many different data structures obey these rules, and some obey extra rules by accident.
The intended data type is the one that obeys the rules and nothing more, and where every value is built by the operations.
This is the [[initial algebra|HVF403PQ4H]] of the rules, and it is the same up to renaming for every honest implementation.