# Self-algebraic effects in Coq

This plugin allows to easily apply an effectful translation to CIC terms.
The translation is generic over the effect, provided it complies with a few
requirements, that turn it into what we call a self-algebraic pseudo-monad (SAPM).

A SAPM is described by the following terms:
- `M : Type@{i} -> Type@{i}`
- `ret : forall A : Type, A -> M A`
- `bind : forall (A B : Type), M A -> (A -> M B) -> M B`
- `El : M TYPE -> TYPE`
- `hbind : forall (A : Type) (B : TYPE), M A -> (A -> El B) -> El B`
- `pbind : foral (A : Type) (R : M TYPE) (B : A -> El (R  →ᵉ Typeᵉ))
    (l : M A) (r : El R) (f : forall x : A, El (B x r)), El (hbind A (R  →ᵉ Typeᵉ) l B r)`

where the following data is derived as:
- `TYPE := {A : Type & M A -> A}`

The terms must satisfy a few definitional equations, namely:
- `hbind A B (ret A t) f ≡ f t`
- `pbind A B (ret A t) f r ≡ f t r`

A paper describing this translation in-depth can be found
[here](https://www.xn--pdrot-bsa.fr/articles/weaning.pdf).

# Compilation

This requires Coq 8.6. If the `COQBIN` variable is correctly set, a `make`
invokation should be enough.

# Use of the plugin

An effect is described by any module `EFF` containing the above definitions,
plus the following constants:
- `Free : Type -> M TYPE := ret (exist Type (fun A => M A -> A) (M A) (fun x => bind x (fun x => x)))`
- `Typeᵉ : M TYPE := Free TYPE`
- `Prodᵉ : forall (A : M TYPE), (B : (El A).(wit) -> M TYPE) -> M TYPE := ...`

Ideally, these constants should be derived from the given self-algebraic structure,
but for now this is still a TODO.

Before being available, the effect must first be declared using the following
command:

```
Declare Effect EFF.
```

Aftewards, it can be used in two ways.
- Coq definitions can be automatically translated.
- New terms can by constructed through the translation.

The first case is covered by the command:
```
Effect Translate foo using EFF.
```
where `foo` is the global definition to translate. The command defines a new
constant `fooᵉ` whose type is the translated type of `foo`.

The second case is covered by the command:
```
Effect Definition foo : T using EFF.
```
which opens a proof whose goal is the translation of T. After the proof is
completed, an axiom `foo : T` is added to the environment, and a constant
`fooᵉ` is defined with the term given by the proof.

# Examples

The repository contains a few examples of SAPM, some as effects, other
handcoded. Subfolders of the `theory` folder correspond to various instances of
the effects.

Files named `Eff.v` declare the structure effect to be used by the translator.
Files named `Alg.v` define instead combinators to play with the translation by
hand, without having to resort to the plugin. Files name `AlgParam.v` define
combinators to play with the parametric translation.

## Exceptions (`M A ~ A + E`)

The underlying translation is a variant of Friedman's trick, except that it
scales to dependent type theory in a convoluted way. Obviously, the resulting
theory is inconsistent, but it allows to extract constructive data out of CIC
proofs. Most notably `[(A → ⊥) → ⊥] ∼ ([A] → E) → E`, which allows to reason
classically on the first-order fragment.

## Non-determinism (`M A ~ A × list A`)

I do not know any logical interpretation for that one.

## Unbounded fixpoints (`M A ~ νX. A + X`)

Nothing interesting yet.

## Writer (`M A ~ A × W`)

Nothing interesting yet.

# License

This software is licensed under the WTFPL 2.0.