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

2007-08-12 Thread 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 <[EMAIL PROTECTED]>
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


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

2007-08-11 Thread 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe