Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 572:a913f19955e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update for Coq 8.11
author Adam Chlipala <adam@chlipala.net>
date Sun, 02 Feb 2020 10:46:14 -0500
parents 81d63d9c1cc5
children 1dc1d41620b6
comparison
equal deleted inserted replaced
571:3fc43e261f67 572:a913f19955e2
779 779
780 %\medskip% 780 %\medskip%
781 781
782 I know no easy fix for this problem of [thunk], but we can define an alternate co-inductive monad that avoids the problem, based on a proposal by Megacz%~\cite{Megacz}%. We ran into trouble because [TBind] was not a constructor of [thunk], so let us define a new type family where "bind" is a constructor. *) 782 I know no easy fix for this problem of [thunk], but we can define an alternate co-inductive monad that avoids the problem, based on a proposal by Megacz%~\cite{Megacz}%. We ran into trouble because [TBind] was not a constructor of [thunk], so let us define a new type family where "bind" is a constructor. *)
783 783
784 Set Universe Polymorphism.
785
784 CoInductive comp (A : Type) : Type := 786 CoInductive comp (A : Type) : Type :=
785 | Ret : A -> comp A 787 | Ret : A -> comp A
786 | Bnd : forall B, comp B -> (B -> comp A) -> comp A. 788 | Bnd : forall B, comp B -> (B -> comp A) -> comp A.
787 789
788 (** This example shows off Coq's support for%\index{recursively non-uniform parameters}% _recursively non-uniform parameters_, as in the case of the parameter [A] declared above, where each constructor's type ends in [comp A], but there is a recursive use of [comp] with a different parameter [B]. Beside that technical wrinkle, we see the simplest possible definition of a monad, via a type whose two constructors are precisely the monad operators. 790 (** This example shows off Coq's support for%\index{recursively non-uniform parameters}% _recursively non-uniform parameters_, as in the case of the parameter [A] declared above, where each constructor's type ends in [comp A], but there is a recursive use of [comp] with a different parameter [B]. Beside that technical wrinkle, we see the simplest possible definition of a monad, via a type whose two constructors are precisely the monad operators.