On Tue, Dec 18, 2012 at 11:53 PM, Christopher Howard < christopher.howard@frigidcode.com> wrote:
I really like the idea that all parts of my program could be cleanly and systematically composed from smaller pieces, in some beautiful design patter. Many of the problems in my practical programming, however, are not like the examples I have seen (nice pipes or unidirectional calculations) but rather complex fitting together of components. E.g., space ships are made up of guns + engines + shields + ammo. Different kinds of space ships may use the same kind of guns (reusable components) but some wont. Some will have many guns, some will have none.
So, suppose we have the types: data Gun = Gun { requiresAmmo :: Ammo } data Engine = ... data Ammo = ... data Shield = ... Now, we can build up a space ship in two basic ways: type SpaceShip = ([Gun], [Engine], [Shield], [Ammo]) mkSpaceShip :: [Gun] -> [Engine] -> [Shield] -> [Ammo] -> SpaceShip or we can define a data type: data SpaceShip = SpaceShip [Gun] [Engine] [Shied] [Ammo] or other variations. Note that, as morphisms, mkSpaceShip and 'SpaceShip' are "isomorphic", insofar as the objects they build are different representations of the same data -- both are "product" types. In any case, note that some spaceships can have lots of engines, and others can have none. Now, suppose we want a spaceship to actually do something. In particular, we might worry about pirate space ships: type PirateShip = SpaceShip and worry about whether your speedy ship can deal with them effectively. How would we model this? Here is an example: simulateBattle :: SpaceShip -> PirateShip -> Bool simulateBattle s@(SpaceShip gs es ss as) p@(SpaceShip gs' es' ss' as') = if es `subset` es' then mustFight s p else True -- Your ship ran away mustFight :: SpaceShip -> PirateShip -> Bool mustFight = undefined -- encode semantics about guns, shields, weight, etc here We claim that simulateBattle is a "morphism scheme" -- we can /say/ that it is a morphism from a variety of categories to a variety of categories. For example, by rearranging, we can view it as a morphism from (SpaceShape -> PirateShip) to Bool (as I said elsewhere, this kind of morphism isn't particularly useful to a programmer, since we can't analyze a function to produce a Bool -- being able to do so would mean we have solved the Halting problem) or from SpaceShip to (PirateShip -> Bool) or from (SpaceShip, PirateShip) to Bool or from (SpaceShip) to (PirateShip, Bool) Note that these choices have different representations as data structures, and that these structures might have very different properties in terms of space/time usage. Compositionality isn't "an" architecture. It's a property that lets us transform compositional architectures into other compositional architectures, while still maintaining the semantics we want. There are no "surprises" about the "meaning" of any of the simulateBattle types, even though their values might behave differently in space and time, because of the different data structures in play.