Stream: Coq users

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

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 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: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):

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:

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: Jun 25 2024 at 15:02 UTC