lev

Reading the book https://www.amazon.de/-/en/dp/0137262744 I finally got to algebraic specification; the book explained why multi-sorted algebras are used. Then it dawned on me that I have seen a similar construction in a disguise here: https://chaource.dreamwidth.org/231660.html

By the way, I couldn't find that book online in any form, which is a pity! It's a good tutorial book, it explains things clearly and simply. I wish I could read that book earlier.

In the context of programming languages, a single-sorted algebra is just an F-algebra of some functor F. That is, we must have a type T and a function p of type F T → T, and then (T, p) is an F-algebra.

What is a multi-sorted algebra? It is a construction involving several types and as many functors and functions. For example, we may have 3 types U, V, W and three functors F, G, H (each with 3 type parameters!). Then (U, V, W) is a 3-sorted algebra of the functor triple (F, G, H) if we have three functions of types:

p1 : F U V W → U
p2 : G U V W → V
p3 : H U V W → W

Functor algebras are used in two ways for programming language theory:

- As method signatures for typeclasses that define abstract data types with given method types.

- For defining algebraic data types as initial functor algebras.

There are the corresponding ways for using multi-sorted algebras:

- As method signatures for multi-parameter typeclasses. Such typeclasses can also serve as a full algebraic specification of several abstract data types at once.

- For defining algebraic data types that are mutually recursive, as initial functor algebras.

Trying to understand initial algebra-based definitions and Church encodings for mutually recursive types is what got me first enlightened on why such constructions might be useful.

Apart from the Church encoding and initial algebras, there are important connections between functor algebras, monad algebras, and typeclass laws that I have been exploring before:

https://chaource.dreamwidth.org/236514.html

https://chaource.dreamwidth.org/237852.html

Now with multi-sorted algebras, exactly the same constructions should work. Laws of multi-sorted algebras should be specified via algebras of multi-sorted monads.

What are multi-sorted monads?( Read more... )