[Haskell-cafe] forall & ST monad

[Derek Elkins]

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
> > 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.

They don't.  Any particular constructive proof will yield a particular
new bigger prime, but they don't have to yield the same one.  

Let's choose a simpler example: There exists an Integer.  Any
(constructive) proof of that proposition is just an Integer and thus
certainly a particular Integer.  However, there is nothing special about
any particular Integer.

> 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.

Not particularly, but if you ultimately want an executable algorithm,
you are sooner or later going to have to spell out how such a
non-deterministic choice is made.

-Proof-search-, though, is usually quite non-deterministic.