Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Ryan Ingram]

Also, I have to admit I was a bit handwavy here; I meant P in a
metatheoretic sense, that is "P(a) is some type which contains 'a' as a
free variable", and thus the 'theorem' is really a collection of theorems
parametrized on the P you choose.

For example, P(a) could be "Show a & a -> Int"; in that case we get the
theorem

exists a. (Show a, a -> Int)
 <=>
forall r. (forall a. Show a => (a -> Int) -> r) -> r

as witnessed by the following code (using the ExistentialQuantification and
RankNTypes extensions)

data P = forall a. Show a => MkP (a -> Int)
type CPS_P r = (forall a. Show a => (a -> Int) -> r) -> r

isoR :: P -> forall r. CPS_P r
isoR (MkP f) k =
   -- pattern match on MkP brings a fresh type T into scope,
   -- along with f :: T -> Int, and the constraint Show T.
   -- k :: forall a. Show a => (a -> Int) -> r
   -- so, k {T} f :: r


isoL :: (forall r. CPS_P r) -> P
isoL k = k (\x -> MkP x)
-- k :: forall r. (forall a. Show a => (a -> Int) -> r) -> r
-- k {P} = (forall a. Show a => (a -> Int) -> P) -> P
-- MkP :: forall a. Show a => (a -> Int) -> P
-- therefore, k {P} MkP :: P

Aside: the type 'exists a. (Show a, a -> Int)' is a bit odd, and is another
reason we don't have first class existentials in Haskell.  The 'forall'
side is using currying (a -> b -> r) <=> ((a,b) -> r) which works because
the constraint => can be modeled by dictionary passing.  But we don't have
a simple way to represent the dictionary (Show a) as a member of a tuple.

One answer is to pack it up in another "existential"; I find this a bit of
a misnomer since there's nothing existential about this data type aside
from the dictionary:

data ShowDict a = Show a => MkShowDict

Then the theorem translation is a bit more straightforward:

data P = forall a. MkP (ShowDict a, a -> Int)
type CPS_P r = (forall a. (ShowDict a, a -> Int) -> r) -> r

-- theorem: P <=> forall r. CPS_P r

isoL :: P -> forall r. CPS_P r
isoL (MkP x) k = k x

isoR :: (forall r. CPS_P r) -> P
isoR k = k (\x -> MkP x)

  -- ryan

On Sat, Aug 18, 2012 at 8:24 PM, wren ng thornton  wrote:

> On 8/17/12 12:54 AM, Alexander Solla wrote:
>
>> On Thu, Aug 16, 2012 at 8:07 PM, wren ng thornton 
>> wrote:
>>
>>> Though bear in mind we're discussing second-order quantification here,
>>> not
>>> first-order.
>>>
>>
>> Can you expand on what you mean here?  I don't see two kinds of
>> quantification in the type language (at least, reflexively, in the context
>> of what we're discussing).  In particular, I don't see how to quantify
>> over
>> predicates for (or sets of, via the extensions of the predicates) types.
>>
>> Is Haskell's 'forall' doing double duty?
>>
>
> Nope, it's the "forall" of mathematics doing double duty :)
>
> Whenever doing quantification, there's always some domain being quantified
> over, though all too often that domain is left implicit; whence lots of
> confusion over the years. And, of course, there's the scope of the
> quantification, and the entire expression. For example, consider the
> expression:
>
> forall a. P(a)
>
> The three important collections to bear in mind are:
> (1) the collection of things a ranges over
> (2) the collection of things P(a) belongs to
> (3) the collection of things forall a. P(a) belongs to
>
> So if we think of P as a function from (1) to (2), and name the space of
> such functions (1->2), then we can think of the quantifier as a function
> from (1->2) to (3).
>
>
> When you talk to logicians about quantifiers, the first thing they think
> of is so-called "first-order" quantification. That is, given the above
> expression, they think that the thing being quantified over is a collection
> of "individuals" who live outside of logic itself[1]. For example, we could
> be quantifying over the natural numbers, or over the kinds of animals in
> the world, or any other extra-logical group of entities.
>
> In Haskell, when we see the above expression we think that the thing being
> quantified over is some collection of types[2]. But, that means when we
> think of P as a function it's taking types and returning types! So the
> thing you're quantifying over and the thing you're constructing are from
> the same domain[3]! This gets logicians flustered and so they call it
> "second-order" (or more generally, "higher-order") quantification. If you
> assert the primacy of first-order logic, it makes sense right? In the
> first-order case we're quantifying over individuals; in the second-order
> case we're quantifying over collections of individuals; so third-order
> would be quantifying over collections of collections of individuals; and on
> up to higher orders.
>
>
> Personally, I find the names "first-order" and "second-order" rather
> dubious--- though the distinction is a critical one to make. Part of the
> reason for its dubiousness can be seen when you look at PTSes which make
> explicit that (1), (2), and (3) above can each be the same or different in
> all combinations. First-order quantification is the sort

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[wren ng thornton]

On 8/17/12 12:54 AM, Alexander Solla wrote:

On Thu, Aug 16, 2012 at 8:07 PM, wren ng thornton  wrote:

Though bear in mind we're discussing second-order quantification here, not
first-order.


Can you expand on what you mean here?  I don't see two kinds of
quantification in the type language (at least, reflexively, in the context
of what we're discussing).  In particular, I don't see how to quantify over
predicates for (or sets of, via the extensions of the predicates) types.

Is Haskell's 'forall' doing double duty?


Nope, it's the "forall" of mathematics doing double duty :)

Whenever doing quantification, there's always some domain being 
quantified over, though all too often that domain is left implicit; 
whence lots of confusion over the years. And, of course, there's the 
scope of the quantification, and the entire expression. For example, 
consider the expression:


forall a. P(a)

The three important collections to bear in mind are:
(1) the collection of things a ranges over
(2) the collection of things P(a) belongs to
(3) the collection of things forall a. P(a) belongs to

So if we think of P as a function from (1) to (2), and name the space of 
such functions (1->2), then we can think of the quantifier as a function 
from (1->2) to (3).



When you talk to logicians about quantifiers, the first thing they think 
of is so-called "first-order" quantification. That is, given the above 
expression, they think that the thing being quantified over is a 
collection of "individuals" who live outside of logic itself[1]. For 
example, we could be quantifying over the natural numbers, or over the 
kinds of animals in the world, or any other extra-logical group of entities.


In Haskell, when we see the above expression we think that the thing 
being quantified over is some collection of types[2]. But, that means 
when we think of P as a function it's taking types and returning types! 
So the thing you're quantifying over and the thing you're constructing 
are from the same domain[3]! This gets logicians flustered and so they 
call it "second-order" (or more generally, "higher-order") 
quantification. If you assert the primacy of first-order logic, it makes 
sense right? In the first-order case we're quantifying over individuals; 
in the second-order case we're quantifying over collections of 
individuals; so third-order would be quantifying over collections of 
collections of individuals; and on up to higher orders.



Personally, I find the names "first-order" and "second-order" rather 
dubious--- though the distinction is a critical one to make. Part of the 
reason for its dubiousness can be seen when you look at PTSes which make 
explicit that (1), (2), and (3) above can each be the same or different 
in all combinations. First-order quantification is the sort of thing you 
get from Pi/Sigma types in dependently typed languages like LF; 
second-order quantification is the sort of thing you get from the 
forall/exists quantifiers in polymorphic languages like System F. But 
the Barendregt cube makes it clear that these are *orthogonal* features. 
Neither one of them comes "first" or "second"; they just do very 
different things. Logicians thought first of first-order quantification, 
so they consider that primitive and worry about the complications of 
dealing with second-/higher-order quantification. Until recently type 
theory was focused on polymorphism of various sorts, so that's 
considered primitive or at least easier, whereas dependent types are 
exotic and worrisome/hard.



[1] This is also the root of the distinction between "functions", 
"predicates", and "logical connectives" in traditional logic. Functions 
map individuals to individuals; predicates map individuals to 
propositions/truth-values; and connectives map propositions/TVs to 
propositions/TVs. Though, traditionally, the set of connectives is taken 
to be small and fixed whereas functions and predicates are left to be 
defined by a "signature".


[2] Namely monotypes. If we allowed quantified variables to be 
instantiated with polymorphic types, then we'd get "impredicative" 
quantification. Impredicativity can be both good and bad, depending on 
what you're up to.


[3] Well, they're only the same domain for impredicative quantification. 
Otherwise the collection of types you're constructing is "bigger" than 
the collection you're quantifying over.


--
Live well,
~wren

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Alexander Solla]

On Thu, Aug 16, 2012 at 8:07 PM, wren ng thornton  wrote:

> On 8/15/12 2:55 PM, Albert Y. C. Lai wrote:
>
>> On 12-08-15 03:20 AM, wren ng thornton wrote:
>>
>>> (forall a. P(a)) -> Q <=> exists a. (P(a) -> Q)
>>>
>>
>> For example:
>>
>> A. (forall p. p drinks) -> (everyone drinks)
>> B. exists p. ((p drinks) -> (everyone drinks))
>>
>> In a recent poll, 100% of respondents think A true, 90% of them think B
>> paradoxical, and 40% of them have not heard of the Smullyan drinking
>> paradox.
>>
>
> :)
>
> Though bear in mind we're discussing second-order quantification here, not
> first-order.


Can you expand on what you mean here?  I don't see two kinds of
quantification in the type language (at least, reflexively, in the context
of what we're discussing).  In particular, I don't see how to quantify over
predicates for (or sets of, via the extensions of the predicates) types.

Is Haskell's 'forall' doing double duty?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[wren ng thornton]

On 8/15/12 2:55 PM, Albert Y. C. Lai wrote:

On 12-08-15 03:20 AM, wren ng thornton wrote:

(forall a. P(a)) -> Q <=> exists a. (P(a) -> Q)


For example:

A. (forall p. p drinks) -> (everyone drinks)
B. exists p. ((p drinks) -> (everyone drinks))

In a recent poll, 100% of respondents think A true, 90% of them think B
paradoxical, and 40% of them have not heard of the Smullyan drinking
paradox.


:)

Though bear in mind we're discussing second-order quantification here, 
not first-order.


--
Live well,
~wren

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[wren ng thornton]

On 8/15/12 12:32 PM, David Feuer wrote:

On Aug 15, 2012 3:21 AM, "wren ng thornton"  wrote:

It's even easier than that.

 (forall a. P(a)) -> Q <=> exists a. (P(a) -> Q)

Where P and Q are metatheoretic/schematic variables. This is just the
usual thing about antecedents being in a "negative" position, and thus
flipping as you move into/out of that position.


Most of this conversation is going over my head. I can certainly see how
exists a. (P(a)->Q) implies that (forall a. P(a))->Q. The opposite
certainly doesn't hold in classical logic. What sort of logic are you folks
working in?


Ryan gave a nice classical proof. Though note that, in a constructive 
setting you're right to be dubious. The validity of the questioned 
article is related to the "generalized Markov's principle" which Russian 
constructivists accept but which is not derivable from Heyting's 
axiomatization of intuitionistic logic:


GMP : ~(forall x. P(x)) -> (exists x. ~P(x))

There's been a fair amount of work on showing that GMP is constructively 
valid; though the fact that it does not derive from Heyting's 
axiomatization makes some squeamish. For these reasons it may be 
preferable to stick with the double-negation form upthread for 
converting between quantifiers. I just mentioned the above as a 
simplification of the double-negation form, which may be more familiar 
to those indoctrinated in classical logic.


--
Live well,
~wren

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[David Feuer]

I understand this now, though I still don't understand the context. Thanks!
I managed to mix up implication with causation, to my great embarrassment.
On Aug 15, 2012 3:39 PM, "Ryan Ingram"  wrote:

> In classical logic  A -> B is the equivalent to ~A v B
> (with ~ = not and v = or)
>
> So
>
> (forall a. P(a)) -> Q
> {implication = not-or}
> ~(forall a. P(a)) v Q
> {forall a. X is equivalent to there does not exist a such that X doesn't
> hold}
> ~(~exists a. ~P(a)) v Q
> {double negation elimination}
> (exists a. ~P(a)) v Q
> {a is not free in Q}
> exists a. (~P(a) v Q)
> {implication = not-or}
> exists a. (P(a) -> Q)
>
> These steps are all equivalencies, valid in both directions.
>
> On Wed, Aug 15, 2012 at 9:32 AM, David Feuer wrote:
>
>> On Aug 15, 2012 3:21 AM, "wren ng thornton"  wrote:
>> > It's even easier than that.
>> >
>> > (forall a. P(a)) -> Q  <=>  exists a. (P(a) -> Q)
>> >
>> > Where P and Q are metatheoretic/schematic variables. This is just the
>> usual thing about antecedents being in a "negative" position, and thus
>> flipping as you move into/out of that position.
>>
>> Most of this conversation is going over my head. I can certainly see how
>> exists a. (P(a)->Q) implies that (forall a. P(a))->Q. The opposite
>> certainly doesn't hold in classical logic. What sort of logic are you folks
>> working in?
>>
>> ___
>> Haskell-Cafe mailing list
>> Haskell-Cafe@haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Ryan Ingram]

In classical logic  A -> B is the equivalent to ~A v B
(with ~ = not and v = or)

So

(forall a. P(a)) -> Q
{implication = not-or}
~(forall a. P(a)) v Q
{forall a. X is equivalent to there does not exist a such that X doesn't
hold}
~(~exists a. ~P(a)) v Q
{double negation elimination}
(exists a. ~P(a)) v Q
{a is not free in Q}
exists a. (~P(a) v Q)
{implication = not-or}
exists a. (P(a) -> Q)

These steps are all equivalencies, valid in both directions.

On Wed, Aug 15, 2012 at 9:32 AM, David Feuer  wrote:

> On Aug 15, 2012 3:21 AM, "wren ng thornton"  wrote:
> > It's even easier than that.
> >
> > (forall a. P(a)) -> Q  <=>  exists a. (P(a) -> Q)
> >
> > Where P and Q are metatheoretic/schematic variables. This is just the
> usual thing about antecedents being in a "negative" position, and thus
> flipping as you move into/out of that position.
>
> Most of this conversation is going over my head. I can certainly see how
> exists a. (P(a)->Q) implies that (forall a. P(a))->Q. The opposite
> certainly doesn't hold in classical logic. What sort of logic are you folks
> working in?
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Albert Y. C. Lai]

On 12-08-15 03:20 AM, wren ng thornton wrote:

 (forall a. P(a)) -> Q  <=>  exists a. (P(a) -> Q)


For example:

A. (forall p. p drinks) -> (everyone drinks)
B. exists p. ((p drinks) -> (everyone drinks))

In a recent poll, 100% of respondents think A true, 90% of them think B 
paradoxical, and 40% of them have not heard of the Smullyan drinking 
paradox.


Hehe!

http://www.vex.net/~trebla/weblog/any-all-some.html

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[David Feuer]

On Aug 15, 2012 3:21 AM, "wren ng thornton"  wrote:
> It's even easier than that.
>
> (forall a. P(a)) -> Q  <=>  exists a. (P(a) -> Q)
>
> Where P and Q are metatheoretic/schematic variables. This is just the
usual thing about antecedents being in a "negative" position, and thus
flipping as you move into/out of that position.

Most of this conversation is going over my head. I can certainly see how
exists a. (P(a)->Q) implies that (forall a. P(a))->Q. The opposite
certainly doesn't hold in classical logic. What sort of logic are you folks
working in?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[wren ng thornton]

On 8/13/12 9:25 PM, Jay Sulzberger wrote:

I did suspect that, in some sense, "constraints" in combination
with "forall" could give the quantifier "exists".


It's even easier than that.

(forall a. P(a)) -> Q  <=>  exists a. (P(a) -> Q)

Where P and Q are metatheoretic/schematic variables. This is just the 
usual thing about antecedents being in a "negative" position, and thus 
flipping as you move into/out of that position.


The duality mentioned previously is just for the case where you don't 
have that handy "-> Q" there. How do we get the universal quantifier 
into a negative position when there's no implication? Why, we add an 
implication, of course. Even better, add two.


--
Live well,
~wren

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Ryan Ingram]

On Mon, Aug 13, 2012 at 6:53 PM, Alexander Solla wrote:

> In a classical logic, the duality is expressed by !E! = A, and !A! = E,
> where E and A are backwards/upsidedown and ! represents negation.  In
> particular, for a proposition P,
>
> Ex Px <=> !Ax! Px (not all x's are not P)
> and
> Ax Px <=> !Ex! Px (there does not exist an x which is not P)
>
> Negation is relatively tricky to represent in a constructive logic --
> hence the use of functions/implications and bottoms/contradictions.  The
> type ConcreteType -> b represents the negation of ConcreteType, because it
> shows that ConcreteType "implies the contradiction".
>
> Put these ideas together, and you will recover the duality as expressed
> earlier.
>

I'd been looking for a good explanation of how to get from Ex Px to !Ax! Px
in constructive logic, and this is basically it.  What is said here is
actually a slightly different statement, which is what had me confused!

If you do the naive encoding, you get something like

-- This is my favorite representation of "Contradiction" in Haskell, since
-- it has reductio ad absurdum encoded directly in the type
-- and only requires Rank2Types.
newtype Contradiction = Bottom { absurd :: forall a. a }
-- absurd :: forall a. Contradiction -> a

type Not a = a -> Contradiction
newtype NotC (c :: * -> Constraint) = MkNotC { unNotC :: forall a. c a =>
Not a }
type UselessExists (c :: * -> Constraint) = Not (NotC c)
-- here I'm using ConstraintKinds as, in a sense, the 'most generic' way of
specifying a type-level predicate,
-- at least in bleeding edge Haskell.  It's trivial to make a less generic
version for any particular constraint
-- you care about without going quite so overboard on type system
extensions :)
-- i.e.
-- newtype NoShow = MkNoShow {  unNoShow :: forall a. Show a => Not a }
-- type UselessExistsShow = Not NoShow

-- A simple example: there is a type that is equal to Bool:
silly :: UselessExists ((~) Bool)
silly (MkNotC k) = k True

-- need silly :: NotC ((~) Bool) -> Contradiction
-- after pattern matching on MkNotC
-- k :: forall a. (a ~ Bool) => a -> Contradiction
-- i.e. k :: Bool -> Contradiction
-- therefore, k True :: Contradiction.

This type is useless, however; NotC c isn't usefully inhabited at any
reasonable c -- there's no way to actually call it!

The magic comes when you unify the 'return type' from the two Nots
instead of using bottoms as a catch-all... I guess this is the CPS
translation of negation?

type NotR r a = a -> r
newtype NotRC r (c :: * -> Constraint) = MkNotRC { unNotRC :: forall a. c a
=> NotR r a }
-- MkNotRC :: forall r c. (forall a. c a => a -> r) -> NotRC r

type ExistsR r (c :: * -> Constraint) = NotR r (NotRC r c)
-- ~= c a => (a -> r) -> r

newtype Exists (c :: * -> Constraint) = MkExists { unExists :: forall r.
ExistsR r c }
-- MkExists :: forall c. (forall r. NotR r (NotRC r c)) -> Exists c
-- ~= forall c. (forall r. c a => (a -> r) -> r) -> Exists c

-- A simple example: there is a type that is equal to Bool:
silly2 :: Exists ((~) Bool)
silly2 = MkExists (\(MkNotRC k) -> k False)

This version allows you to specify the type of 'absurd' result you
want, and use that to let the witness of existence escape out via whatever
interface the provided constraint gives.

caseExists :: (forall a. c a => a -> r)  -> Exists c -> r
caseExists k (MkExists f) = f (MkNotRC k)

main = putStrLn $ caseExists show silly2
-- should print "False"
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the

[oleg]

> It's only a test case. The real thing is for a game and will be
> something like:

> class EntityT e where
>update  :: e -> e
>render  :: e -> IO ()
>handleEvent :: e -> Event -> e
>getBound:: e -> Maybe Bound

> data Entity = forall e. (EntityT e) => Entity e

> data Level = Level {
>entities = [Entity],
>...
>}

I suspected the real case would look like that. It is also covered on
the same web page on Eliminating existentials. Here is your example
without existentials, in pure Haskell98 (I took a liberty to fill in
missing parts to make the example running)


data Event = Event Int  -- Stubs
type Bound = Pos
type Pos  = (Float,Float)

data EntityO = EntityO{
  update  :: EntityO,
  render  :: IO (),
  handleEvent :: Event -> EntityO,
  getBound:: Maybe Bound
  }

type Name = String

new_entity :: Name -> Pos -> EntityO
new_entity name pos@(posx,posy) =
  EntityO{update = update,
  render = render,
  handleEvent = handleEvent,
  getBound = getBound}
 where
 update = new_entity name (posx+1,posy+1)
 render = putStrLn $ name ++ " at " ++ show pos
 handleEvent (Event x) = new_entity name (posx + fromIntegral x,posy)
 getBound = if abs posx + abs posy < 1.0 then Just pos else Nothing


data Level = Level {
entities :: [EntityO]
}

levels = Level {
  entities = [new_entity "e1" (0,0),
  new_entity "e2" (1,1)]
  }


evolve :: Level -> Level
evolve l = l{entities = map update (entities l)}

renderl :: Level -> IO ()
renderl l = mapM_ render (entities l)

main = renderl . evolve $ levels


I think the overall pattern should look quite familiar. The
code shows off the encoding of objects as records of closures. See
http://okmij.org/ftp/Scheme/oop-in-fp.txt
for the references and modern reconstruction of Ken Dickey's
``Scheming with Objects''.

It is this encoding that gave birth to Scheme -- after Steele and
Sussman realized that closures emulate actors (reactive
objects). Incidentally, existentials do enter the picture: the
emerge upon closure conversion:

  Yasuhiko Minamide, J. Gregory Morrisett and Robert Harper
  Typed Closure Conversion. POPL1996
  http://www.cs.cmu.edu/~rwh/papers/closures/popl96.ps

This message demonstrates the inverse of the closure conversion,
eliminating existentials and introducing closures.



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Jay Sulzberger]

On Mon, 13 Aug 2012, Alexander Solla  wrote:


On Mon, Aug 13, 2012 at 6:25 PM, Jay Sulzberger  wrote:




On Mon, 13 Aug 2012, Ryan Ingram  wrote:

 On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger  wrote:


 Does Haskell have a word for "existential type" declaration?  I

have the impression, and this must be wrong, that "forall" does
double duty, that is, it declares a "for all" in some sense like
the usual "for all" of the Lower Predicate Calculus, perhaps the
"for all" of system F, or something near it.



It's using the forall/exists duality:
   exsts a. P(a)  <=>  forall r. (forall a. P(a) -> r) -> r



;)

This is, I think, a good joke.  It has taken me a while, but I
now understand that one of the most attractive things about
Haskell is its sense of humor, which is unfailing.

I will try to think about this, after trying your examples.

I did suspect that, in some sense, "constraints" in combination
with "forall" could give the quantifier "exists".



In a classical logic, the duality is expressed by !E! = A, and !A! = E,
where E and A are backwards/upsidedown and ! represents negation.  In
particular, for a proposition P,

Ex Px <=> !Ax! Px (not all x's are not P)
and
Ax Px <=> !Ex! Px (there does not exist an x which is not P)


Yes.



Negation is relatively tricky to represent in a constructive logic -- hence
the use of functions/implications and bottoms/contradictions.  The type
ConcreteType -> b represents the negation of ConcreteType, because it shows
that ConcreteType "implies the contradiction".


I am becoming sensitized to this distinction.  I now, I think,
feel the impulse toward "constructivism", that is, the
assumption/delusion^Waspiration that all functions from the reals
to the reals are continuous.  One argument that helped me goes:

 The reals between 0 and 1 are functions from the integers to say {0, 1}.

 They are attained as limits of functions f: iota(n) -> {0, 1}, as
 n becomes larger and larger and ... , where iota(n) is a set with
 n elements, n a finite integer.

 So, our objects, the reals, are attained as limits.  And the
 process of proceeding toward the limit is "natural", "functorial"
 in the sense of category theory.

 Thus so also our morphisms, that is functions from the reals to
 the reals, must be produced functorially as limits of maps
 between objects f: iota(n) -> {0, 1}.



Put these ideas together, and you will recover the duality as expressed
earlier.


Thanks!  I am reading some blog posts and I was impressed by the
buffalo hair here:

  
http://existentialtype.wordpress.com/2012/08/11/extensionality-intensionality-and-brouwers-dictum/

oo--JS.










For example:
   (exists a. Show a => a) <=> forall r. (forall a. Show a => a -> r) -> r

This also works when you look at the type of a constructor:

   data Showable = forall a. Show a => MkShowable a
   -- MkShowable :: forall a. Show a => a -> Showable

   caseShowable :: forall r. (forall a. Show a => a -> r) -> Showable -> r
   caseShowable k (MkShowable x) = k x

   testData :: Showable
   testData = MkShowable (1 :: Int)

   useData :: Int
   useData = case testData of (MkShowable x) -> length (show x)

   useData2 :: Int
   useData2 = caseShowable (length . show) testData

Haskell doesn't currently have first class existentials; you need to wrap
them in an existential type like this.  Using 'case' to pattern match on
the constructor unwraps the existential and makes any packed-up
constraints
available to the right-hand-side of the case.

An example of existentials without using constraints directly:

   data Stream a = forall s. MkStream s (s -> Maybe (a,s))

   viewStream :: Stream a -> Maybe (a, Stream a)
   viewStream (MkStream s k) = case k s of
   Nothing -> Nothing
   Just (a, s') -> Just (a, MkStream s' k)

   takeStream :: Int -> Stream a -> [a]
   takeStream 0 _ = []
   takeStream n s = case viewStream s of
   Nothing -> []
   Just (a, s') -> a : takeStream (n-1) s'

   fibStream :: Stream Integer
   fibStream = Stream (0,1) (\(x,y) -> Just (x, (y, x+y)))

Here the 'constraint' made visible by pattern matching on MkStream (in
viewStream) is that the "s" type stored in the stream matches the "s" type
taken and returned by the 'get next element' function.  This allows the
construction of another stream with the same function but a new state --
MkStream s' k.

It also allows the stream function in fibStream to be non-recursive which
greatly aids the GHC optimizer in certain situations.

 -- ryan



__**_
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/**mailman/listinfo/haskell-cafe





___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Alexander Solla]

On Mon, Aug 13, 2012 at 6:25 PM, Jay Sulzberger  wrote:

>
>
> On Mon, 13 Aug 2012, Ryan Ingram  wrote:
>
>  On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger  wrote:
>>
>>  Does Haskell have a word for "existential type" declaration?  I
>>> have the impression, and this must be wrong, that "forall" does
>>> double duty, that is, it declares a "for all" in some sense like
>>> the usual "for all" of the Lower Predicate Calculus, perhaps the
>>> "for all" of system F, or something near it.
>>>
>>>
>> It's using the forall/exists duality:
>>exsts a. P(a)  <=>  forall r. (forall a. P(a) -> r) -> r
>>
>
> ;)
>
> This is, I think, a good joke.  It has taken me a while, but I
> now understand that one of the most attractive things about
> Haskell is its sense of humor, which is unfailing.
>
> I will try to think about this, after trying your examples.
>
> I did suspect that, in some sense, "constraints" in combination
> with "forall" could give the quantifier "exists".
>
>
In a classical logic, the duality is expressed by !E! = A, and !A! = E,
where E and A are backwards/upsidedown and ! represents negation.  In
particular, for a proposition P,

Ex Px <=> !Ax! Px (not all x's are not P)
and
Ax Px <=> !Ex! Px (there does not exist an x which is not P)

Negation is relatively tricky to represent in a constructive logic -- hence
the use of functions/implications and bottoms/contradictions.  The type
ConcreteType -> b represents the negation of ConcreteType, because it shows
that ConcreteType "implies the contradiction".

Put these ideas together, and you will recover the duality as expressed
earlier.


>
>
>
>> For example:
>>(exists a. Show a => a) <=> forall r. (forall a. Show a => a -> r) -> r
>>
>> This also works when you look at the type of a constructor:
>>
>>data Showable = forall a. Show a => MkShowable a
>>-- MkShowable :: forall a. Show a => a -> Showable
>>
>>caseShowable :: forall r. (forall a. Show a => a -> r) -> Showable -> r
>>caseShowable k (MkShowable x) = k x
>>
>>testData :: Showable
>>testData = MkShowable (1 :: Int)
>>
>>useData :: Int
>>useData = case testData of (MkShowable x) -> length (show x)
>>
>>useData2 :: Int
>>useData2 = caseShowable (length . show) testData
>>
>> Haskell doesn't currently have first class existentials; you need to wrap
>> them in an existential type like this.  Using 'case' to pattern match on
>> the constructor unwraps the existential and makes any packed-up
>> constraints
>> available to the right-hand-side of the case.
>>
>> An example of existentials without using constraints directly:
>>
>>data Stream a = forall s. MkStream s (s -> Maybe (a,s))
>>
>>viewStream :: Stream a -> Maybe (a, Stream a)
>>viewStream (MkStream s k) = case k s of
>>Nothing -> Nothing
>>Just (a, s') -> Just (a, MkStream s' k)
>>
>>takeStream :: Int -> Stream a -> [a]
>>takeStream 0 _ = []
>>takeStream n s = case viewStream s of
>>Nothing -> []
>>Just (a, s') -> a : takeStream (n-1) s'
>>
>>fibStream :: Stream Integer
>>fibStream = Stream (0,1) (\(x,y) -> Just (x, (y, x+y)))
>>
>> Here the 'constraint' made visible by pattern matching on MkStream (in
>> viewStream) is that the "s" type stored in the stream matches the "s" type
>> taken and returned by the 'get next element' function.  This allows the
>> construction of another stream with the same function but a new state --
>> MkStream s' k.
>>
>> It also allows the stream function in fibStream to be non-recursive which
>> greatly aids the GHC optimizer in certain situations.
>>
>>  -- ryan
>>
>>
> __**_
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/**mailman/listinfo/haskell-cafe
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Jay Sulzberger]

On Mon, 13 Aug 2012, Ryan Ingram  wrote:


On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger  wrote:


Does Haskell have a word for "existential type" declaration?  I
have the impression, and this must be wrong, that "forall" does
double duty, that is, it declares a "for all" in some sense like
the usual "for all" of the Lower Predicate Calculus, perhaps the
"for all" of system F, or something near it.



It's using the forall/exists duality:
   exsts a. P(a)  <=>  forall r. (forall a. P(a) -> r) -> r


;)

This is, I think, a good joke.  It has taken me a while, but I
now understand that one of the most attractive things about
Haskell is its sense of humor, which is unfailing.

I will try to think about this, after trying your examples.

I did suspect that, in some sense, "constraints" in combination
with "forall" could give the quantifier "exists".

Thanks, ryan!

oo--JS.




For example:
   (exists a. Show a => a) <=> forall r. (forall a. Show a => a -> r) -> r

This also works when you look at the type of a constructor:

   data Showable = forall a. Show a => MkShowable a
   -- MkShowable :: forall a. Show a => a -> Showable

   caseShowable :: forall r. (forall a. Show a => a -> r) -> Showable -> r
   caseShowable k (MkShowable x) = k x

   testData :: Showable
   testData = MkShowable (1 :: Int)

   useData :: Int
   useData = case testData of (MkShowable x) -> length (show x)

   useData2 :: Int
   useData2 = caseShowable (length . show) testData

Haskell doesn't currently have first class existentials; you need to wrap
them in an existential type like this.  Using 'case' to pattern match on
the constructor unwraps the existential and makes any packed-up constraints
available to the right-hand-side of the case.

An example of existentials without using constraints directly:

   data Stream a = forall s. MkStream s (s -> Maybe (a,s))

   viewStream :: Stream a -> Maybe (a, Stream a)
   viewStream (MkStream s k) = case k s of
   Nothing -> Nothing
   Just (a, s') -> Just (a, MkStream s' k)

   takeStream :: Int -> Stream a -> [a]
   takeStream 0 _ = []
   takeStream n s = case viewStream s of
   Nothing -> []
   Just (a, s') -> a : takeStream (n-1) s'

   fibStream :: Stream Integer
   fibStream = Stream (0,1) (\(x,y) -> Just (x, (y, x+y)))

Here the 'constraint' made visible by pattern matching on MkStream (in
viewStream) is that the "s" type stored in the stream matches the "s" type
taken and returned by the 'get next element' function.  This allows the
construction of another stream with the same function but a new state --
MkStream s' k.

It also allows the stream function in fibStream to be non-recursive which
greatly aids the GHC optimizer in certain situations.

 -- ryan



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Ryan Ingram]

On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger  wrote:

> Does Haskell have a word for "existential type" declaration?  I
> have the impression, and this must be wrong, that "forall" does
> double duty, that is, it declares a "for all" in some sense like
> the usual "for all" of the Lower Predicate Calculus, perhaps the
> "for all" of system F, or something near it.
>

It's using the forall/exists duality:
exsts a. P(a)  <=>  forall r. (forall a. P(a) -> r) -> r

For example:
(exists a. Show a => a) <=> forall r. (forall a. Show a => a -> r) -> r

This also works when you look at the type of a constructor:

data Showable = forall a. Show a => MkShowable a
-- MkShowable :: forall a. Show a => a -> Showable

caseShowable :: forall r. (forall a. Show a => a -> r) -> Showable -> r
caseShowable k (MkShowable x) = k x

testData :: Showable
testData = MkShowable (1 :: Int)

useData :: Int
useData = case testData of (MkShowable x) -> length (show x)

useData2 :: Int
useData2 = caseShowable (length . show) testData

Haskell doesn't currently have first class existentials; you need to wrap
them in an existential type like this.  Using 'case' to pattern match on
the constructor unwraps the existential and makes any packed-up constraints
available to the right-hand-side of the case.

An example of existentials without using constraints directly:

data Stream a = forall s. MkStream s (s -> Maybe (a,s))

viewStream :: Stream a -> Maybe (a, Stream a)
viewStream (MkStream s k) = case k s of
Nothing -> Nothing
Just (a, s') -> Just (a, MkStream s' k)

takeStream :: Int -> Stream a -> [a]
takeStream 0 _ = []
takeStream n s = case viewStream s of
Nothing -> []
Just (a, s') -> a : takeStream (n-1) s'

fibStream :: Stream Integer
fibStream = Stream (0,1) (\(x,y) -> Just (x, (y, x+y)))

Here the 'constraint' made visible by pattern matching on MkStream (in
viewStream) is that the "s" type stored in the stream matches the "s" type
taken and returned by the 'get next element' function.  This allows the
construction of another stream with the same function but a new state --
MkStream s' k.

It also allows the stream function in fibStream to be non-recursive which
greatly aids the GHC optimizer in certain situations.

  -- ryan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Jay Sulzberger]

On Mon, 13 Aug 2012, Johan Holmquist  wrote:


That pattern looks so familiar. :) Existential types seem to fit in to the
type system really well so I never got why it is not part of the standard.
On Aug 12, 2012 10:36 AM, "Daniel Trstenjak" 
wrote:


Does Haskell have a word for "existential type" declaration?  I
have the impression, and this must be wrong, that "forall" does
double duty, that is, it declares a "for all" in some sense like
the usual "for all" of the Lower Predicate Calculus, perhaps the
"for all" of system F, or something near it.

oo--JS.






Hi Oleg,

On Sat, Aug 11, 2012 at 08:14:47AM -, o...@okmij.org wrote:

I'd like to point out that the only operation we can do on the first
argument of MkFoo is to show to it. This is all we can ever do:
we have no idea of its type but we know we can show it and get a
String. Why not to apply show to start with (it won't be evaluated
until required anyway)?


It's only a test case. The real thing is for a game and will be
something like:

class EntityT e where
   update  :: e -> e

   render  :: e -> IO ()

   handleEvent :: e -> Event -> e

   getBound:: e -> Maybe Bound


data Entity = forall e. (EntityT e) => Entity e

data Level = Level {
   entities = [Entity],
   ...
   }


Greetings,
Daniel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe





___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Johan Holmquist]

That pattern looks so familiar. :) Existential types seem to fit in to the
type system really well so I never got why it is not part of the standard.
On Aug 12, 2012 10:36 AM, "Daniel Trstenjak" 
wrote:

>
> Hi Oleg,
>
> On Sat, Aug 11, 2012 at 08:14:47AM -, o...@okmij.org wrote:
> > I'd like to point out that the only operation we can do on the first
> > argument of MkFoo is to show to it. This is all we can ever do:
> > we have no idea of its type but we know we can show it and get a
> > String. Why not to apply show to start with (it won't be evaluated
> > until required anyway)?
>
> It's only a test case. The real thing is for a game and will be
> something like:
>
> class EntityT e where
>update  :: e -> e
>
>render  :: e -> IO ()
>
>handleEvent :: e -> Event -> e
>
>getBound:: e -> Maybe Bound
>
>
> data Entity = forall e. (EntityT e) => Entity e
>
> data Level = Level {
>entities = [Entity],
>...
>}
>
>
> Greetings,
> Daniel
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Daniel Trstenjak]

Hi Oleg,

On Sat, Aug 11, 2012 at 08:14:47AM -, o...@okmij.org wrote:
> I'd like to point out that the only operation we can do on the first
> argument of MkFoo is to show to it. This is all we can ever do:
> we have no idea of its type but we know we can show it and get a
> String. Why not to apply show to start with (it won't be evaluated
> until required anyway)?

It's only a test case. The real thing is for a game and will be
something like:

class EntityT e where
   update  :: e -> e

   render  :: e -> IO ()

   handleEvent :: e -> Event -> e

   getBound:: e -> Maybe Bound


data Entity = forall e. (EntityT e) => Entity e

data Level = Level {
   entities = [Entity],
   ...
   }


Greetings,
Daniel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Heinrich Apfelmus]

Antoine Latter wrote:

It should be pretty easy to write an adapter function of type "String ->
(Show a => a)".


The type needs to be

   String -> (exists a. Show a => a)

which is equivalent to

   String -> (forall a. Show a => a -> c) -> c


Here is the implementation of the adapter

   newtype ExistsShow = E { showE :: String }
   instance Show ExistsShow where
   show = showE

   withShow :: String -> (forall a. Show a => a -> c) -> c
   withShow s f = f (E s)

Essentially, the point is that the types are equivalent

   ExistsShow  ==  exists a. Show a => a


Best regards,
Heinrich Apfelmus

--
http://apfelmus.nfshost.com


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Alexander Solla]

On Sat, Aug 11, 2012 at 12:01 PM, Antoine Latter  wrote:

> It should be pretty easy to write an adapter function of type "String ->
> (Show a => a)".
>

Not with that type.  Give it a try.

Hint:  what is the extension of the type variable 'a'?  What do you know
about it?  How would you use that to write the function?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Antoine Latter]

It should be pretty easy to write an adapter function of type "String ->
(Show a => a)".
On Aug 11, 2012 12:34 PM, "Patrick Palka"  wrote:

> On Sat, Aug 11, 2012 at 4:14 AM,  wrote:
>
>>
>> I'd like to point out that the only operation we can do on the first
>> argument of MkFoo is to show to it. This is all we can ever do:
>> we have no idea of its type but we know we can show it and get a
>> String.
>>
>
> That's not all you can do: you can also pass the first argument of MkFoo
> to a function that expects a Show a => a argument, like the function
> 'print'. Can you do that with just a String (that represents show x for
> some x)?
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Patrick Palka]

On Sat, Aug 11, 2012 at 4:14 AM,  wrote:

>
> I'd like to point out that the only operation we can do on the first
> argument of MkFoo is to show to it. This is all we can ever do:
> we have no idea of its type but we know we can show it and get a
> String.
>

That's not all you can do: you can also pass the first argument of MkFoo to
a function that expects a Show a => a argument, like the function 'print'.
Can you do that with just a String (that represents show x for some x)?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[David Feuer]

Has anyone used existential types to represent items on a schedule in a
scheduled lazy data structure?
On Aug 11, 2012 4:15 AM,  wrote:

>
> > data A = A deriving Show
> > data B = B deriving Show
> > data C = C deriving Show
> >
> > data Foo = forall a. Show a => MkFoo a (Int -> Bool)
> >
> > instance Show Foo where
> >show (MkFoo a f) = show a
>
> I'd like to point out that the only operation we can do on the first
> argument of MkFoo is to show to it. This is all we can ever do:
> we have no idea of its type but we know we can show it and get a
> String. Why not to apply show to start with (it won't be evaluated
> until required anyway)? Therefore, the data type Foo above is in all
> respects equivalent to
>
> > data Foo = MkFoo String (Int -> Bool)
>
> and no existentials are ever needed. The following article explains
> elimination of existentials in more detail, touching upon the original
> problem, of bringing different types into union.
>
> http://okmij.org/ftp/Computation/Existentials.html
>
>
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Data structure containing elements which are instances of the same type class

[oleg]

> data A = A deriving Show
> data B = B deriving Show
> data C = C deriving Show
>
> data Foo = forall a. Show a => MkFoo a (Int -> Bool)
>
> instance Show Foo where
>show (MkFoo a f) = show a

I'd like to point out that the only operation we can do on the first
argument of MkFoo is to show to it. This is all we can ever do:
we have no idea of its type but we know we can show it and get a
String. Why not to apply show to start with (it won't be evaluated
until required anyway)? Therefore, the data type Foo above is in all
respects equivalent to

> data Foo = MkFoo String (Int -> Bool)

and no existentials are ever needed. The following article explains
elimination of existentials in more detail, touching upon the original
problem, of bringing different types into union.

http://okmij.org/ftp/Computation/Existentials.html



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Alexander Solla]

On Tue, Aug 7, 2012 at 11:03 AM, Daniel Trstenjak <
daniel.trsten...@gmail.com> wrote:

>
> Hi all,
>
> it should be possible a call a function on all elements of the data
> structure, to add and remove elements.
>
> What I currently have:
>
> the type class:
>
> class Foo a where
>hasId :: a -> Int -> Maybe a
>
>
> a few instances:
>
> data A = A deriving Show
> instance Foo A where
>hasId a 1 = Just a
>hasId _ _ = Nothing
>
> data B = B deriving Show
> instance Foo B where
>hasId a 2 = Just a
>hasId _ _ = Nothing
>
> data C = C deriving Show
> instance Foo C where
>hasId a 3 = Just a
>hasId _ _ = Nothing
>
>
> the data structure holding any instance of Foo, which itself is a
> instance of Foo:
>
> data Foos l r = Foos l r
>   | FooL l
>   | FooR r
>   | NoFoos deriving Show
>
> instance (Foo l, Foo r) => Foo (Foos l r) where
>hasId (Foos l r) id =
>   case (hasId l id, hasId r id) of
>(Just l, Just r) -> Just $ Foos l r
>(Just l, _ ) -> Just $ FooL l
>(_ , Just r) -> Just $ FooR r
>_-> Nothing
>
>
> combinator for Foos:
>
> (+++) :: l -> r -> Foos l r
> l +++ r = Foos l r
> infixr 5 +++
>
>
> Now I can write:
>
> *Main> A +++ B +++ C +++ A
> Foos A (Foos B (Foos C A))
> *Main> (A +++ B +++ C +++ A) `hasId` 1
> Just (Foos A (FooR (FooR A)))
>
>
> Doesn't seem that nice. For every operation I would have to extend the
> type class. After some operations the data structure contains many
> dummy nodes (FooR, FooL).
>
> Is there some nicer way?
>

Read "Data types a la carte".  You can use the "free" package for most of
the plumbing (I think -- it definitely does free monads, which are a
tangentially related idea, but it has a module for dealing with these funny
functors, if I recall correctly.)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Daniel Trstenjak]

Hi Joey,

On Tue, Aug 07, 2012 at 02:13:09PM -0400, Joey Adams wrote:
> Are you looking for existential quantification [1]?
> 
> data SomeFoo = forall a. Foo a => a
> 
>  [1]: 
> http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#existential-quantification

Thanks! Yes, that looks really nice. :)

data A = A deriving Show
data B = B deriving Show
data C = C deriving Show

data Foo = forall a. Show a => MkFoo a (Int -> Bool)

instance Show Foo where
   show (MkFoo a f) = show a

hasId foos id = filter (\(MkFoo a f) -> f id) foos

*Main> let foos = [MkFoo A (==1), MkFoo B (==2), MkFoo C (==3)]
*Main> hasId foos 1
[A]


Greetings,
Daniel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

[Joey Adams]

On Tue, Aug 7, 2012 at 2:03 PM, Daniel Trstenjak
 wrote:
> Data structure containing elements which are instances of the same type class

Are you looking for existential quantification [1]?

data SomeFoo = forall a. Foo a => a

 [1]: 
http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#existential-quantification

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Data structure containing elements which are instances of the same type class

[Daniel Trstenjak]

Hi all,

it should be possible a call a function on all elements of the data
structure, to add and remove elements.

What I currently have:

the type class:

class Foo a where
   hasId :: a -> Int -> Maybe a


a few instances:

data A = A deriving Show
instance Foo A where
   hasId a 1 = Just a
   hasId _ _ = Nothing

data B = B deriving Show
instance Foo B where
   hasId a 2 = Just a
   hasId _ _ = Nothing

data C = C deriving Show
instance Foo C where
   hasId a 3 = Just a
   hasId _ _ = Nothing


the data structure holding any instance of Foo, which itself is a
instance of Foo:

data Foos l r = Foos l r
  | FooL l
  | FooR r
  | NoFoos deriving Show

instance (Foo l, Foo r) => Foo (Foos l r) where
   hasId (Foos l r) id =
  case (hasId l id, hasId r id) of
   (Just l, Just r) -> Just $ Foos l r
   (Just l, _ ) -> Just $ FooL l
   (_ , Just r) -> Just $ FooR r
   _-> Nothing


combinator for Foos:

(+++) :: l -> r -> Foos l r
l +++ r = Foos l r
infixr 5 +++


Now I can write:

*Main> A +++ B +++ C +++ A
Foos A (Foos B (Foos C A))
*Main> (A +++ B +++ C +++ A) `hasId` 1
Just (Foos A (FooR (FooR A)))


Doesn't seem that nice. For every operation I would have to extend the
type class. After some operations the data structure contains many
dummy nodes (FooR, FooL).

Is there some nicer way?


Greetings,
Daniel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe