
  0 | module Control.Cont.Void
  1 | 
  2 | import Control.EffectAlgebra
  3 | import Control.HigherOrder
  4 | 
  5 | import Control.Monad.Free
  6 | 
  7 | public export
  8 | data VoidC1 : Type -> Type where
  9 | 
 10 | public export
 11 | VoidC : (Type -> Type) -> (Type -> Type)
 12 | VoidC = Lift VoidC1
 13 | 
 14 | public export
 15 | VoidE : (Type -> Type) -> (Type -> Type)
 16 | VoidE = Lift VoidC1
 17 | 
 18 | public export
 19 | Uninhabited (VoidC1 a) where
 20 |   uninhabited x impossible
 21 | 
 22 | public export
 23 | Functor VoidC1 where
 24 |   map f x impossible
 25 | 
 26 | public export
 27 | runVoidC : Free VoidC a -> a
 28 | runVoidC (Return x) = x
 29 | runVoidC (Op (MkLift x)) = absurd x
 30 | 
 31 | namespace Algebra
 32 |   public export
 33 |   [Void] (mon : Monad m) => Algebra VoidE m where
 34 |     alg ctx hdl (MkLift x) = absurd x
 35 | 
 36 |   %hint
 37 |   public export
 38 |   AlgebraVoid : (mon : Monad m) => Algebra VoidE m
 39 |   AlgebraVoid = Algebra.Void
 40 |