[Haskell-cafe] type metaphysics

[Eugene Kirpichov]

Luke, sorry for being offtopic, but you are more and more intriguing
me with topology.
I wonder if any stuff from it has, apart from applications in
computability/complexity, also computational applications as useful as
monoids or rings do (i.e. parallel prefix sums).

2009/2/3 Luke Palmer <lrpalmer at gmail.com>:
> 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
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>