Data.Linear.Communications

This module is based on the content of the functional pearl
How to Take the Inverse of a Type
by Daniel Marshall and Dominic Orchard

Definitions

data Protocol : Type

Totality: total
Visibility: public export
Constructors:

Send : Type -> Protocol -> Protocol

Recv : Type -> Protocol -> Protocol

End : Protocol

Dual : Protocol -> Protocol

Totality: total
Visibility: public export

data LChan : Protocol -> Type

Totality: total
Visibility: export
Constructor: 

MkLChan : LChan p