Delayed.idr

||| Utilities functions for contitionally delaying values.
module Control.Delayed

%default total

||| Type-level function for a conditionally infinite type.
public export
inf : Bool -> Type -> Type
inf True a = Inf a
inf False a = a

Main.idr

module Main

import Data.MonadLike

testFinite : MonadLike True Int
testFinite = do pureC False Z
                pureC True 5

testInfinite : MonadLike True Int
testInfinite = do pureC True Z
                  testInfinite

MonadLike.idr

module Mod.Used

import Control.Delayed

%default total

export
data MonadLike : Bool -> Type -> Type where
  Pure : a -> MonadLike c a

  Bind : MonadLike c1 a ->
         (a -> MonadLike c2 b) ->
         MonadLike (c1 || c2) b

  InfBind : MonadLike True a ->
            Inf (a -> MonadLike c2 b) ->
            MonadLike True b

export
pureC : (c : Bool) -> a -> MonadLike c a
pureC c = Pure

export
(>>=) : MonadLike c1 a -> inf c1 (a -> MonadLike c2 b) -> MonadLike (c1 || c2) b
(>>=) {c1 = True} = InfBind
(>>=) {c1 = False} = Bind