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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe