bens

{-# LANGUAGE EmptyDataDecls    #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}

module Sublist (S, L, R, Sublist, sublistHead, sublistTail, fromSublist) where

import           Control.Applicative ((<|>))
import qualified Control.Lens        as L
import           Data.Maybe          (fromMaybe)

bens

import Control.Applicative
import Control.Concurrent (forkIO, newEmptyMVar, putMVar, takeMVar)
import Control.Monad
import Control.Monad.Trans.Class
import Control.Monad.IO.Class
import System.Command

newtype Cmd m a = Cmd { runCmd :: m (Either (ExitCode, String) a) }

cmd :: MonadIO m => FilePath -> [String] -> String -> Cmd m String

bens

runController :: (MonadIO m) => Controller a -> Producer a m ()
runController (Controller m) = do
  input <- liftIO m
  let loop = do
        xM <- liftIO (atomically $ recv input)
        maybe (return ()) (\x -> yield x >> loop) xM
  loop

type StateFn s = (Maybe s -> s) -> IO s

bens

{-# LANGUAGE EmptyDataDecls           #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE RecordWildCards          #-}

module Command
  ( Command, Root, User, Verbose
  , runAsRoot, runAsCurrentUser
  , command, getTempName, dropRoot
  ) where

bens

-- Decide if applying f over a collection gives either Nothing or Just for every element.
decideMaybes :: Traversable f => (a -> Maybe b) -> f a -> Maybe (Either (f a) (f (a, b)))
decideMaybes f xs =
  asum [Left <$> nothingsOf pairs, Right <$> justsOf pairs, Nothing]
  where
    pairs      = fmap (\x -> (x, f x)) xs
    nothingsOf = traverse (\(x,y) -> x <$ guard (isNothing y))
    justsOf    = traverse (\(x,y) -> (x, fromJust y) <$ guard (isJust y))

bens

module MonadLaws where

open import Category.Applicative
open import Category.Applicative.Indexed
open import Category.Functor
open import Category.Monad
open import Category.Monad.Indexed
open import Data.Maybe renaming (monad to monadMaybe)
open import Function
open import Level

bens

{-# OPTIONS --termination-depth=2 #-}

module Printf where

open import Algebra.FunctionProperties using (Associative)
open import Data.Char using (Char) renaming (_≟_ to _≟ᶜ_)
open import Data.List using (List; []; _∷_; [_]; length)
open import Data.Maybe
open import Data.Nat using (ℕ; suc)
open import Data.Nat.Show using (show)

bens

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

import Control.Category
import GHC.Exts (Constraint)
import Prelude hiding ((.))

bens

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Rank2Types                #-}

module Unfold where

import           Control.Applicative
import           Data.List

data Fold a b = forall x . Fold (x -> a -> x) x (x -> b)

bens

module Main where

import Control.Monad.Free

data StackF a
    = Push Int a
    | Pop (Int -> a)

instance Functor StackF where
    fmap f (Push x k) = Push x (f k)