Heinrich Apfelmus wrote:
Now,
(forall a. T[a]) - S
is clearly true while
exists a. (T[a] - S)
should be nonsense: having one example of a marble that is either red or
blue does in no way imply that all of them are, at least constructively.
(It is true classically, but I
On Wed, 2009-02-25 at 10:18 -0800, Kim-Ee Yeoh wrote:
Heinrich Apfelmus wrote:
Now,
(forall a. T[a]) - S
is clearly true while
exists a. (T[a] - S)
should be nonsense: having one example of a marble that is either red or
blue does in no way imply that all of
On Fri, Feb 20, 2009 at 11:33 AM, Kim-Ee Yeoh a.biurvo...@asuhan.com wrote:
Here's a counterexample, regardless of whether you're using
constructive or classical logic, that (forall a. T[a]) - T' does
not imply exists a. (T[a] - T').
Let a not exist, but T' true. Done.
That isn't quite a
Wolfgang Jeltsch-2 wrote:
Am Montag, 16. Februar 2009 19:22 schrieb Wolfgang Jeltsch:
First, I thought so too but I changed my mind. To my knowledge a type
(forall a. T[a]) - T' is equivalent to the type exists a. (T[a] - T').
It’s the same as in predicate logic – Curry-Howard in action.
Jonathan Cast-2 wrote:
Summary: Existential types are not enough for ST. You need the rank 2
type, to guarantee that *each* application of runST may (potentially)
work with a different class of references. (A different state thread).
Interesting.
What's going on in the example that
On Thursday 19 February 2009 7:22:48 am Kim-Ee Yeoh wrote:
Jonathan Cast-2 wrote:
Summary: Existential types are not enough for ST. You need the rank 2
type, to guarantee that *each* application of runST may (potentially)
work with a different class of references. (A different state
There's a lot to chew on (thank you!), but I'll just take something
I can handle for now.
Dan Doel wrote:
An existential:
exists a:T. P(a)
is a pair of some a with type T and a proof that a satisfies P (which has
type
P(a)). In Haskell, T is some kind, and P(a) is some type
On Thu, 2009-02-19 at 05:53 -0800, Kim-Ee Yeoh wrote:
There's a lot to chew on (thank you!), but I'll just take something
I can handle for now.
Dan Doel wrote:
An existential:
exists a:T. P(a)
is a pair of some a with type T and a proof that a satisfies P (which has
Jonathan Cast-2 wrote:
Taking the `let open' syntax from `First-class
Modules for Haskell' [1], we can say
let open runST' = runST in
let
ref = runST' $ newSTRef 0
!() = runST' $ writeSTRef ref 1
!() = runST' $ writeSTRef ref 2
in runST' $ readSTRef ref
This
Am Sonntag, 15. Februar 2009 17:50 schrieb Peter Verswyvelen:
I'm having trouble understanding the explanation of the meaning of the
signature of runST
Were you just reading the documentation of Grapefruit’s era parameters or why
are you studying ST? ;-)
Best wishes,
Wolfgang
Aha! Wolfgang is a man who knows his own code :)
Yes, I've seen this a couple of times but when I saw it again in Grapefruit,
I wanted to know how this usage of existentials worked, since I'm sooo
curious to find out how you managed to use the type system for solving some
of the typical FRP
Am Montag, 16. Februar 2009 14:21 schrieben Sie:
Aha! Wolfgang is a man who knows his own code :)
Yes, I've seen this a couple of times but when I saw it again in
Grapefruit, I wanted to know how this usage of existentials worked, since
I'm sooo curious to find out how you managed to use the
Peter Verswyvelen-2 wrote:
I'm having trouble understanding the explanation of the meaning of the
signature of runST at
http://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types
I could try to read the article a couple of times again, but are there any
other good readings
Am Montag, 16. Februar 2009 19:04 schrieb Kim-Ee Yeoh:
Despite its rank-2 type, runST really doesn't have anything to do with
existential quantification.
First, I thought so too but I changed my mind. To my knowledge a type
(forall a. T[a]) - T' is equivalent to the type exists a. (T[a] - T').
Am Montag, 16. Februar 2009 19:22 schrieb Wolfgang Jeltsch:
Am Montag, 16. Februar 2009 19:04 schrieb Kim-Ee Yeoh:
Despite its rank-2 type, runST really doesn't have anything to do with
existential quantification.
First, I thought so too but I changed my mind. To my knowledge a type
Correct. And under the hood, GHC does implement runST in its
existential dual form using a hidden State# type.
I wonder however, if we're wandering too far away from the
OP's query about grokking runST and how the ST monad
works. I'd imagine that means he'd like to see how rank-2
polymorphism
On Mon, 2009-02-16 at 19:36 +0100, Wolfgang Jeltsch wrote:
Am Montag, 16. Februar 2009 19:22 schrieb Wolfgang Jeltsch:
Am Montag, 16. Februar 2009 19:04 schrieb Kim-Ee Yeoh:
Despite its rank-2 type, runST really doesn't have anything to do with
existential quantification.
First, I
I'm having trouble understanding the explanation of the meaning of the
signature of runST at
http://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types
I could try to read the article a couple of times again, but are there any
other good readings about these existentially quantified
On 2009 Feb 15, at 11:50, Peter Verswyvelen wrote:
I could try to read the article a couple of times again, but are
there any other good readings about these existentially quantified
types and how the ST monad works?
You could think about it as playing a dirty trick on the typechecker.
Peter Verswyvelen-2 wrote:
I could try to read the article a couple of times again, but are there any
other good readings about these existentially quantified types and how the
ST monad works?
The primary source is if I'm not mistaken, the following
State in Haskell paper:
On Sun, Feb 15, 2009 at 11:50 AM, Kim-Ee Yeoh a.biurvo...@asuhan.com wrote:
Having said that, I'm not sure about the statement on page 9
that readVar v simply does not have type forall s. ST s Bool.
The variable v could be of type forall s. MutVar s Bool,
in which case all of runST (readVar v)
Peter Verswyvelen schrieb:
I'm having trouble understanding the explanation of the meaning of the
signature of runST at
http://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types
Is this one better
http://haskell.org/haskellwiki/Monad/ST ?
2009/2/15 Brandon S. Allbery KF8NH allb...@ece.cmu.edu
On 2009 Feb 15, at 11:50, Peter Verswyvelen wrote:
I could try to read the article a couple of times again, but are there any
other good readings about these existentially quantified types and how the
ST monad works?
You could think
23 matches
Mail list logo
