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?

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.

okay, I'm more confused: (okay that's acknowledged), the second `(Fin.t (S n) : Type)`

won't parse`dist`

does _not_ have type `Type -> Type`

but `finType -> Type`

, and the third, `Dist`

, has type `nat -> Set`

.

more importantly, `A -> prob`

is contravariant in `A`

, while monads are covariant

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.

I thought `A -> prob`

would be a bit like the powerset of `A`

, with both covariant and contravariant versions.

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

is finite).

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

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

I see it is a monad from a non-`Type`

category, so I retract the objection on variance — I was missing something, thanks.

do you also see how to turn `finType -> Type`

into a `Type -> Type`

monad?

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.

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

It's probably going to have to be a monad on setoids rather than `Type`

, unless you're happy to add axioms.

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?

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?

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

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.

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.

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.

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

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

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

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

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

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

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?).

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

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

and given the type `Type -> choiceType`

, it must use a classical axiom right?

so _yes_ I was being dense :-)

(I was still thinking of `finType`

or `countableType`

which cannot)

yes, MathComp-Analysis is a classical setting

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

monad.

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.

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.

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

Oh I see. Saw trying to convert probability monad to `Type -> Type`

and thought the libs are specific for that.

abab9579 said:

`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?

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

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: Jan 31 2023 at 13:02 UTC