Skip to content

Instantly share code, notes, and snippets.

@ahmadsalim

ahmadsalim/phoas.idr

Created March 14, 2015 15:30
Show Gist options
  • Save ahmadsalim/7ef5198397348e68b999 to your computer and use it in GitHub Desktop.
Save ahmadsalim/7ef5198397348e68b999 to your computer and use it in GitHub Desktop.
Download ZIP
PHOAS, not total?
Raw
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment