fixY

gistfile1.txt

delay :: MonadQuote m => (PC.Term PC.TyName PC.Name ()) -> m (PC.Term PC.TyName PC.Name ())
delay body = PC.LamAbs () <$> safeFreshName "thunk" <*> liftQuote Unit.getBuiltinUnit <*> pure body

delayType :: MonadQuote m => (PC.Type PC.Tyname ()) -> m (PC.Type PC.Tyname ())
delayType orig = PC.TyFun () <$> liftQuote Unit.getBuiltinUnit <*> pure orig

force :: MonadQuote m => (PC.Term PC.TyName PC.Name ()) -> m (PC.Term PC.TyName PC.Name ())
force thunk = PC.Apply () thunk <$> liftQuote Unit.getBuiltinUnitval

delayFunction :: MonadQuote m => (PC.Type PC.Tyname ()) -> (PC.Term PC.TyName PC.Name ()) -> m (PC.Term PC.TyName PC.Name ())
delayFunction ty f = do
    n <- safeFreshName "arg"
    forcedUse <- force $ PC.Var () n
    dType <- delayType ty
    pure $ PC.LamAbs () n dType $ PC.Apply () f forcedUse

-- | A fixpoint combinator on functions of type @a -> a@.
fixY :: MonadQuote m => (PC.Type PC.Tyname ()) -> (PC.Term PC.TyName PC.Name ()) -> m (PC.Term PC.TyName PC.Name ())
fixY ty f = do
    unitTy <- liftQuote Unit.getBuiltinUnit
    z <- liftQuote Function.getBuiltinFix
    let instantiated = PC.TyInst () (PC.TyInst () z unitTy) ty
    zFunction <- delayFunction ty f
    pure $ PC.Apply () instantiated zFunction