[Haskell-cafe] type metaphysics

[Luke Palmer]

On Mon, Feb 2, 2009 at 4:18 PM, Reid Barton <rwbarton at math.harvard.edu>wrote:

> > So here's a programming challenge: write a total function (expecting
> > total arguments) toSame :: ((Nat -> Bool) -> Nat) -> (Nat -> Bool,Nat
> > -> Bool) that finds a pair that get mapped to the same Nat.
> >
> > Ie. f a==f b where (a,b) = toSame f
>
> (Warning: sketchy argument ahead.)  Let f :: (Nat -> Bool) -> Nat be a
> total function and let g0 = const True.  The application f g0 can
> only evaluate g0 at finitely many values, so f g0 = f (< k) for any k
> larger than all these values.  So we can write
>
> > toSame f = (const True, head [ (< k) | k <- [1..], f (const True) == f (<
> k) ])
>
> and toSame is total on total inputs.


Well done!  That's not sketchy at all!  There is always such a k (when the
result type of f has decidable equality) and it is the "modulus of uniform
continuity" of f.  This is computable directly, but the implementation
you've provided might come up with a smaller one that still works (since you
only need to differentiate between const True, not all other streams).

I guess I should hold off on conjecturing the impossibility of things... :-)

Luke
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090202/5eac6b14/attachment.htm