I picked 1-Lipschitzness, as that one seems to be the best motivated.
I would motivate this by saying that |ψ(f)−ψ(f′)|supx|f(x)−f′(x)|≤1 can be rewritten as supϕ∈{g↦g(x)}∪{ψ}|ϕ(f)−ϕ(f′)|=supϕ∈{g↦g(x)}|ϕ(f)−ϕ(f′)|.
As for implementing it: I’m not sure whether there’s a way to enforce concavity and 1-Lipschitzness on the type level, but one sure could define [[X→[0,1]]→[0,1]]. Here’s a definition of [−∞,∞] without much type-level safety: newtype Real = UnsafeReal {greaterThan :: Double -> ()}; embedDouble :: Double -> Real; embedDouble d = UnsafeReal (\d' -> if d>d' then () else error ("embedDouble" + show d + show d')). So long as nobody uses try/catch or UnsafeReal, the only thing you can get out of a value of this type is that it is larger than a given double.
I would motivate this by saying that |ψ(f)−ψ(f′)|supx|f(x)−f′(x)|≤1 can be rewritten as supϕ∈{g↦g(x)}∪{ψ}|ϕ(f)−ϕ(f′)|=supϕ∈{g↦g(x)}|ϕ(f)−ϕ(f′)|.
As for implementing it:
I’m not sure whether there’s a way to enforce concavity and 1-Lipschitzness on the type level, but one sure could define [[X→[0,1]]→[0,1]]. Here’s a definition of [−∞,∞] without much type-level safety:
newtype Real = UnsafeReal {greaterThan :: Double -> ()}; embedDouble :: Double -> Real; embedDouble d = UnsafeReal (\d' -> if d>d' then () else error ("embedDouble" + show d + show d')). So long as nobody usestry/catchorUnsafeReal, the only thing you can get out of a value of this type is that it is larger than a given double.