Damn it, I came to write about the monad1 then saw the edit. You may want to add it to this list, and compare it with the other entries.
Here’s a dissertation and blog post by Jared Tobin on using (X -> R) -> R with flat reals to represent usual distributions in Haskell. He appears open to get hired.
Maybe you want a more powerful type system? I think Coq allows constructing that subtype of a type which satisfies a property. Agda’s cubical type theory places a lot of emphasis for its for the unit interval. Might dependent types be enough express lipschitzness and concavity?
1: Spotted it during literature search on pushforwards to measure the distribution of the vector of all activations in a neural network for one input, given the known distribution of inputs to a GAN generator that outputs inputs to the first network. Which I started modeling (as ((Neurons -> R) -> R) -> R) between you giving me that DT book and first reading about the technique in this post :). imalsoopentogethired
Damn it, I came to write about the monad1 then saw the edit. You may want to add it to this list, and compare it with the other entries.
Here’s a dissertation and blog post by Jared Tobin on using
(X -> R) -> Rwith flat reals to represent usual distributions in Haskell. He appears open to get hired.Maybe you want a more powerful type system? I think Coq allows constructing that subtype of a type which satisfies a property. Agda’s cubical type theory places a lot of emphasis for its for the unit interval. Might dependent types be enough express lipschitzness and concavity?
1: Spotted it during literature search on pushforwards to measure the distribution of the vector of all activations in a neural network for one input, given the known distribution of inputs to a GAN generator that outputs inputs to the first network. Which I started modeling (as
((Neurons -> R) -> R) -> R) between you giving me that DT book and first reading about the technique in this post :). imalsoopentogethired