Logic.fs

type ('r, 'a) logic = Logic of (('a -> 'r -> 'r) -> 'r -> 'r)

let runLogic : ('r, 'a) logic -> ('a -> 'r -> 'r) -> 'r -> 'r
  = fun (Logic run) -> run

let bind : ('r, 'a) logic -> ('a -> ('r, 'b) logic) -> ('r, 'b) logic
  = fun (Logic ma) amb ->
    Logic <| fun yes no ->
      ma (fun a -> runLogic (amb a) yes) no

let just : 'a -> ('r, 'a) logic
  = fun a ->
    Logic <| fun yes no ->
      yes a no

let zero : unit -> ('r, 'a) logic
  = fun () ->
    Logic <| fun _yes no ->
      no

let select : ('r, 'a) logic -> ('r, 'a) logic -> ('r, 'a) logic
  = fun (Logic l) (Logic r) ->
    Logic <| fun yes no ->
      l yes (r yes no)

let reflect : ('a * ('r, 'a) logic) option -> ('r, 'a) logic
  = function
    | None         -> zero ()
    | Some (a, ma) -> select (just a) ma

let split : ('r, 'a) logic -> ('r, ('a * ('r, 'a) logic) option) logic
  = fun (Logic ma) ->
      ma
        (fun a rest -> just (Some (a, bind rest reflect)))
        (just None)

Logic.hs

{-# language RankNTypes #-}

import Control.Applicative
import Control.Monad
import Control.Monad.Trans.Class

newtype Logic a = Logic
  { runLogic :: forall r. (a -> r -> r) -> r -> r
  }

just :: a -> Logic a
just a = Logic $ \yes no -> yes a no

bind :: Logic a -> (a -> Logic b) -> Logic b
bind (Logic xs) callb = Logic $ \yes no ->
  xs (\x -> runLogic (callb x) yes) no

zero :: Logic a
zero = Logic $ \_yes no -> no

plus :: Logic a -> Logic a -> Logic a
plus (Logic l) (Logic r) = Logic $ \yes no ->
  l yes (r yes no)

split :: Logic a -> Logic (Maybe (a, Logic a))
split (Logic ma) = do
  ma
    (\a rest -> just $ Just (a, bind rest reflect))
    (just Nothing)

reflect :: Maybe (a, Logic a) -> Logic a
reflect Nothing = zero
reflect (Just (a, ma)) = just a `plus` ma