[Haskell-cafe] Re: towards a new foundation for set theory with atoms

[Brandon Michael Moore]

On Fri, Aug 10, 2007 at 03:54:23PM -0700, Greg Meredith wrote:
> Haskellians,
> 
> A quick follow up. If you look at the code that i have written there is a
> great deal of repeated structure. Each of these different kinds of sets and
> atoms are isomorphic copies of each other. Because, however, of the
> alternation discipline, i could see no way to abstract the structure and
> simplify the code. Perhaps someone better versed in the Haskellian mysteries
> could enlighten me.

You could take a less absolute view of the game, and describe each node
instead locally from the perspective of a player. Imagine Alice Bob and
Carol sitting around a table:

data ThreePlayers a b c =
   Next (ThreePlayer b c a)
 | Prev (ThreePlayers c a b)

In general you can get subgroups of a symmetric group as your sets of
colors this way (i.e, the set of elements of any group), I'm not quite
sure how much freedom you have in the sets of allowed transitions
(in particular, making some of the argument types identical can break
symmetry).

You could also go for the obvious big hammer, pretend that Haskell has
a strongly normalizing subset and encode inequality explicitly with
GADTs and such.

date Eq a b where Refl a a
data False
type Neq a b = Eq a b -> False
-- might be trouble if a and b are only equal non-constructively?

data Red = Red
data Green = Green
....

data Set color where
  Red :: Neq Red color -> Set Red -> Set color
  ...

Brandon