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
On 8/17/12 12:54 AM, Alexander Solla wrote:
On Thu, Aug 16, 2012 at 8:07 PM, wren ng thornton w...@freegeek.org 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
On 8/15/12 12:32 PM, David Feuer wrote:
On Aug 15, 2012 3:21 AM, wren ng thorntonw...@freegeek.org 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
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,
On Thu, Aug 16, 2012 at 8:07 PM, wren ng thornton w...@freegeek.org 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
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
On Aug 15, 2012 3:21 AM, wren ng thornton w...@freegeek.org 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
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
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}
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 ryani.s...@gmail.com wrote:
In classical logic A - B is the equivalent to ~A v B
(with ~ = not and v = or)
On Mon, Aug 13, 2012 at 6:53 PM, Alexander Solla alex.so...@gmail.comwrote:
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)
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 daniel.trsten...@gmail.com
wrote:
Hi Oleg,
On Sat, Aug 11, 2012 at 08:14:47AM -, o...@okmij.org
On Mon, 13 Aug 2012, Johan Holmquist holmi...@gmail.com 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 daniel.trsten...@gmail.com
wrote:
On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger j...@panix.com 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
On Mon, 13 Aug 2012, Ryan Ingram ryani.s...@gmail.com wrote:
On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger j...@panix.com 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
On Mon, Aug 13, 2012 at 6:25 PM, Jay Sulzberger j...@panix.com wrote:
On Mon, 13 Aug 2012, Ryan Ingram ryani.s...@gmail.com wrote:
On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger j...@panix.com wrote:
Does Haskell have a word for existential type declaration? I
have the impression,
On Mon, 13 Aug 2012, Alexander Solla alex.so...@gmail.com wrote:
On Mon, Aug 13, 2012 at 6:25 PM, Jay Sulzberger j...@panix.com wrote:
On Mon, 13 Aug 2012, Ryan Ingram ryani.s...@gmail.com wrote:
On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger j...@panix.com wrote:
Does Haskell have
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
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
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
Has anyone used existential types to represent items on a schedule in a
scheduled lazy data structure?
On Aug 11, 2012 4:15 AM, o...@okmij.org 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)
On Sat, Aug 11, 2012 at 4:14 AM, 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.
That's not all you can do:
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 patr...@parcs.ath.cx wrote:
On Sat, Aug 11, 2012 at 4:14 AM, o...@okmij.org wrote:
I'd like to point out that the only operation we can do on the first
argument of
On Sat, Aug 11, 2012 at 12:01 PM, Antoine Latter aslat...@gmail.com 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
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
On Tue, Aug 7, 2012 at 2:03 PM, Daniel Trstenjak
daniel.trsten...@gmail.com 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]:
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!
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
28 matches
Mail list logo
