PHOAS, not total?

phoas.idr

-- Inspired by https://www.fpcomplete.com/user/edwardk/phoas
record Rec : (p : Type -> Type -> Type) -> (a : Type) -> (b : Type) -> Type where
  MkRec : (runRec : {r : Type} -> (b -> r) -> (p a r -> r) -> r) -> Rec p a b

purerec : b -> Rec p a b
purerec b = MkRec $ \br,_ => br b

-- not total?
seqrec : Rec p a b -> (b -> Rec p a c) -> Rec p a c
seqrec m f = MkRec $ \kp, kf => runRec m (\a => runRec (f a) kp kf) kf