Noncomputable vs crisp variables

Stream: Type theory

[David Michael Roberts]

There is a thing in Agda that implements the "flat modality" from real-cohesive type theory / crisp type theory. Conceptually, it's something like thinking of functions A->B between types as being "continuous", and then if one has a function ♭(A)->B, this is "discontinuous" ("crisp" in the generic variable of type A). More generally, given a multivariable function some of the variables can be crisp. The operation ♭ is an idempotent comonad, in category theoretic semantics.

I'm wondering if noncomputable acts in a similar way. My only understanding of noncomputable is what I just read here, so I'm open to being educated.

[David Michael Roberts]

(Obviously noncomputable applies to more than just definitions of functions, and that's fine, I expect that given some Curry–Howard magic.)

[Eric Wieser]

(I don't understand your parenthesized statement; noncomputable applies only to data and not proofs, aka just to definitions of functions)

[David Michael Roberts]

Well, one could have a proposition that depended on noncomputable, I guess. It's not important for my question.

[Mario Carneiro]

I don't think there is much of an analogue. noncomputable is a property of terms, not of positions in a term / arguments to a function. In particular, the rules for when noncomputable is not viral are very term-oriented: a term constructed from noncomputable parts is itself noncomputable unless it is a type or type constructor (it has type ... -> Sort u) or it is a proof (it has type p where p : Prop). By contrast, there is no "taint analysis" style mechanism to justify that a function like \lam x y, y (where x and y have a generic type) preserves the noncomputability of its second argument and discards the first. That is a much more refined notion than lean's version, which summarizes the whole analysis into one bit: computable or not.

[Eric Wieser]

This absence of "taint analysis" comes up when working with noncomputable instances where the fields you care about are computable but the ones you don't aren't, and you end up being unfairly tainted by noncomputability

[Eric Wieser]

But usually there are workarounds

[Mario Carneiro]

One of the workarounds is the type erased A, which basically launders the type through types and proofs so that you end up with a type that is provably isomorphic to A but is also computable by lean's definition. You can use this as a poor man's flat modality, at least as long as you aren't doing anything too crazy with the value

[Eric Wieser]

(docs#erased)

[David Michael Roberts]

Aha, erased.out : erased α → α looks like the counit for flat, thanks. But I'm not so reliant on this to be true.

[Reid Barton]

I would rather consider erased.mk : α → erased α to be the unit of a modality, since it's the computable one. Noncomputably, erased α is isomorphic to α so there is not much point in looking at the structure that erased has if you allow noncomputable functions.

[Reid Barton]

A noncomputable function a -> b is the same as a computable function a -> erased b but it's not the same as anything like ?? a -> b--I'm not sure quite how to prove this, but it seems pretty clear. So I would imagine the computable setting as lying over the noncomputable/classical one, with erased as the corresponding modality/monad/reflection/whatever.

[Reid Barton]

There should be a picture where, in the computable setting, each type corresponds to something like a topological space, whose points are the classical values of the type but where the only computable functions we can define out of the type are the continuous ones. For example, sequences nat -> bool form a Cantor space (because a computable function of a sequence to something discrete like bool can only depend on finitely many entries in the sequence). In this picture, erased will be retopologizing with the indiscrete topology.

[Mario Carneiro]

A noncomputable function a -> b is the same as a computable function a -> erased b but it's not the same as anything like ?? a -> b--I'm not sure quite how to prove this, but it seems pretty clear.

Perhaps consider the noncomputable function choice : nonempty A -> A for some A that has no computational realizers, for example A := decidable continuum_hypothesis. nonempty A is equal to true so the ?? (nonempty A) -> A function is equivalent to ?? true -> A, so if ?? true is computably inhabited we have a contradiction, and if there are no inhabitants then it is extensionally equal to ?? true -> false, so it's not an equivalence, since nonempty A -> A and nonempty A -> false are not equal in the classical setting.