DBDBD.hs

-- example from: https://arxiv.org/abs/1611.09259

interface Send X = send : X -> Unit
interface Recieve X = recieve : X
interface Abort = aborting : Zero

catter : [Receive (List X)]List X
catter! = on receive! { nil -> nil | xs -> append xs catter! }

pipe : <Send X>Unit -> <Receive X>Y -> [Abort]Y
pipe <send x -> s> <receive -> r> =
pipe (s unit) (r x)
pipe <_> y = y
pipe unit <_> = abort!


pipe (sends (cons "do" (cons "be" (cons "" nil)))) catter! == "dobe"

spacer : [Send (List Char), Receive (List Char)]Unit
spacer! = send receive; send " "; spacer!

pipe (sends (cons "do" (cons "be" (cons "" nil)))) (pipe spacer! catter!) == "do be "

pipe (pipe (sends (cons "do" (cons "be" (cons "" nil)))) spacer!) catter! == "do be "

extensible.hs

#!/usr/bin/env stack
{- stack
  runghc
  --resolver nightly-2017-07-06
  --package extensible
  --package monad-skeleton
-}

{-# LANGUAGE GADTs, TypeOperators, DataKinds, QuasiQuotes, TemplateHaskell, FlexibleContexts #-}
{-# LANGUAGE OverloadedLabels, RankNTypes, LambdaCase, PolyKinds, TypeApplications #-}
import Control.Monad.Skeleton
import Data.Extensible
import Data.Extensible.Internal
import Data.Void

skipEff :: Eff xs a -> Eff (k : xs) a
skipEff = hoistSkeleton (\(Instruction m av) -> Instruction (navNext m) av)

extend :: IncludeAssoc xs ys => Eff ys a -> Eff xs a
extend = hoistSkeleton (\(Instruction m av) -> Instruction (hlookup m inclusionAssoc) av)

data Send a r where
  Send :: x -> Send x ()

data Recieve r a where
  Recieve :: Recieve x x

data Abort r a where
  Aborting :: Abort Void a

catter :: Eff '["recieve" >: Recieve [r]] [r]
catter = do
  liftEff #recieve Recieve >>= \case
    [] -> return []
    xs -> (xs ++) <$> catter

pipe' :: Associate "aborting" (Abort Void) xs => Eff ("send" >: Send x : xs) () -> Eff ("recieve" >: Recieve x : xs) y -> Eff xs (y, ())
pipe' es er
  = peelEff1
    (\a b -> peelEff1 (\a b -> return (a,b)) (\Recieve _ _ -> liftEff #aborting Aborting) er ())
    (\(Send x) s () -> peelEff1 (\a b -> return (a,b)) (\Recieve r b -> pipe' (skipEff $ snd <$> s () ()) (skipEff $ fst <$> r x ())) er ()) es ()

pipe :: Associate "aborting" (Abort Void) xs => Eff ("send" >: Send x : xs) () -> Eff ("recieve" >: Recieve x : xs) y -> Eff xs y
pipe x y = fst <$> pipe' x y
    
sends :: [a] -> Eff '["send" >: Send a] ()
sends xs = mapM_ (liftEff #send . Send) xs

runAborting :: Eff '["aborting" >: Abort Void] a -> Maybe a
runAborting ev = leaveEff $ peelEff1 (\a () -> return $ Just a) (\Aborting _ _ -> return Nothing) ev ()

spacer :: Eff ["send" >: Send String, "recieve" >: Recieve String] ()
spacer = liftEff #recieve Recieve >>= liftEff #send . Send >> liftEff #send (Send " ") >> spacer

(>$>) = pipe

main = do
  print $ runAborting $ extend (sends ["do", "be"]) >$> (extend catter)