Skip to main content
MathOverflow

Return to Answer

added 119 characters in body
Source Link
Urs Schreiber
Urs Schreiber
  • 19.8k
  • 1
  • 74
  • 269

Mutations -- aka "side effects" or "changes of state" -- in functional programming languages, such as the programming languages Coq and Agda which run Homotopy Type Theory, are implemented by equipping the type theory with monads on the type system, as described on the nLab at

See there for details on how this works.

Now in homotopy type theory these monads are of course refined to ∞-monads.

These are currently best explored in terms of HoTT in the simple special cases where

  1. either the $\infty$-monad is freefree presentable, in which case an $\infty$-algebra over it is a higher inductive type;

  2. or they are idempotent, which is the case where they are called modal operators .

See the discussion behind the links for pointers.

Neither of these special case may be what you are after, but I think, while it hasn't been discussed much in print to date, it is in principle straightforward to talk about more general $\infty$-monads in (or rather: on) homotopy type theory, to encode general kinds of side effects/mutations.

Mutations -- aka "side effects" or "changes of state" -- in functional programming languages, such as the programming languages Coq and Agda which run Homotopy Type Theory, are implemented by equipping the type theory with monads on the type system, as described on the nLab at

See there for details on how this works.

Now in homotopy type theory these monads are of course refined to ∞-monads.

These are currently best explored in terms of HoTT in the simple special cases where

  1. either the $\infty$-monad is free, in which case an $\infty$-algebra over it is a higher inductive type;

  2. or they are idempotent, which is the case where they are called modal operators .

See the discussion behind the links for pointers.

Neither of these special case may be what you are after, but I think, while it hasn't been discussed much in print to date, it is in principle straightforward to talk about more general $\infty$-monads in (or rather: on) homotopy type theory, to encode general kinds of side effects/mutations.

Mutations -- aka "side effects" or "changes of state" -- in functional programming languages, such as the programming languages Coq and Agda which run Homotopy Type Theory, are implemented by equipping the type theory with monads on the type system, as described on the nLab at

See there for details on how this works.

Now in homotopy type theory these monads are of course refined to ∞-monads.

These are currently best explored in terms of HoTT in the simple special cases where

  1. either the $\infty$-monad is free presentable, in which case an $\infty$-algebra over it is a higher inductive type;

  2. or they are idempotent, which is the case where they are called modal operators .

See the discussion behind the links for pointers.

Neither of these special case may be what you are after, but I think, while it hasn't been discussed much in print to date, it is in principle straightforward to talk about more general $\infty$-monads in (or rather: on) homotopy type theory, to encode general kinds of side effects/mutations.

Source Link
Urs Schreiber
Urs Schreiber
  • 19.8k
  • 1
  • 74
  • 269

Mutations -- aka "side effects" or "changes of state" -- in functional programming languages, such as the programming languages Coq and Agda which run Homotopy Type Theory, are implemented by equipping the type theory with monads on the type system, as described on the nLab at

See there for details on how this works.

Now in homotopy type theory these monads are of course refined to ∞-monads.

These are currently best explored in terms of HoTT in the simple special cases where

  1. either the $\infty$-monad is free, in which case an $\infty$-algebra over it is a higher inductive type;

  2. or they are idempotent, which is the case where they are called modal operators .

See the discussion behind the links for pointers.

Neither of these special case may be what you are after, but I think, while it hasn't been discussed much in print to date, it is in principle straightforward to talk about more general $\infty$-monads in (or rather: on) homotopy type theory, to encode general kinds of side effects/mutations.