[Haskell-cafe] Re: towards a new foundation for set theory with
lgreg.meredith at biosimilarity.com
Sun Aug 12 09:49:42 EDT 2007
Cool. Well spotted. i was thinking a lot about the symmetry in the type
space as a kind of group. i'll play around with your suggestion.
On 8/11/07, Brandon Michael Moore <brandon at regurgitate.ugcs.caltech.edu>
> 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
> > great deal of repeated structure. Each of these different kinds of sets
> > 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
> > 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
> 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
505 N 72nd St
Seattle, WA 98103
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe