[FoRK] alchemical type theory
dl at silcom.com
Mon Sep 27 13:11:42 PDT 2004
There is a system of correspondences
between how chemists classify "stuff"
and how programmers type data.
The least constrained lump of matter
is a mixture: different bits will be
of different compositions, and there
are mechanical means for separation.
Next, one has solutions, and uniform
composition within the lump, but not
with a universally fixed composition.
(steel is a solution of C in Fe, and
one can vary the amount of carbon in
the mix while keeping it still steel)
These can often be separated by heat,
as a still does for alcohol, or as a
subduction zone does for continental
Then one has compounds, with a fixed
composition: an ethanol alway has an
identical number of Cs and Os and Hs,
and without the correct ratio, there
is a good chance of getting "whiskey"
that's really wood alcohol.
Finally, there are elements: one may
burn hydrocarbons, splitting them up
into CO and H2O, but splitting up Us,
or separating the C12s from the C13s,
or transmuting some Pb into Au, is a
job for non-chemical mechanisms.
Moving across to the programming, an
unconstrained lump of data isn't any
particular type (in some domains, we
may say "document", but I don't know
of any general term); different bits
have different types, and we usually
need to parse or otherwise provide a
context to separate out the bits.
Next, one has recursive sum types: a
list has a uniform composition (each
node is either nil or a list element
and another node) but not one that's
universally fixed (there may well be
any given number of nodes before nil)
These can be separated explicitly: a
case-construct or conditional branch
is the usual suspect; or they can be
implicitly handled via polymorphism.
Then one has the product types, with
a fixed composition. (drinking wood
alcohol only induces blindess, but a
dereference of the pointer projected
from the tuple (char*, int) when the
data passed was a tuple (float, char)
will probably induce a segfault)
Finally, there are base types. Here
we have an advantage on the chemists
because we can always (until getting
to bare bool distinctions) find ways
to split any given lump of data, but
usually, for base types, we lack any
way to do it smoothly.
So, is plucking an overflow bit from
the middle of a register to handle a
BCD conversion a rough equivalent to
enzymes plucking out their preferred
isotope of carbon?
More information about the FoRK