A type T
is a subtype of type M[X]
iff:
- There exists a function
unit
of typeX → M[X]
- There exists a function
bind
of type(M[X], X → R) → R
- For all
x:X
andf:X→R
:bind(unit(x),f) ≡ f(x)
The natural inclination is to ask, "What are the semantics here?" but it turns out that the semantics depend wholly on the