[Haskell-cafe] forall & ST monad
Kim-Ee Yeoh
a.biurvOir4 at asuhan.com
Thu Feb 19 08:53:07 EST 2009
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 making use of a.
> That
> doesn't mean that there is only one a:T for which P is satisfied. But it
> *does* mean that for any particular proof of exists a:T. P(a), only one
> a:T is
> involved. So if you can open that proof, then you know that that is the
> particular a you're dealing with, which leads to the problems in the
> grandparent.
>
re: Constructivity and the opening of a proof
A form of the theorem that the primes are infinite goes
"Given a finite set of primes, there's a prime bigger than any of them."
The usual proof is constructive since factorization is algorithmic,
but I don't see why a priori, applications of this theorem on a given input
should always yield the same prime when more than one factor exists.
Is non-deterministic choice forbidden in constructive math? A cursory
google seems to suggest that if not, it's at least a bête noire to some.
--
View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22100873.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
More information about the Haskell-Cafe
mailing list