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

[Greg Meredith]

Brandon,

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.

Best wishes,

--greg

On 8/11/07, Brandon Michael Moore <brandon at regurgitate.ugcs.caltech.edu>
wrote:
>
> 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
>



-- 
L.G. Meredith
Managing Partner
Biosimilarity LLC
505 N 72nd St
Seattle, WA 98103

+1 206.650.3740

http://biosimilarity.blogspot.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20070812/c1523710/attachment.htm