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 tha
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
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
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 tru
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"
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
>
>
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}
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, a
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 yo
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. Th
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 <
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,
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"
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
t
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 Predica
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 ty
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 t
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
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
newty
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 t
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.
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 als
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)
> >
> > inst
> 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
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 -
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
Thank
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
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
28 matches
Mail list logo
