Question: Computational Types

Many interesting data structures are only implementable (or only efficiently implementable) on a subset of types. For example, we often think of sets as having a decidable equality which enables us to, for example, compute the cardinality of a set. The method of expressing these constraints is of key importance to high levels of abstraction.

Goals

There are several primary goals:

1. Easy to program with (this includes reasonably efficient resolution)
2. Expressive
3. Faithful to their mathematics formulations
4. Easy to reason about

Structure Parameter

Class Monad1 (m : Type -> Type) (P : Type -> Type) : Type :=
{ ret1 : forall {t} {Pt : P t}, t -> m t
; bind1 : forall {t} {u} {Pu : P u}, m t -> (t -> m u) -> m u
}.

Structure Field

Class Monad2 (m : Type -> Type) : Type :=
{ MonP : Type -> Type
; ret2 : forall t, MonP t -> t -> m t
; bind2 : forall t u, MonP u -> m t -> (t -> m u) -> m u
}.

Dependent Type

Class Monad3 (P : Type -> Type) (m : forall (T : Type) {PT : RESOLVE (P T)}, Type) : Type :=
{ ret3 : forall t (Pt : RESOLVE (P t)), t -> m t
; bind3 : forall t u (Pt : RESOLVE (P t)) (Pu : RESOLVE (P u)), m t -> (t -> m u) -> m u 
}.