Stream: Coq users

Topic: Probability Monad for Fin.t

Mukesh Tiwari (Sep 17 2022 at 20:32):

Hi everyone,

what is the best way to turn this Dist definition into an instance of monad?

Definition Dist {n : nat} := Fin.t (S n) -> prob.

More context: If I define a probability distribution as

Definition dist (A : Type) := list (A * prob)

then I can make it an instance of monad. Also, I can define a distribution as

Definition dist (A : finType) := A -> prob

and this definition can also be turned into an instance of monad. However, say, if I define a distribution as

Definition Dist {n : nat} := Fin.t (S n) -> prob.

which is almost same as the previous definition. In previous two definitions, the type of dist is Type -> Type, but the type of Dist is Set and this can't be turned into an instance of monad. I can add a spurious type

Definition Dist {n : nat} (Fin.t (S n) : Type) := Fin.t (S n) -> prob

then it appears similar to the finType definition, except A is concrete, i.e., Fin.t (S n). First, Coq does not accept this definition and second it's not serving any purpose, so my question is: what is the best way to turn this into monad?

Paolo Giarrusso (Sep 18 2022 at 09:27):

Your second dist can't actually turn into a Type -> Type monad by itself, only with a coercion, and I'm not sure that's meaningful. The third seems even harder... unless you use monads on different categories.

Paolo Giarrusso (Sep 18 2022 at 09:31):

okay, I'm more confused: (Fin.t (S n) : Type) won't parse (okay that's acknowledged), the second dist does _not_ have type Type -> Type but finType -> Type, and the third, Dist, has type nat -> Set.

Paolo Giarrusso (Sep 18 2022 at 09:34):

more importantly, A -> prob is contravariant in A, while monads are covariant

Paolo Giarrusso (Sep 18 2022 at 09:37):

the best I can say is that fun (A : Type) => A -> prob is a contravariant functor from Type, and fun {n : nat} => Fin.t (S n) -> prob could be a contravariant functor from a different category.

James Wood (Sep 18 2022 at 09:38):

I thought A -> prob would be a bit like the powerset of A, with both covariant and contravariant versions.

James Wood (Sep 18 2022 at 09:39):

Particularly if there's a finite support (or, as we have here, the even stronger property that A is finite).

Paolo Giarrusso (Sep 18 2022 at 09:41):

if you need finite support, then it might be a monad from a non-Type category but it won't be an ExtLib Monad https://coq-community.org/coq-ext-lib/v0.11.1/ExtLib.Structures.Monad.html

James Wood (Sep 18 2022 at 09:42):

https://ncatlab.org/nlab/show/distribution+monad

Paolo Giarrusso (Sep 18 2022 at 09:45):

I see it is a monad from a non-Type category, so I retract the objection on variance — I was missing something, thanks.

Paolo Giarrusso (Sep 18 2022 at 09:46):

do you also see how to turn finType -> Type into a Type -> Type monad?

James Wood (Sep 18 2022 at 09:47):

I might do something like:

Definition Dist (A : Type) := { xs : list A & forall x, In x xs -> prob }.

I think you have to define it on (something like) Type if you want a monad because there will be infinitely many distributions even on a 2-element set.

James Wood (Sep 18 2022 at 09:48):

It'd be nice to enforce that it sums to 1, too.

James Wood (Sep 18 2022 at 09:50):

It's probably going to have to be a monad on setoids rather than Type, unless you're happy to add axioms.

Paolo Giarrusso (Sep 18 2022 at 09:54):

thanks for clarifying how the second definition works, and I retract the comments about that. But do you see how to deal with the third one?

Paolo Giarrusso (Sep 18 2022 at 09:54):

It seems there might be a monad from the partial order on N, but I still miss how to make it a monad from Type — it doesn't seem worth trying, but I'm probably wrong there too?

Mukesh Tiwari (Sep 18 2022 at 17:24):

@Paolo Giarrusso @James Wood Thank you very much! It seems I can't avoid reading a bit of type theory and category theory.

James Wood (Sep 18 2022 at 22:51):

Paolo Giarrusso said:

do you also see how to turn finType -> Type into a Type -> Type monad?

Maybe you could do something equivalent to picking out a finite support. You have T : finType -> Type and A : Type, then pick out a finite subtype of A and apply T to it.

James Wood (Sep 18 2022 at 22:53):

I guess that would at least preserve functoriality of T, and maybe you could find some properties of T to yield the monad laws, but I wouldn't know what they were.

Arthur Azevedo de Amorim (Sep 19 2022 at 00:06):

I have an implementation of finite probability theory here: https://github.com/arthuraa/finprob. It allows you to define probability distributions over any ordered type. These distributions form themselves an ordered type, so you can define a monad structure over them: the Giry monad.

Karl Palmskog (Sep 19 2022 at 05:46):

Giry monad also here: https://github.com/coq-community/alea

Karl Palmskog (Sep 19 2022 at 11:26):

unless I'm mistaken, Infotheo has a Giry monad as well? https://github.com/affeldt-aist/infotheo/tree/master/probability

Karl Palmskog (Sep 19 2022 at 11:28):

and another one: https://github.com/jtassarotti/coq-proba

Reynald Affeldt (Sep 19 2022 at 12:11):

the monad in infotheo uses finitely-supported distributions over choiceType: https://github.com/affeldt-aist/infotheo/blob/master/probability/fsdist.v

Paolo Giarrusso (Sep 19 2022 at 16:25):

And the infotheo one doesn't try to fit into a generic monad interface, AFAICT? Or do I miss it?

Reynald Affeldt (Sep 19 2022 at 16:57):

in a sense it does since it is used to give a model to the hierarchy of monads of monae: https://github.com/affeldt-aist/monae/blob/master/hierarchy.v

Paolo Giarrusso (Sep 19 2022 at 18:11):

but... A => {dist A} isn't Type => Type since it takes a choiceType, while in your link to monae, isMonadProb takes M : UU0 -> UU0 and UU0 := Type. Feel free to tell me if I'm being dense: I agree that fsdist fits a more generic notion of monad, but I still don't see how to fit it into the "simple" monads of Haskell/ExtLib/(maybe monae?).

Reynald Affeldt (Sep 19 2022 at 18:24):

the model is here: https://github.com/affeldt-aist/monae/blob/19f1e2ad2c2226b913e208a877a53622e0e257d2/proba_monad_model.v#L23

Reynald Affeldt (Sep 19 2022 at 18:30):

this uses a choice_of_Type function that ultimately comes from MathComp-Analysis

Paolo Giarrusso (Sep 19 2022 at 18:30):

and given the type Type -> choiceType, it must use a classical axiom right?

Paolo Giarrusso (Sep 19 2022 at 18:31):

so _yes_ I was being dense :-)

Paolo Giarrusso (Sep 19 2022 at 18:31):

(I was still thinking of finType or countableType which cannot)

Reynald Affeldt (Sep 19 2022 at 18:31):

yes, MathComp-Analysis is a classical setting

abab9579 (Sep 20 2022 at 02:58):

I find it interesting that there is a coq library for monads but it only supports Type -> Type monad.

John Wiegley (Sep 20 2022 at 03:48):

abab9579 said:

I find it interesting that there is a coq library for monads but it only supports Type -> Type monad.

I think that's mostly because those are the monads most reached for by programmers.

Reynald Affeldt (Sep 20 2022 at 04:17):

abab9579 said:

I find it interesting that there is a coq library for monads but it only supports Type -> Type monad.

I don't know which library you are referring to but in monae besides the hierarchy of "Type -> Type" monads there is a more general formalization (https://github.com/affeldt-aist/monae/blob/master/category.v) that we use as an intermediate step to build another monad.

Reynald Affeldt (Sep 20 2022 at 04:19):

But as John said for semantics in the end we didn't really need the more general formalization.

abab9579 (Sep 20 2022 at 04:28):

Oh I see. Saw trying to convert probability monad to Type -> Type and thought the libs are specific for that.

Mukesh Tiwari (Sep 20 2022 at 09:06):

abab9579 said:

I find it interesting that there is a coq library for monads but it only supports Type -> Type monad.

Interesting, I did not know that there is more general than this. Is there any Coq library that has the most general Monad encoding?

Li-yao (Sep 20 2022 at 09:11):

jwiegley/category-theory :)

For a middle ground that's still somewhat programmer-friendly there are indexed monads, cf. McBride's Kleisli arrows of outrageous fortune.

John Wiegley (Sep 20 2022 at 15:01):

Li-yao said:

jwiegley/category-theory :)

For a middle ground that's still somewhat programmer-friendly there are indexed monads, cf. McBride's Kleisli arrows of outrageous fortune.

Thanks, Li-yao. :) Also, within the category-theory library I'm now working on a sub-library, under Category.Theory.Coq that refines several CT concepts to their programming use-case for Coq developers. I'd be happy to include indexed monads, if there is a practical use. Mostly I'm looking to the Haskell library ecosystem to see what they've found useful over the past several years.

Last updated: Oct 13 2024 at 01:02 UTC