gistfile1.txt

infixr 9 -*
(-*) : Type -> Type -> Type
(-*) a b = (1 _ : a) -> b

Eff : Type
Eff = IO ()
-- Negation, 
N : Type -> Type
N a = a -* Eff

NN : Type -> Type
NN a = N (N a)

mutual
  data Source : Type -> Type where
    Nil  : Source a
    (::) : a -* N (Sink a) -* Source a

  data Sink : Type -> Type where
    Full : Sink a
    Cont : N (Source a) -* Sink a

infix 9 &|
(&|) : Type -> Type -> Type
a &| b = N (Either (N a) (N b))

await : Source a -* (Eff &| (a -* Source a -* Eff)) -* Eff
await [] r = r (Left (\end => end))
await (x :: xs) r = r (Right (\1 c => ?fsdfsd))

await' : Source a -* (Eff &| (g -* a -* Source a -* Eff)) -* Eff
await' [] r = r (Left (\end => end))
await' (x :: xs) r = r (Right (\1 c => ?fsdfsdd))