Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Using the lack of strict positivity to run an infinite computation
data EventT : (event : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
MkEventTCont : (event -> m (EventT event m a)) -> EventT event m a
MkEventTTerm : m a -> EventT event m a
MkEventTEmpty : EventT event m a
data LAM : (x : Type) -> Type where
App : x -> x -> LAM x
Lam : (x -> x) -> LAM x
LC : Type
LC = EventT () LAM Void
app : LC -> LC -> LC
app f t = MkEventTCont (\ () => App f t)
lam : (LC -> LC) -> LC
lam b = MkEventTCont (\ () => Lam b)
delta : LC
delta = lam (\ x => app x x)
omega : LC
omega = app delta delta
reduce : LC -> LC
reduce lc@(MkEventTCont e) = case e () of
App (MkEventTCont f) t => case f () of
Lam b => reduce (b t)
_ => lc
_ => lc
reduce lc = lc
-- good luck running `reduce omega`!
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment