{-# LANGUAGE Trustworthy #-} -- can't use Safe due to IsList instances
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PartialTypeSignatures #-}

{-# LANGUAGE AllowAmbiguousTypes #-} -- these are needed for numerical monoids
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}

-- The following two extensions are used only in examples:

-- {-# LANGUAGE OverloadedLists #-}
-- {-# LANGUAGE OverloadedStrings #-}

-- |
-- Module      : Control.Monad.List.Exotic
-- Description : Non-standard monads on the list functor
-- Copyright   : (c) Dylan McDermott, Maciej Piróg, Tarmo Uustalu, 2020
-- License     : MIT
-- Maintainer  : maciej.adam.pirog@gmail.com
-- Stability   : experimental
-- Portability : portable
--
-- The usual list monad is only one of infinitely many ways to turn
-- the List functor into a monad. This module collects a number of
-- such non-standard "list" monads.
--
-- __Notes:__
--
-- * Types marked with \"(?)\" have not been formally verified to be
-- monads (yet), though they were thoroughly tested with billions of
-- QuickCheck tests.
--
-- * Monads in this module are defined in terms of @join@ rather than
-- '>>='. The 'return' of every monad is singleton (it is not known if
-- there exists a monad on lists with a different return).
--
-- * For readability, code snippets in this documentation assume the
-- @OverloadedLists@ and @OverloadedStrings@ language extensions,
-- which make it possible to omit some @newtype@ constructors. Example
-- definitions of joins of monads always skip the @newtype@
-- constructors, that is, assume '>>=' is always defined as follows
-- for a particular local @join@:
--
-- @
-- m '>>=' f = 'wrap' $ join $ 'map' ('unwrap' . f) $ 'unwrap' m
--  where
--   join = ...
-- @
--
-- * The definitions of monads are optimized for readability and not
-- run-time performance. This is because the monads in this module
-- don't seem to be of any practical use, they are more of a
-- theoretical curiosity.
--
-- __References:__
--
-- Most of the monads defined in this module have been introduced in
-- the following papers (although there are some new specimens as
-- well):
-- 
-- * [Degrading Lists](https://raw.githubusercontent.com/maciejpirog/exotic-list-monads/master/degrading-lists.pdf)
-- by Dylan McDermott, Maciej Piróg, Tarmo Uustalu (PPDP 2020),
-- 
-- * [Counting Monads on Lists](https://cla.tcs.uj.edu.pl/pdfs/McDermott-Pirog-Uustalu-Abstract.pdf)
-- by Dylan McDermott, Maciej Piróg, Tarmo Uustalu (CLA 2023),
--
-- * [Hybrid Programs](http://alfa.di.uminho.pt/~nevrenato/pdfs/thesis.pdf) by Renato Neves (PhD Thesis, 2018).
module Control.Monad.List.Exotic
  (
  -- * List monads in general

    ListMonad(wrap, unwrap)
  , DualListMonad(..)
  , isSingle

  -- * Monads with finite presentation

  -- $finite_presentation
  
  -- ** Pointed magmas

  , PointedMagma(..)
  , FreeRBPM(..)

  -- ** The Global Failure monad
  
  , ZeroSemigroup
  , GlobalFailure(..)

  -- ** The Maze Walk monad

  , PalindromeAlgebra
  , palindromize
  , MazeWalk(..)
  
  -- ** The Discrete Hybrid monad

  , LeaningAlgebra
  , safeLast
  , DiscreteHybrid(..)
    
  -- ** The List Unfold monad
    
  , SkewedAlgebra
  , ListUnfold(..)

  -- ** The Stutter monad

  , StutterAlgebra
  , replicateLast
  , Stutter(..)

  -- ** The Stutter-Keeper monad  

  , StutterKeeperAlgebra
  , StutterKeeper(..)
  
  -- ** The Stutter-Stutter monad

  , StutterStutterAlgebra
  , StutterStutter(..)

  -- * Monads from numerical monoids

  -- $numerical_monoids
  
  -- ** The Mini monad

  , Mini(..)
  
  -- ** The Odd monad

  , Odd(..)

  -- ** The At Least monad

  , AtLeast(..)

  -- ** The Numerical Monoid monad

  , NumericalMonoidGenerators(..)
  , NumericalMonoidMonad(..)
  
  -- * Other list monads

  -- ** The At Most monad

  , AtMost(..)

  -- ** The Continuum-of-Monads monad

  -- $continuum-monads

  , SetOfNats(..)
  , ContinuumOfMonads(..)
  
  -- ** The Short Stutter-Keeper monad (?)

  , ShortStutterKeeper(..)

  ) where

import Prelude hiding ((<>))
import Control.Monad (ap, join)
import GHC.Exts (IsList(..), IsString(..), Constraint)
import GHC.TypeLits
import Data.Proxy
import qualified Data.Monoid (Monoid)

----------------------------
-- List monads in general --
----------------------------

-- | In this module, a \"list monad\" is a monad in which the
-- underlying functor is isomorphic to List. We require:
--
-- @
-- wrap . unwrap  ==  id
-- unwrap . wrap  ==  id
-- @
--
-- There is a default implementation provided if @m@ is known to be a
-- list (meaning @m a@ is an instance of 'GHC.Exts.IsList' for all
-- @a@).
class (Monad m) => ListMonad m where

  wrap   :: [a] -> m a
  default wrap   :: (IsList (m a), Item (m a) ~ a) => [a] -> m a
  wrap = forall l. IsList l => [Item l] -> l
fromList
  
  unwrap :: m a -> [a]
  default unwrap :: (IsList (m a), Item (m a) ~ a) => m a -> [a]
  unwrap = forall l. IsList l => l -> [Item l]
toList

instance ListMonad []

liftListFun :: (ListMonad m) => ([a] -> [a]) -> m a -> m a
liftListFun :: forall (m :: * -> *) a. ListMonad m => ([a] -> [a]) -> m a -> m a
liftListFun [a] -> [a]
f = forall (m :: * -> *) a. ListMonad m => [a] -> m a
wrap forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [a]
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. ListMonad m => m a -> [a]
unwrap

-- | Every list monad has a dual, in which join is defined as
--
-- @
-- join . reverse . fmap reverse
-- @
--
-- (where join is the join of the original list monad), while return is
--
-- @
-- reverse . return
-- @
--
-- (where return is the return of the original list monad).
newtype DualListMonad m a = DualListMonad { forall {k} (m :: k -> *) (a :: k). DualListMonad m a -> m a
unDualListMonad :: m a }
 deriving (forall a b. a -> DualListMonad m b -> DualListMonad m a
forall a b. (a -> b) -> DualListMonad m a -> DualListMonad m b
forall (m :: * -> *) a b.
Functor m =>
a -> DualListMonad m b -> DualListMonad m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> DualListMonad m a -> DualListMonad m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> DualListMonad m b -> DualListMonad m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> DualListMonad m b -> DualListMonad m a
fmap :: forall a b. (a -> b) -> DualListMonad m a -> DualListMonad m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> DualListMonad m a -> DualListMonad m b
Functor)

instance (ListMonad m) => Applicative (DualListMonad m) where
  pure :: forall a. a -> DualListMonad m a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b.
DualListMonad m (a -> b) -> DualListMonad m a -> DualListMonad m b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (ListMonad m) => Monad (DualListMonad m) where
  return :: forall a. a -> DualListMonad m a
return = forall {k} (m :: k -> *) (a :: k). m a -> DualListMonad m a
DualListMonad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. ListMonad m => ([a] -> [a]) -> m a -> m a
liftListFun forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return
  DualListMonad m a
m >>= :: forall a b.
DualListMonad m a -> (a -> DualListMonad m b) -> DualListMonad m b
>>= a -> DualListMonad m b
f = forall {k} (m :: k -> *) (a :: k). m a -> DualListMonad m a
DualListMonad forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. ListMonad m => ([a] -> [a]) -> m a -> m a
liftListFun forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) a. ListMonad m => ([a] -> [a]) -> m a -> m a
liftListFun forall a. [a] -> [a]
reverse m a
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. ListMonad m => ([a] -> [a]) -> m a -> m a
liftListFun forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (m :: k -> *) (a :: k). DualListMonad m a -> m a
unDualListMonad forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> DualListMonad m b
f

instance (ListMonad m, IsList (m a)) => IsList (DualListMonad m a) where
  type Item (DualListMonad m a) = Item (m a)
  toList :: DualListMonad m a -> [Item (DualListMonad m a)]
toList (DualListMonad m a
m) = forall l. IsList l => l -> [Item l]
toList m a
m
  fromList :: [Item (DualListMonad m a)] -> DualListMonad m a
fromList [Item (DualListMonad m a)]
xs = forall {k} (m :: k -> *) (a :: k). m a -> DualListMonad m a
DualListMonad (forall l. IsList l => [Item l] -> l
fromList [Item (DualListMonad m a)]
xs)

instance (ListMonad m) => ListMonad (DualListMonad m) where
  wrap :: forall a. [a] -> DualListMonad m a
wrap   = forall {k} (m :: k -> *) (a :: k). m a -> DualListMonad m a
DualListMonad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. ListMonad m => [a] -> m a
wrap
  unwrap :: forall a. DualListMonad m a -> [a]
unwrap = forall (m :: * -> *) a. ListMonad m => m a -> [a]
unwrap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (m :: k -> *) (a :: k). DualListMonad m a -> m a
unDualListMonad 

-- | Checks if a given list is a singleton (= list of length one).
isSingle :: [a] -> Bool
isSingle :: forall a. [a] -> Bool
isSingle [a
_] = Bool
True
isSingle [a]
_   = Bool
False

-- $finite_presentation
--
-- This section contains monads that come about from free algebras of
-- theories with a finite number of operations, represented as type
-- classes. Coincidentally, all theories in this module have one
-- binary and one nullary operation, that is, each is a subclass of
-- "PointedMagma" with additional laws. (So does the usual list monad,
-- where the subclass is monoid.) It is not known if there exists a
-- list monad that has a finite presentation but necessarily with a
-- different set of operations (there are such monads on non-empty
-- lists, for example, 'Control.Monad.List.NonEmpty.Exotic.HeadTails'
-- and 'Control.Monad.List.NonEmpty.Exotic.HeadsTail').

---------------------
-- Pointed magamas --
---------------------

-- | Pointed magmas are structures with one binary operation and one
-- constant. In general, no laws are imposed.
class PointedMagma a where
  eps  :: a
  (<>) :: a -> a -> a

instance PointedMagma [a] where
  eps :: [a]
eps  = []
  <> :: [a] -> [a] -> [a]
(<>) = forall a. [a] -> [a] -> [a]
(++)

-- | A class for __free right-braketed__ (subclasses of)
-- __pointed magmas__.
--
-- Most of the monads defined in this module arise from subclasses of
-- 'PointedMagma', in which we do not assume any additional methods,
-- but require the instances to satisfy additional equations. This
-- means that the monad is not only an instance of such a class that
-- defines a type of algebra, but it is /free/ such algebra.
--
-- In particular, we consider theories @c@ in which the equations have
-- the following shapes:
--
-- @
-- x '<>' 'eps'       ==  ...
-- 'eps' '<>' x       ==  ...
-- (x '<>' y) '<>' z  ==  ...
-- @
--
-- Moreover, when read left-to-right, they form a terminating and
-- confluent rewriting system with normal forms of the following
-- shape:
--
-- @
-- 'eps'
-- x '<>' (y '<>' ( ... (z '<>' t) ... ))
-- @
--
-- This class offers a witness that a particular list monad @m@ is a free algebra of
-- the theory @c@. This gives us the function
--
-- @
-- foldRBPM _ ('unwrap' -> []) = 'eps'
-- foldRBPM f ('unwrap' -> xs) = 'foldr1' ('<>') ('map' f xs)
-- @
--
-- which is the unique lifting of an interpretation of generators to a
-- homomorphism (between algebras of this sort) from the list monad to
-- any algebra (an instance) of @c@.
--
-- Note that the default definition of 'foldRBPM' is always the right
-- one for right-bracketed subclasses of 'PointedMagma', so it is
-- enough to declare the relationship, for example:
--
-- @
-- instance FreeRBPM [] 'Data.Monoid.Monoid'
-- @
class (ListMonad m) => FreeRBPM m (c :: * -> Constraint) | m -> c where
  foldRBPM :: (PointedMagma a, c a) => (x -> a) -> m x -> a
  foldRBPM x -> a
_ (forall (m :: * -> *) a. ListMonad m => m a -> [a]
unwrap -> []) = forall a. PointedMagma a => a
eps
  foldRBPM x -> a
f (forall (m :: * -> *) a. ListMonad m => m a -> [a]
unwrap -> [x]
xs) = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 forall a. PointedMagma a => a -> a -> a
(<>) (forall a b. (a -> b) -> [a] -> [b]
map x -> a
f [x]
xs)

instance FreeRBPM [] Data.Monoid.Monoid

------------------------------
-- The Global Failure monad --
------------------------------

-- | A zero semigroup has an associative binary operation and a
-- constant that is absorbing on both sides. That is, the following
-- equations hold:
--
-- @
-- x '<>' 'eps'       ==  'eps'
-- 'eps' '<>' x       ==  'eps'
-- (x '<>' y) '<>' z  ==  x '<>' (y '<>' z)
-- @
class (PointedMagma a) => ZeroSemigroup a

-- | The Global Failure monad arises from free zero semigroups. It
-- implements a kind of nondeterminism similar to the usual List
-- monad, but failing (= producing an empty list) in one branch makes
-- the entire computation fail.  Its join is defined as:
--
-- @
-- join xss | any null xss = []
--          | otherwise    = concat xss
-- @
--
-- For example:
--
-- >>> [1, 2, 3] >>= (\n -> [1..n]) :: GlobalFailure Int
-- GlobalFailure [1,1,2,1,2,3]
-- >>> [1, 0, 3] >>= (\n -> [1..n]) :: GlobalFailure Int
-- GlobalFailure []
newtype GlobalFailure a = GlobalFailure { forall a. GlobalFailure a -> [a]
unGlobalFailure :: [a] }
 deriving (forall a b. a -> GlobalFailure b -> GlobalFailure a
forall a b. (a -> b) -> GlobalFailure a -> GlobalFailure b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> GlobalFailure b -> GlobalFailure a
$c<$ :: forall a b. a -> GlobalFailure b -> GlobalFailure a
fmap :: forall a b. (a -> b) -> GlobalFailure a -> GlobalFailure b
$cfmap :: forall a b. (a -> b) -> GlobalFailure a -> GlobalFailure b
Functor, Int -> GlobalFailure a -> ShowS
forall a. Show a => Int -> GlobalFailure a -> ShowS
forall a. Show a => [GlobalFailure a] -> ShowS
forall a. Show a => GlobalFailure a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GlobalFailure a] -> ShowS
$cshowList :: forall a. Show a => [GlobalFailure a] -> ShowS
show :: GlobalFailure a -> String
$cshow :: forall a. Show a => GlobalFailure a -> String
showsPrec :: Int -> GlobalFailure a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> GlobalFailure a -> ShowS
Show, GlobalFailure a -> GlobalFailure a -> Bool
forall a. Eq a => GlobalFailure a -> GlobalFailure a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GlobalFailure a -> GlobalFailure a -> Bool
$c/= :: forall a. Eq a => GlobalFailure a -> GlobalFailure a -> Bool
== :: GlobalFailure a -> GlobalFailure a -> Bool
$c== :: forall a. Eq a => GlobalFailure a -> GlobalFailure a -> Bool
Eq)

deriving instance IsString (GlobalFailure Char)

instance Applicative GlobalFailure where
  pure :: forall a. a -> GlobalFailure a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b.
GlobalFailure (a -> b) -> GlobalFailure a -> GlobalFailure b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad GlobalFailure where
  return :: forall a. a -> GlobalFailure a
return a
x = forall a. [a] -> GlobalFailure a
GlobalFailure [a
x]
  GlobalFailure [a]
xs >>= :: forall a b.
GlobalFailure a -> (a -> GlobalFailure b) -> GlobalFailure b
>>= a -> GlobalFailure b
f = forall a. [a] -> GlobalFailure a
GlobalFailure forall a b. (a -> b) -> a -> b
$ forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
join forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. GlobalFailure a -> [a]
unGlobalFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> GlobalFailure b
f) [a]
xs 
   where
    join :: t [a] -> [a]
join t [a]
xss | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall (t :: * -> *) a. Foldable t => t a -> Bool
null t [a]
xss = []
             | Bool
otherwise    = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat t [a]
xss

instance IsList (GlobalFailure a) where
  type Item (GlobalFailure a) = a
  toList :: GlobalFailure a -> [Item (GlobalFailure a)]
toList   = forall a. GlobalFailure a -> [a]
unGlobalFailure
  fromList :: [Item (GlobalFailure a)] -> GlobalFailure a
fromList = forall a. [a] -> GlobalFailure a
GlobalFailure

instance ListMonad GlobalFailure

instance PointedMagma (GlobalFailure a) where
  GlobalFailure a
m <> :: GlobalFailure a -> GlobalFailure a -> GlobalFailure a
<> GlobalFailure a
t = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall a. [a] -> GlobalFailure a
GlobalFailure forall a b. (a -> b) -> a -> b
$ [GlobalFailure a
m, GlobalFailure a
t]
  eps :: GlobalFailure a
eps    = forall a. [a] -> GlobalFailure a
GlobalFailure []

instance ZeroSemigroup (GlobalFailure a)

instance FreeRBPM GlobalFailure ZeroSemigroup

-------------------------
-- The Maze Walk monad --
-------------------------

-- | A palindrome algebra is a pointed magma that satisfies the
-- following equations:
--
-- @
-- x '<>' 'eps'       ==  'eps'
-- 'eps' '<>' x       ==  'eps'
-- (x '<>' y) '<>' z  ==  x '<>' (y '<>' (x '<>' z))
-- @
class (PointedMagma a) => PalindromeAlgebra a

-- | Turns a list into a palindrome by appending it and its reversed
-- init. For example:
--
-- @
-- palindromize []       ==  []
-- palindromize \"Ringo\"  ==  \"RingogniR\"
-- @
palindromize :: [a] -> [a]
palindromize :: forall a. [a] -> [a]
palindromize [] = []
palindromize [a]
xs = [a]
xs forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [a]
reverse (forall a. [a] -> [a]
init [a]
xs)

-- | The Maze Walk monad arises from free palindrome algebras. Its
-- join is defined as:
--
-- @
-- join xss | null xss     = []
--          | any null xss = []
--          | otherwise    = concatMap palindromize (init xss) ++ last xss
-- @
--
-- Intuitively, it is a list of values one encounters when walking a
-- path in a maze.  The bind operation attaches to each value a new
-- "corridor" to visit.  In our walk we explore every such
-- corridor. For example, consider the following expression:
--
-- >>> join ["John", "Paul", "George", "Ringo"] :: MazeWalk Char
-- MazeWalk "JohnhoJPauluaPGeorgegroeGRingo"
--
-- It represents a walk through the following maze (the entrance is
-- marked with \">\"):
--
-- @
--   ┌────┬──────┐
--   │L U │ N G O│
--   ├─┤A ┴ I┌───┘
--  > J P G R│
-- ┌─┘O ┬ E ┌┘
-- │N H │ O └──┐
-- └────┤ R G E│
--      └──────┘
-- @
--
-- First, we take the J-O-H-N path. When we reach its end, we turn
-- around and go back to J, so our walk to this point is J-O-H-N-H-O-J
-- (hence the connection with palindromes).  Then, we explore the
-- P-A-U-L corridor, adding P-A-U-L-U-A-P to our walk. The same
-- applies to G-E-O-R-G-E. But when at the end of R-I-N-G-O, we have
-- explored the entire maze, so our walk is done (this is why we do
-- not palindromize the last element).
--
newtype MazeWalk a = MazeWalk { forall a. MazeWalk a -> [a]
unMazeWalk :: [a] }
 deriving (forall a b. a -> MazeWalk b -> MazeWalk a
forall a b. (a -> b) -> MazeWalk a -> MazeWalk b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> MazeWalk b -> MazeWalk a
$c<$ :: forall a b. a -> MazeWalk b -> MazeWalk a
fmap :: forall a b. (a -> b) -> MazeWalk a -> MazeWalk b
$cfmap :: forall a b. (a -> b) -> MazeWalk a -> MazeWalk b
Functor, Int -> MazeWalk a -> ShowS
forall a. Show a => Int -> MazeWalk a -> ShowS
forall a. Show a => [MazeWalk a] -> ShowS
forall a. Show a => MazeWalk a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MazeWalk a] -> ShowS
$cshowList :: forall a. Show a => [MazeWalk a] -> ShowS
show :: MazeWalk a -> String
$cshow :: forall a. Show a => MazeWalk a -> String
showsPrec :: Int -> MazeWalk a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> MazeWalk a -> ShowS
Show, MazeWalk a -> MazeWalk a -> Bool
forall a. Eq a => MazeWalk a -> MazeWalk a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MazeWalk a -> MazeWalk a -> Bool
$c/= :: forall a. Eq a => MazeWalk a -> MazeWalk a -> Bool
== :: MazeWalk a -> MazeWalk a -> Bool
$c== :: forall a. Eq a => MazeWalk a -> MazeWalk a -> Bool
Eq)

deriving instance IsString (MazeWalk Char)

instance Applicative MazeWalk where
  pure :: forall a. a -> MazeWalk a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b. MazeWalk (a -> b) -> MazeWalk a -> MazeWalk b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad MazeWalk where
  return :: forall a. a -> MazeWalk a
return a
x = forall a. [a] -> MazeWalk a
MazeWalk [a
x]
  MazeWalk [a]
xs >>= :: forall a b. MazeWalk a -> (a -> MazeWalk b) -> MazeWalk b
>>= a -> MazeWalk b
f = forall a. [a] -> MazeWalk a
MazeWalk forall a b. (a -> b) -> a -> b
$ forall {a}. [[a]] -> [a]
join forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. MazeWalk a -> [a]
unMazeWalk forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> MazeWalk b
f) [a]
xs 
   where
    join :: [[a]] -> [a]
join [[a]]
xss | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[a]]
xss Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[a]]
xss
             = []
             | Bool
otherwise
             = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a. [a] -> [a]
palindromize (forall a. [a] -> [a]
init [[a]]
xss) forall a. [a] -> [a] -> [a]
++ forall a. [a] -> a
last [[a]]
xss

instance IsList (MazeWalk a) where
  type Item (MazeWalk a) = a
  toList :: MazeWalk a -> [Item (MazeWalk a)]
toList   = forall a. MazeWalk a -> [a]
unMazeWalk
  fromList :: [Item (MazeWalk a)] -> MazeWalk a
fromList = forall a. [a] -> MazeWalk a
MazeWalk
  
instance ListMonad MazeWalk

instance PointedMagma (MazeWalk a) where
  MazeWalk a
m <> :: MazeWalk a -> MazeWalk a -> MazeWalk a
<> MazeWalk a
t = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall a. [a] -> MazeWalk a
MazeWalk forall a b. (a -> b) -> a -> b
$ [MazeWalk a
m, MazeWalk a
t]
  eps :: MazeWalk a
eps    = forall a. [a] -> MazeWalk a
MazeWalk []

instance PalindromeAlgebra (MazeWalk a)

instance FreeRBPM MazeWalk PalindromeAlgebra

-------------------------------
-- The Discrete Hybrid monad --
-------------------------------

-- | Instances should satisfy the following:
--
-- @
-- x '<>' 'eps'       ==  'eps'
-- 'eps' '<>' x       ==  x
-- (x '<>' y) '<>' z  ==  y '<>' z
-- @
class (PointedMagma a) => LeaningAlgebra a

-- | A singleton list with the last element of the argument,
-- if it exists. Otherwise, empty.
--
-- @
-- safeLast \"Roy\"  ==  \"y\"
-- safeLast []     ==  []
-- @
safeLast :: [a] -> [a]
safeLast :: forall a. [a] -> [a]
safeLast [] = []
safeLast [a]
xs = [forall a. [a] -> a
last [a]
xs]

-- | The Discrete Hybrid monad arises from free leaning algebras. Its
-- join is defined as:
--
-- @
-- join xss | null xss        = []
--          | null (last xss) = []
--          | otherwise       = concatMap safeLast (init xss) ++ last xss
-- @
--
-- For example:
--
-- >>> join ["Roy", "Kelton", "Orbison"] :: DiscreteHybrid Char
-- DiscreteHybrid "ynOrbison"
-- >>> join ["Roy", "", "Orbison"] :: DiscreteHybrid Char
-- DiscreteHybrid "yOrbison"
newtype DiscreteHybrid a = DiscreteHybrid { forall a. DiscreteHybrid a -> [a]
unDiscreteHybrid :: [a] }
 deriving (forall a b. a -> DiscreteHybrid b -> DiscreteHybrid a
forall a b. (a -> b) -> DiscreteHybrid a -> DiscreteHybrid b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> DiscreteHybrid b -> DiscreteHybrid a
$c<$ :: forall a b. a -> DiscreteHybrid b -> DiscreteHybrid a
fmap :: forall a b. (a -> b) -> DiscreteHybrid a -> DiscreteHybrid b
$cfmap :: forall a b. (a -> b) -> DiscreteHybrid a -> DiscreteHybrid b
Functor, Int -> DiscreteHybrid a -> ShowS
forall a. Show a => Int -> DiscreteHybrid a -> ShowS
forall a. Show a => [DiscreteHybrid a] -> ShowS
forall a. Show a => DiscreteHybrid a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DiscreteHybrid a] -> ShowS
$cshowList :: forall a. Show a => [DiscreteHybrid a] -> ShowS
show :: DiscreteHybrid a -> String
$cshow :: forall a. Show a => DiscreteHybrid a -> String
showsPrec :: Int -> DiscreteHybrid a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> DiscreteHybrid a -> ShowS
Show, DiscreteHybrid a -> DiscreteHybrid a -> Bool
forall a. Eq a => DiscreteHybrid a -> DiscreteHybrid a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DiscreteHybrid a -> DiscreteHybrid a -> Bool
$c/= :: forall a. Eq a => DiscreteHybrid a -> DiscreteHybrid a -> Bool
== :: DiscreteHybrid a -> DiscreteHybrid a -> Bool
$c== :: forall a. Eq a => DiscreteHybrid a -> DiscreteHybrid a -> Bool
Eq)

deriving instance IsString (DiscreteHybrid Char)

instance Applicative DiscreteHybrid where
  pure :: forall a. a -> DiscreteHybrid a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b.
DiscreteHybrid (a -> b) -> DiscreteHybrid a -> DiscreteHybrid b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad DiscreteHybrid where
  return :: forall a. a -> DiscreteHybrid a
return a
x = forall a. [a] -> DiscreteHybrid a
DiscreteHybrid [a
x]
  DiscreteHybrid [a]
xs >>= :: forall a b.
DiscreteHybrid a -> (a -> DiscreteHybrid b) -> DiscreteHybrid b
>>= a -> DiscreteHybrid b
f = forall a. [a] -> DiscreteHybrid a
DiscreteHybrid forall a b. (a -> b) -> a -> b
$ forall {a}. [[a]] -> [a]
join forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. DiscreteHybrid a -> [a]
unDiscreteHybrid forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> DiscreteHybrid b
f) [a]
xs 
   where
    join :: [[a]] -> [a]
join [[a]]
xss | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[a]]
xss        = []
             | forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a. [a] -> a
last [[a]]
xss) = []
             | Bool
otherwise       = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a. [a] -> [a]
safeLast (forall a. [a] -> [a]
init [[a]]
xss) forall a. [a] -> [a] -> [a]
++ forall a. [a] -> a
last [[a]]
xss

instance IsList (DiscreteHybrid a) where
  type Item (DiscreteHybrid a) = a
  toList :: DiscreteHybrid a -> [Item (DiscreteHybrid a)]
toList   = forall a. DiscreteHybrid a -> [a]
unDiscreteHybrid
  fromList :: [Item (DiscreteHybrid a)] -> DiscreteHybrid a
fromList = forall a. [a] -> DiscreteHybrid a
DiscreteHybrid
  
instance ListMonad DiscreteHybrid

instance PointedMagma (DiscreteHybrid a) where
  DiscreteHybrid a
m <> :: DiscreteHybrid a -> DiscreteHybrid a -> DiscreteHybrid a
<> DiscreteHybrid a
t = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall a. [a] -> DiscreteHybrid a
DiscreteHybrid forall a b. (a -> b) -> a -> b
$ [DiscreteHybrid a
m, DiscreteHybrid a
t]
  eps :: DiscreteHybrid a
eps    = forall a. [a] -> DiscreteHybrid a
DiscreteHybrid []

instance LeaningAlgebra (DiscreteHybrid a)

instance FreeRBPM DiscreteHybrid LeaningAlgebra

---------------------------
-- The List Unfold monad --
---------------------------

-- | A skewed algebra allows only right-nested composition of the
-- binary operation. Every other expression is equal to 'eps'.
--
-- @
-- x '<>' 'eps'       ==  'eps'
-- 'eps' '<>' x       ==  'eps'
-- (x '<>' y) '<>' z  ==  'eps'
-- @
class (PointedMagma a) => SkewedAlgebra a

-- | The List Unfold monad arises from free skewed algebras. It
-- implements a form of nondeterminism similar to the usual list
-- monad, but new choices may arise only in the last element (so the
-- bind operation can only rename other elements), essentially
-- unfolding a list. If new choices arise in the "init" of the list,
-- the entire computation fails. Also, failure is always global. The
-- join operation is defined as follows:
--
-- @
-- join xss | null xss                        = []
--          | any null xss                    = []
--          | any (not . isSingle) (init xss) = []
--          | otherwise                       = concat xss
-- @
--
-- For example:
--
-- >>> [1,1,1,4] >>= \x -> [1..x] :: ListUnfold Int
-- ListUnfold [1,1,1,1,2,3,4]
-- >>> [1,2,1,4] >>= \x -> [1..x] :: ListUnfold Int
-- ListUnfold []
-- >>> [1,0,1,4] >>= \x -> [1..x] :: ListUnfold Int
-- ListUnfold []
newtype ListUnfold a = ListUnfold { forall a. ListUnfold a -> [a]
unListUnfold :: [a] }
 deriving (forall a b. a -> ListUnfold b -> ListUnfold a
forall a b. (a -> b) -> ListUnfold a -> ListUnfold b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> ListUnfold b -> ListUnfold a
$c<$ :: forall a b. a -> ListUnfold b -> ListUnfold a
fmap :: forall a b. (a -> b) -> ListUnfold a -> ListUnfold b
$cfmap :: forall a b. (a -> b) -> ListUnfold a -> ListUnfold b
Functor, Int -> ListUnfold a -> ShowS
forall a. Show a => Int -> ListUnfold a -> ShowS
forall a. Show a => [ListUnfold a] -> ShowS
forall a. Show a => ListUnfold a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ListUnfold a] -> ShowS
$cshowList :: forall a. Show a => [ListUnfold a] -> ShowS
show :: ListUnfold a -> String
$cshow :: forall a. Show a => ListUnfold a -> String
showsPrec :: Int -> ListUnfold a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> ListUnfold a -> ShowS
Show, ListUnfold a -> ListUnfold a -> Bool
forall a. Eq a => ListUnfold a -> ListUnfold a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ListUnfold a -> ListUnfold a -> Bool
$c/= :: forall a. Eq a => ListUnfold a -> ListUnfold a -> Bool
== :: ListUnfold a -> ListUnfold a -> Bool
$c== :: forall a. Eq a => ListUnfold a -> ListUnfold a -> Bool
Eq)

deriving instance IsString (ListUnfold Char)

instance Applicative ListUnfold where
  pure :: forall a. a -> ListUnfold a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b. ListUnfold (a -> b) -> ListUnfold a -> ListUnfold b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad ListUnfold where
  return :: forall a. a -> ListUnfold a
return a
x = forall a. [a] -> ListUnfold a
ListUnfold [a
x]
  ListUnfold [a]
xs >>= :: forall a b. ListUnfold a -> (a -> ListUnfold b) -> ListUnfold b
>>= a -> ListUnfold b
f = forall a. [a] -> ListUnfold a
ListUnfold forall a b. (a -> b) -> a -> b
$ forall {a}. [[a]] -> [a]
join forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. ListUnfold a -> [a]
unListUnfold forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ListUnfold b
f) [a]
xs 
   where
    join :: [[a]] -> [a]
join [[a]]
xss | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[a]]
xss Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[a]]
xss
             = []
             | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Bool
isSingle) (forall a. [a] -> [a]
init [[a]]
xss)
             = []
             | Bool
otherwise
             = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[a]]
xss

instance IsList (ListUnfold a) where
  type Item (ListUnfold a) = a
  toList :: ListUnfold a -> [Item (ListUnfold a)]
toList   = forall a. ListUnfold a -> [a]
unListUnfold
  fromList :: [Item (ListUnfold a)] -> ListUnfold a
fromList = forall a. [a] -> ListUnfold a
ListUnfold
  
instance ListMonad ListUnfold

instance PointedMagma (ListUnfold a) where
  ListUnfold a
m <> :: ListUnfold a -> ListUnfold a -> ListUnfold a
<> ListUnfold a
t = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall a. [a] -> ListUnfold a
ListUnfold forall a b. (a -> b) -> a -> b
$ [ListUnfold a
m, ListUnfold a
t]
  eps :: ListUnfold a
eps    = forall a. [a] -> ListUnfold a
ListUnfold []

instance SkewedAlgebra (ListUnfold a)

instance FreeRBPM ListUnfold SkewedAlgebra

-----------------------
-- The Stutter monad --
-----------------------

-- | A stutter algebra (for a given natural number @n@) is a pointed
-- magma that satisfies the following equations:
--
-- @
-- x '<>' 'eps'       ==  'foldr1' ('<>') ('replicate' (n + 2) x)
-- 'eps' '<>' x       ==  'eps'  
-- (x '<>' y) '<>' z  ==  'eps'
-- @
class (KnownNat n, PointedMagma a) => StutterAlgebra n a

-- | Repeat the last element on the list @n@ additional times, that is:
--
-- @
-- replicateLast n [] = []
-- replicateLast n xs = xs ++ replicate n (last xs)
-- @
replicateLast :: Int -> [a] -> [a]
replicateLast :: forall a. Int -> [a] -> [a]
replicateLast Int
_ [] = []
replicateLast Int
n [a]
xs = [a]
xs forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate Int
n (forall a. [a] -> a
last [a]
xs)

-- | The Stutter monad arises from free stutter algebras. Its join is
-- a concat of the longest prefix consisting only of singletons with a
-- \"stutter\" on the last singleton (that is, the last singleton is
-- additionally repeated @n+1@ times for an @n@ fixed in the type). It
-- doesn't stutter only when the init consists only of singletons and
-- the last list is non-empty. The join can thus be defined as follows
-- (omitting the conversion of the type-level 'Nat' @n@ to a run-time
-- value):
--
-- @
-- join xss | null xss
--          = []
--          | any (not . isSingle) (init xss) || null (last xss)
--          = replicateLast (n + 1) (concat $ takeWhile isSingle (init xss))
--          | otherwise
--          = concat xss
-- @
--
-- The 'Stutter' monad is quite similar to 'ListUnfold'. The
-- difference is that when the latter fails (that is, its join results
-- in an empty list), the former stutters on the last singleton.
--
-- Examples:
--
-- >>> join ["1", "2", "buckle", "my", "shoe"] :: Stutter 5 Char
-- Stutter "12222222"
-- >>> join ["1", "2", "buckle"] :: Stutter 5 Char
-- Stutter "12buckle"
-- >>> join ["1", "2", "", "my", "shoe"] :: Stutter 5 Char
-- Stutter "12222222"
newtype Stutter (n :: Nat) a = Stutter { forall (n :: Nat) a. Stutter n a -> [a]
unStutter :: [a] }
 deriving (forall (n :: Nat) a b. a -> Stutter n b -> Stutter n a
forall (n :: Nat) a b. (a -> b) -> Stutter n a -> Stutter n b
forall a b. a -> Stutter n b -> Stutter n a
forall a b. (a -> b) -> Stutter n a -> Stutter n b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Stutter n b -> Stutter n a
$c<$ :: forall (n :: Nat) a b. a -> Stutter n b -> Stutter n a
fmap :: forall a b. (a -> b) -> Stutter n a -> Stutter n b
$cfmap :: forall (n :: Nat) a b. (a -> b) -> Stutter n a -> Stutter n b
Functor, Int -> Stutter n a -> ShowS
forall (n :: Nat) a. Show a => Int -> Stutter n a -> ShowS
forall (n :: Nat) a. Show a => [Stutter n a] -> ShowS
forall (n :: Nat) a. Show a => Stutter n a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Stutter n a] -> ShowS
$cshowList :: forall (n :: Nat) a. Show a => [Stutter n a] -> ShowS
show :: Stutter n a -> String
$cshow :: forall (n :: Nat) a. Show a => Stutter n a -> String
showsPrec :: Int -> Stutter n a -> ShowS
$cshowsPrec :: forall (n :: Nat) a. Show a => Int -> Stutter n a -> ShowS
Show, Stutter n a -> Stutter n a -> Bool
forall (n :: Nat) a. Eq a => Stutter n a -> Stutter n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Stutter n a -> Stutter n a -> Bool
$c/= :: forall (n :: Nat) a. Eq a => Stutter n a -> Stutter n a -> Bool
== :: Stutter n a -> Stutter n a -> Bool
$c== :: forall (n :: Nat) a. Eq a => Stutter n a -> Stutter n a -> Bool
Eq)

deriving instance (KnownNat n) => IsString (Stutter n Char)

instance (KnownNat n) => Applicative (Stutter n) where
  pure :: forall a. a -> Stutter n a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b. Stutter n (a -> b) -> Stutter n a -> Stutter n b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (KnownNat n) => Monad (Stutter n) where
  return :: forall a. a -> Stutter n a
return a
x = forall (n :: Nat) a. [a] -> Stutter n a
Stutter [a
x]
  Stutter [a]
xs >>= :: forall a b. Stutter n a -> (a -> Stutter n b) -> Stutter n b
>>= a -> Stutter n b
f = forall (n :: Nat) a. [a] -> Stutter n a
Stutter forall a b. (a -> b) -> a -> b
$ [[b]] -> [b]
join forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (n :: Nat) a. Stutter n a -> [a]
unStutter forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Stutter n b
f) [a]
xs
   where
    join :: [[b]] -> [b]
join [[b]]
xss | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[b]]
xss
             = []
             | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Bool
isSingle) (forall a. [a] -> [a]
init [[b]]
xss) Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a. [a] -> a
last [[b]]
xss)
             = let n :: Int
n = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
               in  forall a. Int -> [a] -> [a]
replicateLast (Int
n forall a. Num a => a -> a -> a
+ Int
1) (forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
takeWhile forall a. [a] -> Bool
isSingle (forall a. [a] -> [a]
init [[b]]
xss))
             | Bool
otherwise
             = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[b]]
xss

instance (KnownNat n) => IsList (Stutter n a) where
  type Item (Stutter n a) = a
  toList :: Stutter n a -> [Item (Stutter n a)]
toList   = forall (n :: Nat) a. Stutter n a -> [a]
unStutter
  fromList :: [Item (Stutter n a)] -> Stutter n a
fromList = forall (n :: Nat) a. [a] -> Stutter n a
Stutter 

instance (KnownNat n) => ListMonad (Stutter n) 

instance (KnownNat n) => PointedMagma (Stutter n a) where
  Stutter n a
m <> :: Stutter n a -> Stutter n a -> Stutter n a
<> Stutter n a
t = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) a. [a] -> Stutter n a
Stutter forall a b. (a -> b) -> a -> b
$ [Stutter n a
m, Stutter n a
t]
  eps :: Stutter n a
eps    = forall (n :: Nat) a. [a] -> Stutter n a
Stutter []

instance (KnownNat n) => StutterAlgebra n (Stutter n a)

instance (KnownNat n) => FreeRBPM (Stutter n) (StutterAlgebra n)

------------------------------
-- The Stutter-Keeper monad --
------------------------------

-- | A stutter-keeper algebra (for a given natural number @n@) is a pointed
-- magma that satisfies the following equations:
--
-- @
-- x '<>' 'eps'       ==  'foldr1' ('<>') ('replicate' (n + 2) x)
-- 'eps' '<>' x       ==  'eps'  
-- (x '<>' y) '<>' z  ==  x '<>' y
-- @
class (KnownNat n, PointedMagma a) => StutterKeeperAlgebra n a

-- | The stutter-keeper monad arises from free stutter-keeper
-- algebras. Its join stutters (as in the 'Stutter' monad) if the
-- first non-singleton list in empty. Otherwise, it keeps the
-- singleton prefix, and keeps the first non-singleton list. The join
-- can thus be defined as follows (omitting the conversion of the
-- type-level 'Nat' @n@ to a run-time value):
--
-- @
-- join xss | null xss
--          = []
--          | null (head (dropWhile isSingle (init xss) ++ [last xss]))
--          = replicateLast (n + 1) (concat $ takeWhile isSingle (init xss))
--          | otherwise
--          = map head (takeWhile isSingle (init xss))
--             ++ head (dropWhile isSingle (init xss) ++ [last xss])
-- @
--
-- Examples:
--
-- >>> join ["1", "2", "buckle", "my", "shoe"] :: StutterKeeper 5 Char
  -- StutterKeeper "12buckle"
-- >>> join ["1", "2", "buckle"] :: StutterKeeper 5 Char
-- StutterKeeper "12buckle"
-- >>> join ["1", "2", "", "my", "shoe"] :: StutterKeeper 5 Char
-- StutterKeeper "12222222"
newtype StutterKeeper (n :: Nat) a = StutterKeeper { forall (n :: Nat) a. StutterKeeper n a -> [a]
unStutterKeeper :: [a] }
 deriving (forall (n :: Nat) a b. a -> StutterKeeper n b -> StutterKeeper n a
forall (n :: Nat) a b.
(a -> b) -> StutterKeeper n a -> StutterKeeper n b
forall a b. a -> StutterKeeper n b -> StutterKeeper n a
forall a b. (a -> b) -> StutterKeeper n a -> StutterKeeper n b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> StutterKeeper n b -> StutterKeeper n a
$c<$ :: forall (n :: Nat) a b. a -> StutterKeeper n b -> StutterKeeper n a
fmap :: forall a b. (a -> b) -> StutterKeeper n a -> StutterKeeper n b
$cfmap :: forall (n :: Nat) a b.
(a -> b) -> StutterKeeper n a -> StutterKeeper n b
Functor, Int -> StutterKeeper n a -> ShowS
forall (n :: Nat) a. Show a => Int -> StutterKeeper n a -> ShowS
forall (n :: Nat) a. Show a => [StutterKeeper n a] -> ShowS
forall (n :: Nat) a. Show a => StutterKeeper n a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [StutterKeeper n a] -> ShowS
$cshowList :: forall (n :: Nat) a. Show a => [StutterKeeper n a] -> ShowS
show :: StutterKeeper n a -> String
$cshow :: forall (n :: Nat) a. Show a => StutterKeeper n a -> String
showsPrec :: Int -> StutterKeeper n a -> ShowS
$cshowsPrec :: forall (n :: Nat) a. Show a => Int -> StutterKeeper n a -> ShowS
Show, StutterKeeper n a -> StutterKeeper n a -> Bool
forall (n :: Nat) a.
Eq a =>
StutterKeeper n a -> StutterKeeper n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StutterKeeper n a -> StutterKeeper n a -> Bool
$c/= :: forall (n :: Nat) a.
Eq a =>
StutterKeeper n a -> StutterKeeper n a -> Bool
== :: StutterKeeper n a -> StutterKeeper n a -> Bool
$c== :: forall (n :: Nat) a.
Eq a =>
StutterKeeper n a -> StutterKeeper n a -> Bool
Eq)

deriving instance (KnownNat n) => IsString (StutterKeeper n Char)

instance (KnownNat n) => Applicative (StutterKeeper n) where
  pure :: forall a. a -> StutterKeeper n a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b.
StutterKeeper n (a -> b) -> StutterKeeper n a -> StutterKeeper n b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (KnownNat n) => Monad (StutterKeeper n) where
  return :: forall a. a -> StutterKeeper n a
return a
x = forall (n :: Nat) a. [a] -> StutterKeeper n a
StutterKeeper [a
x]
  StutterKeeper [a]
xs >>= :: forall a b.
StutterKeeper n a -> (a -> StutterKeeper n b) -> StutterKeeper n b
>>= a -> StutterKeeper n b
f = forall (n :: Nat) a. [a] -> StutterKeeper n a
StutterKeeper forall a b. (a -> b) -> a -> b
$ [[b]] -> [b]
join forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (n :: Nat) a. StutterKeeper n a -> [a]
unStutterKeeper forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> StutterKeeper n b
f) [a]
xs
   where
    join :: [[b]] -> [b]
join [[b]]
xss | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[b]]
xss
             = []
             | forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a. [a] -> a
head (forall a. (a -> Bool) -> [a] -> [a]
dropWhile forall a. [a] -> Bool
isSingle (forall a. [a] -> [a]
init [[b]]
xss) forall a. [a] -> [a] -> [a]
++ [forall a. [a] -> a
last [[b]]
xss]))
             = let n :: Int
n = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
               in  forall a. Int -> [a] -> [a]
replicateLast (Int
n forall a. Num a => a -> a -> a
+ Int
1) (forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
takeWhile forall a. [a] -> Bool
isSingle (forall a. [a] -> [a]
init [[b]]
xss))
             | Bool
otherwise
             = forall a b. (a -> b) -> [a] -> [b]
map forall a. [a] -> a
head (forall a. (a -> Bool) -> [a] -> [a]
takeWhile forall a. [a] -> Bool
isSingle (forall a. [a] -> [a]
init [[b]]
xss))
                forall a. [a] -> [a] -> [a]
++ forall a. [a] -> a
head (forall a. (a -> Bool) -> [a] -> [a]
dropWhile forall a. [a] -> Bool
isSingle (forall a. [a] -> [a]
init [[b]]
xss) forall a. [a] -> [a] -> [a]
++ [forall a. [a] -> a
last [[b]]
xss])

instance (KnownNat n) => IsList (StutterKeeper n a) where
  type Item (StutterKeeper n a) = a
  toList :: StutterKeeper n a -> [Item (StutterKeeper n a)]
toList   = forall (n :: Nat) a. StutterKeeper n a -> [a]
unStutterKeeper
  fromList :: [Item (StutterKeeper n a)] -> StutterKeeper n a
fromList = forall (n :: Nat) a. [a] -> StutterKeeper n a
StutterKeeper 

instance (KnownNat n) => ListMonad (StutterKeeper n) 

instance (KnownNat n) => PointedMagma (StutterKeeper n a) where
  StutterKeeper n a
m <> :: StutterKeeper n a -> StutterKeeper n a -> StutterKeeper n a
<> StutterKeeper n a
t = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) a. [a] -> StutterKeeper n a
StutterKeeper forall a b. (a -> b) -> a -> b
$ [StutterKeeper n a
m, StutterKeeper n a
t]
  eps :: StutterKeeper n a
eps    = forall (n :: Nat) a. [a] -> StutterKeeper n a
StutterKeeper []

instance (KnownNat n) => StutterKeeperAlgebra n (StutterKeeper n a)

instance (KnownNat n) => FreeRBPM (StutterKeeper n) (StutterKeeperAlgebra n)

------------------------------
-- The StutterStutter monad --
------------------------------

-- | A stutter-stutter algebra (for given natural numbers @n@ and @m@)
-- is a pointed magma that satisfies the following equations:
--
-- @
-- x '<>' 'eps'       ==  'foldr1' ('<>') ('replicate' (n + 2) x)
-- 'eps' '<>' x       ==  'eps'  
-- (x '<>' y) '<>' z  ==  'foldr1' ('<>') ('replicate' (m + 2) x)
-- @
class (KnownNat n, KnownNat m, PointedMagma a) => StutterStutterAlgebra n m a

-- | The stutter-stutter monad arises from free stutter-stutter
-- algebras. It is similar to 'StutterKeeper', but instead of keeping
-- the first non-singleton list, it stutters on its first element
-- (unless the first non-singleton list is also the last list, in
-- which case it is kept in the result). The join can thus be defined
-- as follows (omitting the conversion of the type-level nats to
-- run-time values):
--
-- @
-- join xss | null xss
--          = []
--          | null (head (dropWhile isSingle (init xss) ++ [last xss]))
--          = replicateLast (n + 1) (concat $ takeWhile isSingle (init xss))
--          | any (not . isSingle) (init xss) || null (last xss)
--          = concat (takeWhile isSingle (init xss))
--             ++ replicate (m + 2) (head (head (dropWhile isSingle (init xss))))
--          | otherwise
--          = concat xss
-- @
--
-- Examples:
--
-- >>> join ["1", "2", "buckle", "my", "shoe"] :: StutterStutter 5 10 Char
-- StutterStutter "12bbbbbbbbbbbb"
-- >>> join ["1", "2", "buckle"] :: StutterStutter 5 10 Char
-- StutterStutter "12buckle"
-- >>> join ["1", "2", "", "my", "shoe"] :: StutterStutter 5 10 Char
-- StutterStutter "12222222"
newtype StutterStutter (n :: Nat) (m :: Nat) a = StutterStutter { forall (n :: Nat) (m :: Nat) a. StutterStutter n m a -> [a]
unStutterStutter :: [a] }
 deriving (forall (n :: Nat) (m :: Nat) a b.
a -> StutterStutter n m b -> StutterStutter n m a
forall (n :: Nat) (m :: Nat) a b.
(a -> b) -> StutterStutter n m a -> StutterStutter n m b
forall a b. a -> StutterStutter n m b -> StutterStutter n m a
forall a b.
(a -> b) -> StutterStutter n m a -> StutterStutter n m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> StutterStutter n m b -> StutterStutter n m a
$c<$ :: forall (n :: Nat) (m :: Nat) a b.
a -> StutterStutter n m b -> StutterStutter n m a
fmap :: forall a b.
(a -> b) -> StutterStutter n m a -> StutterStutter n m b
$cfmap :: forall (n :: Nat) (m :: Nat) a b.
(a -> b) -> StutterStutter n m a -> StutterStutter n m b
Functor, Int -> StutterStutter n m a -> ShowS
forall (n :: Nat) (m :: Nat) a.
Show a =>
Int -> StutterStutter n m a -> ShowS
forall (n :: Nat) (m :: Nat) a.
Show a =>
[StutterStutter n m a] -> ShowS
forall (n :: Nat) (m :: Nat) a.
Show a =>
StutterStutter n m a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [StutterStutter n m a] -> ShowS
$cshowList :: forall (n :: Nat) (m :: Nat) a.
Show a =>
[StutterStutter n m a] -> ShowS
show :: StutterStutter n m a -> String
$cshow :: forall (n :: Nat) (m :: Nat) a.
Show a =>
StutterStutter n m a -> String
showsPrec :: Int -> StutterStutter n m a -> ShowS
$cshowsPrec :: forall (n :: Nat) (m :: Nat) a.
Show a =>
Int -> StutterStutter n m a -> ShowS
Show, StutterStutter n m a -> StutterStutter n m a -> Bool
forall (n :: Nat) (m :: Nat) a.
Eq a =>
StutterStutter n m a -> StutterStutter n m a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StutterStutter n m a -> StutterStutter n m a -> Bool
$c/= :: forall (n :: Nat) (m :: Nat) a.
Eq a =>
StutterStutter n m a -> StutterStutter n m a -> Bool
== :: StutterStutter n m a -> StutterStutter n m a -> Bool
$c== :: forall (n :: Nat) (m :: Nat) a.
Eq a =>
StutterStutter n m a -> StutterStutter n m a -> Bool
Eq)

deriving instance (KnownNat n, KnownNat m) => IsString (StutterStutter n m Char)

instance (KnownNat n, KnownNat m) => Applicative (StutterStutter n m) where
  pure :: forall a. a -> StutterStutter n m a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b.
StutterStutter n m (a -> b)
-> StutterStutter n m a -> StutterStutter n m b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (KnownNat n, KnownNat m) => Monad (StutterStutter n m) where
  return :: forall a. a -> StutterStutter n m a
return a
x = forall (n :: Nat) (m :: Nat) a. [a] -> StutterStutter n m a
StutterStutter [a
x]
  StutterStutter [a]
xs >>= :: forall a b.
StutterStutter n m a
-> (a -> StutterStutter n m b) -> StutterStutter n m b
>>= a -> StutterStutter n m b
f = forall (n :: Nat) (m :: Nat) a. [a] -> StutterStutter n m a
StutterStutter forall a b. (a -> b) -> a -> b
$ [[b]] -> [b]
join forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (n :: Nat) (m :: Nat) a. StutterStutter n m a -> [a]
unStutterStutter forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> StutterStutter n m b
f) [a]
xs
   where
    join :: [[b]] -> [b]
join [[b]]
xss | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[b]]
xss
             = []
             | forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a. [a] -> a
head (forall a. (a -> Bool) -> [a] -> [a]
dropWhile forall a. [a] -> Bool
isSingle (forall a. [a] -> [a]
init [[b]]
xss) forall a. [a] -> [a] -> [a]
++ [forall a. [a] -> a
last [[b]]
xss]))
             = let n :: Int
n = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
               in  forall a. Int -> [a] -> [a]
replicateLast (Int
n forall a. Num a => a -> a -> a
+ Int
1) (forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
takeWhile forall a. [a] -> Bool
isSingle (forall a. [a] -> [a]
init [[b]]
xss))
             | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Bool
isSingle) (forall a. [a] -> [a]
init [[b]]
xss) Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a. [a] -> a
last [[b]]
xss)
             = let m :: Int
m = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy m)
               in  forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat (forall a. (a -> Bool) -> [a] -> [a]
takeWhile forall a. [a] -> Bool
isSingle (forall a. [a] -> [a]
init [[b]]
xss))
                    forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (Int
m forall a. Num a => a -> a -> a
+ Int
2) (forall a. [a] -> a
head (forall a. [a] -> a
head (forall a. (a -> Bool) -> [a] -> [a]
dropWhile forall a. [a] -> Bool
isSingle (forall a. [a] -> [a]
init [[b]]
xss))))
             | Bool
otherwise
             = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[b]]
xss

instance (KnownNat n, KnownNat m) => IsList (StutterStutter n m a) where
  type Item (StutterStutter n m a) = a
  toList :: StutterStutter n m a -> [Item (StutterStutter n m a)]
toList   = forall (n :: Nat) (m :: Nat) a. StutterStutter n m a -> [a]
unStutterStutter
  fromList :: [Item (StutterStutter n m a)] -> StutterStutter n m a
fromList = forall (n :: Nat) (m :: Nat) a. [a] -> StutterStutter n m a
StutterStutter 

instance (KnownNat n, KnownNat m) => ListMonad (StutterStutter n m) 

instance (KnownNat n, KnownNat m) => PointedMagma (StutterStutter n m a) where
  StutterStutter n m a
m <> :: StutterStutter n m a
-> StutterStutter n m a -> StutterStutter n m a
<> StutterStutter n m a
t = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (m :: Nat) a. [a] -> StutterStutter n m a
StutterStutter forall a b. (a -> b) -> a -> b
$ [StutterStutter n m a
m, StutterStutter n m a
t]
  eps :: StutterStutter n m a
eps    = forall (n :: Nat) (m :: Nat) a. [a] -> StutterStutter n m a
StutterStutter []

instance (KnownNat n, KnownNat m)
  => StutterStutterAlgebra n m (StutterStutter n m a)

instance (KnownNat n, KnownNat m)
  => FreeRBPM (StutterStutter n m) (StutterStutterAlgebra n m)

-- $numerical_monoids
-- 
-- A /numerical monoid/ is a subset of the set of natural numbers that
-- contains 0 and is closed under addition. That is,
-- \(M \subseteq \mathbb N\)
-- is a numerical monoid if
--
--  * \(0 \in M\),
--
--  * if \(x,y \in M\), then \(x+y \in M\).
--
-- Representing a numerical monoid \(M\) using its characteristic
-- function @m :: Int -> Bool@ (revealing if a given number belongs to
-- \(M\)), we can define a monad as follows:
--
-- @
-- join xss | isSingle xss || all isSingle xss                         = concat xss
--          | null xss || any null xss                                 = []
--          | m (length xss - 1) && all (\\xs -> m $ length xs - 1) xss = concat xss
--          | otherwise                                                = []
-- @
--
-- There is also some intuition behind the "@- 1@" part: For a set \(M \subseteq \mathbb N\),
-- we define a set shifted by 1 as \(M^{+} =\{x \in \mathbb N \ |\ x-1 \in M\}\).
-- Then, \(M\) is a numerical monoid if and only if:
--
-- * \(1 \in M^{+}\),
--
-- * if \(n, x_1, \ldots, x_n \in M^{+}\), then \(\displaystyle \sum_{i = 0}^n x_i \in M^{+}\).
--
-- (Do note that in the above \(n\) is in \(M^{+}\) as well!) This
-- means that \(M^{+}\) is a set of "accepted lengths" of lists, while
-- the condition above states that when we concatenate an accepted
-- number of accepted lists, we still obtain an accepted list. This in
-- turn can be used to prove the associativity law for monads: breadly
-- speaking, @join :: [[[a]]] -> [a]@ is a concat only if all the
-- lists on all levels are of accepted lengths (save for the unit
-- laws), and joining (either the inner lists or the outer list first)
-- will not produce a non-accepted list.
--
-- Below, we first show a couple of concrete examples of monads
-- arising from particular numerical monoids, and then the general
-- version via a set of generators.

--------------------
-- The Mini monad --
--------------------

-- | The Mini monad is, in a sense, a minimal list monad, meaning that
-- its join fails (= results in an empty list) for all values except
-- the ones that appear in the unit laws (i.e., a singleton or a list
-- of singletons):
--
-- @
-- join xss | isSingle xss || all isSingle xss = concat xss
--          | otherwise                        = []
-- @
--
-- For example:
--
-- >>> join ["HelloThere"] :: Mini Char
-- Mini "HelloThere"
-- >>> join ["Hello", "There"] :: Mini Char
-- Mini ""
-- >>> join ["H", "T"] :: Mini Char
-- Mini "HT"
--
-- This monad arises from the numerical monoid \(\{0\}\).
--
-- It does not arise from a subclass of 'PointedMagma' (or any
-- algebraic theory with a finite number of operations for that 
-- matter).
newtype Mini a = Mini { forall a. Mini a -> [a]
unMini :: [a] }
 deriving (forall a b. a -> Mini b -> Mini a
forall a b. (a -> b) -> Mini a -> Mini b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Mini b -> Mini a
$c<$ :: forall a b. a -> Mini b -> Mini a
fmap :: forall a b. (a -> b) -> Mini a -> Mini b
$cfmap :: forall a b. (a -> b) -> Mini a -> Mini b
Functor, Int -> Mini a -> ShowS
forall a. Show a => Int -> Mini a -> ShowS
forall a. Show a => [Mini a] -> ShowS
forall a. Show a => Mini a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Mini a] -> ShowS
$cshowList :: forall a. Show a => [Mini a] -> ShowS
show :: Mini a -> String
$cshow :: forall a. Show a => Mini a -> String
showsPrec :: Int -> Mini a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Mini a -> ShowS
Show, Mini a -> Mini a -> Bool
forall a. Eq a => Mini a -> Mini a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Mini a -> Mini a -> Bool
$c/= :: forall a. Eq a => Mini a -> Mini a -> Bool
== :: Mini a -> Mini a -> Bool
$c== :: forall a. Eq a => Mini a -> Mini a -> Bool
Eq)

deriving instance IsString (Mini Char)

instance Applicative Mini where
  pure :: forall a. a -> Mini a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b. Mini (a -> b) -> Mini a -> Mini b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad Mini where
  return :: forall a. a -> Mini a
return a
x = forall a. [a] -> Mini a
Mini [a
x]
  Mini [a]
xs >>= :: forall a b. Mini a -> (a -> Mini b) -> Mini b
>>= a -> Mini b
f = forall a. [a] -> Mini a
Mini forall a b. (a -> b) -> a -> b
$ forall {a}. [[a]] -> [a]
join forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Mini a -> [a]
unMini forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Mini b
f) [a]
xs 
   where
    join :: [[a]] -> [a]
join [[a]]
xss | forall a. [a] -> Bool
isSingle [[a]]
xss Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. [a] -> Bool
isSingle [[a]]
xss = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[a]]
xss
             | Bool
otherwise                        = []

instance IsList (Mini a) where
  type Item (Mini a) = a
  toList :: Mini a -> [Item (Mini a)]
toList   = forall a. Mini a -> [a]
unMini
  fromList :: [Item (Mini a)] -> Mini a
fromList = forall a. [a] -> Mini a
Mini

instance ListMonad Mini

-------------------
-- The Odd monad --
-------------------

-- | The join of the Odd monad is a concat of the inner lists provided
-- there is an odd number of them, and that all of them are of odd
-- length themselves. Otherwise (modulo cases needed for the unit
-- laws), it returns an empty list.
--
-- @
-- join xss | isSingle xss || all isSingle xss  = concat xss
--          | odd (length xss)
--             && all (odd . length) xss        = concat xss 
--          | otherwise                         = []
-- @
--
-- For example:
--
-- >>> join ["Elvis", "Presley"] :: Odd Char
-- Odd ""
-- >>> join ["Elvis", "Aaron", "Presley"] :: Odd Char
-- Odd "ElvisAaronPresley"
-- >>> join ["Roy", "Kelton", "Orbison"] :: Odd Char
-- Odd ""
--
-- It arises from the numerical monoid \(\{0,2,4,6,\ldots\}\). -- Note that the sum of even numbers is always even, which cannot be said of odd numbers!
--
--
-- At the moment, it is unclear whether it comes from a finite
-- algebraic theory.
newtype Odd a = Odd { forall a. Odd a -> [a]
unOdd :: [a] }
 deriving (forall a b. a -> Odd b -> Odd a
forall a b. (a -> b) -> Odd a -> Odd b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Odd b -> Odd a
$c<$ :: forall a b. a -> Odd b -> Odd a
fmap :: forall a b. (a -> b) -> Odd a -> Odd b
$cfmap :: forall a b. (a -> b) -> Odd a -> Odd b
Functor, Int -> Odd a -> ShowS
forall a. Show a => Int -> Odd a -> ShowS
forall a. Show a => [Odd a] -> ShowS
forall a. Show a => Odd a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Odd a] -> ShowS
$cshowList :: forall a. Show a => [Odd a] -> ShowS
show :: Odd a -> String
$cshow :: forall a. Show a => Odd a -> String
showsPrec :: Int -> Odd a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Odd a -> ShowS
Show, Odd a -> Odd a -> Bool
forall a. Eq a => Odd a -> Odd a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Odd a -> Odd a -> Bool
$c/= :: forall a. Eq a => Odd a -> Odd a -> Bool
== :: Odd a -> Odd a -> Bool
$c== :: forall a. Eq a => Odd a -> Odd a -> Bool
Eq)

deriving instance IsString (Odd Char)

instance Applicative Odd where
  pure :: forall a. a -> Odd a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b. Odd (a -> b) -> Odd a -> Odd b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad Odd where
  return :: forall a. a -> Odd a
return a
x = forall a. [a] -> Odd a
Odd [a
x]
  Odd [a]
xs >>= :: forall a b. Odd a -> (a -> Odd b) -> Odd b
>>= a -> Odd b
f = forall a. [a] -> Odd a
Odd forall a b. (a -> b) -> a -> b
$ forall {a}. [[a]] -> [a]
join forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Odd a -> [a]
unOdd forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Odd b
f) [a]
xs 
   where
    join :: [[a]] -> [a]
join [[a]]
xss | forall a. [a] -> Bool
isSingle [[a]]
xss Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. [a] -> Bool
isSingle [[a]]
xss
             = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[a]]
xss
             | forall a. Integral a => a -> Bool
odd (forall (t :: * -> *) a. Foldable t => t a -> Int
length [[a]]
xss) Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Integral a => a -> Bool
odd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length) [[a]]
xss
             = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[a]]
xss
             | Bool
otherwise
             = []

instance IsList (Odd a) where
  type Item (Odd a) = a
  toList :: Odd a -> [Item (Odd a)]
toList   = forall a. Odd a -> [a]
unOdd
  fromList :: [Item (Odd a)] -> Odd a
fromList = forall a. [a] -> Odd a
Odd

instance ListMonad Odd

------------------------
-- The At Least monad --
------------------------

-- | The join of the @AtLeast n@ monad is a concat of the inner lists
-- provided there are at least @n@ inner lists and all the inner lists
-- are of length at least @n@ or 1 (plus the cases required by the
-- unit laws).
--
-- The join can thus be defined as follows (omitting the conversion of
-- the type-level nats to run-time values):
--
-- @
-- join xss | isSingle xss || all isSingle xss  = concat xss
--          | otherwise = let ok :: forall x. [x] -> Bool
--                            ok xs = length xs >= n || length xs == 1
--                        in if ok xss && all ok xss
--                             then concat xss
--                             else []
-- @
--
-- For example:
--
-- >>> join ["Strawberry", "Fields", "Forever"] :: AtLeast 3 Char
-- AtLeast "StrawberryFieldsForever"
-- >>> join ["All", "You", "Need", "Is", "Love"] :: AtLeast 3 Char
-- AtLeast []
-- >>> join ["I", "Want", "You"] :: AtLeast 3 Char
-- AtLeast "IWantYou"
-- >>> join ["I", "Am", "The", "Walrus"] :: AtLeast 3 Char
-- AtLeast []
--
-- The monad @AtLeast n@ arises from the numerical monoid \(\{0, n-1, n, n+1, n+2,\ldots\}\).
newtype AtLeast (n :: Nat) a = AtLeast { forall (n :: Nat) a. AtLeast n a -> [a]
unAtLeast :: [a] }
 deriving (forall (n :: Nat) a b. a -> AtLeast n b -> AtLeast n a
forall (n :: Nat) a b. (a -> b) -> AtLeast n a -> AtLeast n b
forall a b. a -> AtLeast n b -> AtLeast n a
forall a b. (a -> b) -> AtLeast n a -> AtLeast n b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> AtLeast n b -> AtLeast n a
$c<$ :: forall (n :: Nat) a b. a -> AtLeast n b -> AtLeast n a
fmap :: forall a b. (a -> b) -> AtLeast n a -> AtLeast n b
$cfmap :: forall (n :: Nat) a b. (a -> b) -> AtLeast n a -> AtLeast n b
Functor, Int -> AtLeast n a -> ShowS
forall (n :: Nat) a. Show a => Int -> AtLeast n a -> ShowS
forall (n :: Nat) a. Show a => [AtLeast n a] -> ShowS
forall (n :: Nat) a. Show a => AtLeast n a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AtLeast n a] -> ShowS
$cshowList :: forall (n :: Nat) a. Show a => [AtLeast n a] -> ShowS
show :: AtLeast n a -> String
$cshow :: forall (n :: Nat) a. Show a => AtLeast n a -> String
showsPrec :: Int -> AtLeast n a -> ShowS
$cshowsPrec :: forall (n :: Nat) a. Show a => Int -> AtLeast n a -> ShowS
Show, AtLeast n a -> AtLeast n a -> Bool
forall (n :: Nat) a. Eq a => AtLeast n a -> AtLeast n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AtLeast n a -> AtLeast n a -> Bool
$c/= :: forall (n :: Nat) a. Eq a => AtLeast n a -> AtLeast n a -> Bool
== :: AtLeast n a -> AtLeast n a -> Bool
$c== :: forall (n :: Nat) a. Eq a => AtLeast n a -> AtLeast n a -> Bool
Eq)

deriving instance (KnownNat n) => IsString (AtLeast n Char)

instance (KnownNat n) => Applicative (AtLeast n) where
  pure :: forall a. a -> AtLeast n a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b. AtLeast n (a -> b) -> AtLeast n a -> AtLeast n b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (KnownNat n) => Monad (AtLeast n) where
  return :: forall a. a -> AtLeast n a
return a
x = forall (n :: Nat) a. [a] -> AtLeast n a
AtLeast [a
x]
  AtLeast [a]
xs >>= :: forall a b. AtLeast n a -> (a -> AtLeast n b) -> AtLeast n b
>>= a -> AtLeast n b
f = forall (n :: Nat) a. [a] -> AtLeast n a
AtLeast forall a b. (a -> b) -> a -> b
$ [[b]] -> [b]
join forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (n :: Nat) a. AtLeast n a -> [a]
unAtLeast forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> AtLeast n b
f) [a]
xs 
   where
    join :: [[b]] -> [b]
join [[b]]
xss | forall a. [a] -> Bool
isSingle [[b]]
xss     = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[b]]
xss
             | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. [a] -> Bool
isSingle [[b]]
xss = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[b]]
xss
             | Bool
otherwise        = let n :: Int
n = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
                                      ok :: forall x. [x] -> Bool
                                      ok :: forall a. [a] -> Bool
ok [x]
xs = forall (t :: * -> *) a. Foldable t => t a -> Int
length [x]
xs forall a. Ord a => a -> a -> Bool
>= Int
n Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => t a -> Int
length [x]
xs forall a. Eq a => a -> a -> Bool
== Int
1
                                  in if forall a. [a] -> Bool
ok [[b]]
xss Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. [a] -> Bool
ok [[b]]
xss
                                       then forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[b]]
xss
                                       else []

instance (KnownNat n) => IsList (AtLeast n a) where
  type Item (AtLeast n a) = a
  toList :: AtLeast n a -> [Item (AtLeast n a)]
toList   = forall (n :: Nat) a. AtLeast n a -> [a]
unAtLeast
  fromList :: [Item (AtLeast n a)] -> AtLeast n a
fromList = forall (n :: Nat) a. [a] -> AtLeast n a
AtLeast

instance (KnownNat n) => ListMonad (AtLeast n)

--------------------------------
-- The Numerical Monoid monad --
--------------------------------

-- | An interesting property of numerical monoids is that they are
-- always finitely generated. This means that every numerical monoid
-- can be constructed by starting out with a finite set of nautral
-- numbers and closing it under addition. For example, the set
-- \(\{0,2,4,6,\ldots\}\) is generated by \(\{2\}\), because every
-- even number is of the form \(2k\) for some \(k\).
--
-- The class @'NumericalMonoidGenerators'@ represents a set of
-- generators given as a type-level list of nats.
class NumericalMonoidGenerators (ns :: [Nat]) where
  -- | Check if a given number is in the numerical monoid generatted
  -- by @ns@. It is the characteristic function of the generated
  -- numerical monoid.
  isInNumericalMonoid :: Int -> Bool

instance NumericalMonoidGenerators '[] where
  isInNumericalMonoid :: Int -> Bool
isInNumericalMonoid = (forall a. Eq a => a -> a -> Bool
== Int
0)

instance (KnownNat g, NumericalMonoidGenerators gs) => NumericalMonoidGenerators (g ': gs) where
  isInNumericalMonoid :: Int -> Bool
isInNumericalMonoid Int
x
     | Int
x forall a. Ord a => a -> a -> Bool
< Int
0     = Bool
False
     | Bool
otherwise =  forall (ns :: [Nat]). NumericalMonoidGenerators ns => Int -> Bool
isInNumericalMonoid @gs Int
x
                 Bool -> Bool -> Bool
|| Int
x forall a. Ord a => a -> a -> Bool
>= Int
g Bool -> Bool -> Bool
&& Int
g forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& forall (ns :: [Nat]). NumericalMonoidGenerators ns => Int -> Bool
isInNumericalMonoid @(g ': gs) (Int
x forall a. Num a => a -> a -> a
- Int
g)
   where
    g :: Int
g = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy g)

-- | The monad generated by the numerical monoid generated by a set of generators @ns@.
--
-- @
-- join xss | null xss || any null xss                                     = []
--          | isInNumericalMonoid \@ns (length xss - 1)
--             && all (\\xs -> isInNumericalMonoid \@ns (length xs - 1)) xss = concat xss
--          | otherwise                                                    = []
-- @
--
-- In particular:
--
-- * @'Mini'@ is equivalent to @NumericalMonoidMonad '[]@,
--
-- * @'GlobalFailure'@ is equivalent to @NumericalMonoidMonad '[1]@,
--
-- * @'Odd'@ is equivalent to @NumericalMonoidMonad '[2]@,
--
-- * @'AtLeast' n@ is equivalent to @NumericalMonoidMonad '[n-1, n, n+1, ..., 2n-3]@.
newtype NumericalMonoidMonad (ns :: [Nat]) a = NumericalMonoidMonad { forall (ns :: [Nat]) a. NumericalMonoidMonad ns a -> [a]
unNumericalMonoidMonad :: [a] }
 deriving (forall (ns :: [Nat]) a b.
a -> NumericalMonoidMonad ns b -> NumericalMonoidMonad ns a
forall (ns :: [Nat]) a b.
(a -> b) -> NumericalMonoidMonad ns a -> NumericalMonoidMonad ns b
forall a b.
a -> NumericalMonoidMonad ns b -> NumericalMonoidMonad ns a
forall a b.
(a -> b) -> NumericalMonoidMonad ns a -> NumericalMonoidMonad ns b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b.
a -> NumericalMonoidMonad ns b -> NumericalMonoidMonad ns a
$c<$ :: forall (ns :: [Nat]) a b.
a -> NumericalMonoidMonad ns b -> NumericalMonoidMonad ns a
fmap :: forall a b.
(a -> b) -> NumericalMonoidMonad ns a -> NumericalMonoidMonad ns b
$cfmap :: forall (ns :: [Nat]) a b.
(a -> b) -> NumericalMonoidMonad ns a -> NumericalMonoidMonad ns b
Functor, Int -> NumericalMonoidMonad ns a -> ShowS
forall (ns :: [Nat]) a.
Show a =>
Int -> NumericalMonoidMonad ns a -> ShowS
forall (ns :: [Nat]) a.
Show a =>
[NumericalMonoidMonad ns a] -> ShowS
forall (ns :: [Nat]) a.
Show a =>
NumericalMonoidMonad ns a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NumericalMonoidMonad ns a] -> ShowS
$cshowList :: forall (ns :: [Nat]) a.
Show a =>
[NumericalMonoidMonad ns a] -> ShowS
show :: NumericalMonoidMonad ns a -> String
$cshow :: forall (ns :: [Nat]) a.
Show a =>
NumericalMonoidMonad ns a -> String
showsPrec :: Int -> NumericalMonoidMonad ns a -> ShowS
$cshowsPrec :: forall (ns :: [Nat]) a.
Show a =>
Int -> NumericalMonoidMonad ns a -> ShowS
Show, NumericalMonoidMonad ns a -> NumericalMonoidMonad ns a -> Bool
forall (ns :: [Nat]) a.
Eq a =>
NumericalMonoidMonad ns a -> NumericalMonoidMonad ns a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NumericalMonoidMonad ns a -> NumericalMonoidMonad ns a -> Bool
$c/= :: forall (ns :: [Nat]) a.
Eq a =>
NumericalMonoidMonad ns a -> NumericalMonoidMonad ns a -> Bool
== :: NumericalMonoidMonad ns a -> NumericalMonoidMonad ns a -> Bool
$c== :: forall (ns :: [Nat]) a.
Eq a =>
NumericalMonoidMonad ns a -> NumericalMonoidMonad ns a -> Bool
Eq)

deriving instance IsString (NumericalMonoidMonad ns Char)

instance (NumericalMonoidGenerators ns) => Applicative (NumericalMonoidMonad ns) where
  pure :: forall a. a -> NumericalMonoidMonad ns a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b.
NumericalMonoidMonad ns (a -> b)
-> NumericalMonoidMonad ns a -> NumericalMonoidMonad ns b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (NumericalMonoidGenerators ns) => Monad (NumericalMonoidMonad ns) where
  return :: forall a. a -> NumericalMonoidMonad ns a
return a
x = forall (ns :: [Nat]) a. [a] -> NumericalMonoidMonad ns a
NumericalMonoidMonad [a
x]
  NumericalMonoidMonad [a]
xs >>= :: forall a b.
NumericalMonoidMonad ns a
-> (a -> NumericalMonoidMonad ns b) -> NumericalMonoidMonad ns b
>>= a -> NumericalMonoidMonad ns b
f = forall (ns :: [Nat]) a. [a] -> NumericalMonoidMonad ns a
NumericalMonoidMonad forall a b. (a -> b) -> a -> b
$ [[b]] -> [b]
join forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (ns :: [Nat]) a. NumericalMonoidMonad ns a -> [a]
unNumericalMonoidMonad forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> NumericalMonoidMonad ns b
f) [a]
xs 
   where
    join :: [[b]] -> [b]
join [[b]]
xss | forall a. [a] -> Bool
isSingle [[b]]
xss Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. [a] -> Bool
isSingle [[b]]
xss                          = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[b]]
xss
             | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[b]]
xss Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[b]]
xss                                  = []
             | forall (ns :: [Nat]). NumericalMonoidGenerators ns => Int -> Bool
isInNumericalMonoid @ns (forall (t :: * -> *) a. Foldable t => t a -> Int
length [[b]]
xss forall a. Num a => a -> a -> a
- Int
1)
             Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\[b]
xs -> forall (ns :: [Nat]). NumericalMonoidGenerators ns => Int -> Bool
isInNumericalMonoid @ns (forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
xs forall a. Num a => a -> a -> a
- Int
1)) [[b]]
xss = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[b]]
xss
             | Bool
otherwise                                                 = []

instance IsList (NumericalMonoidMonad ns a) where
  type Item (NumericalMonoidMonad ns a) = a
  toList :: NumericalMonoidMonad ns a -> [Item (NumericalMonoidMonad ns a)]
toList   = forall (ns :: [Nat]) a. NumericalMonoidMonad ns a -> [a]
unNumericalMonoidMonad
  fromList :: [Item (NumericalMonoidMonad ns a)] -> NumericalMonoidMonad ns a
fromList = forall (ns :: [Nat]) a. [a] -> NumericalMonoidMonad ns a
NumericalMonoidMonad

instance (NumericalMonoidGenerators ns) => ListMonad (NumericalMonoidMonad ns)

-----------------------
-- The At Most monad --
-----------------------

-- | The monad whose join is concat, but only if the total length of
-- the list (that is, the sum of the lengths of the inner lists) is
-- not greater than @n@ (except for the unit laws and the "global
-- failure" property):
--
-- @
-- join xss | isSingle xss || all isSingle xss = concat xss
--          | any null xss                     = []
--          | length (concat xss) <= n         = concat xss
--          | otherwise                        = []
-- @
--
-- For example:
--
-- >>> join ["El","vis"] :: AtMost 5 Char
-- AtMost "Elvis"
-- >>> join ["El","v","i"] :: AtMost 5 Char
-- AtMost "Elvi"
-- >>> join ["El","","vis"] :: AtMost 5 Char
-- AtMost ""
-- >>> join ["Presley"] :: AtMost 5 Char
-- AtMost "Presley"
-- >>> join ["P","r","e","s","l","e","y"] :: AtMost 5 Char
-- AtMost "Presley"
-- >>> join ["Pre","s","ley"] :: AtMost 5 Char
-- AtMost ""
newtype AtMost (n :: Nat) a = AtMost { forall (n :: Nat) a. AtMost n a -> [a]
unAtMost :: [a] }
 deriving (forall (n :: Nat) a b. a -> AtMost n b -> AtMost n a
forall (n :: Nat) a b. (a -> b) -> AtMost n a -> AtMost n b
forall a b. a -> AtMost n b -> AtMost n a
forall a b. (a -> b) -> AtMost n a -> AtMost n b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> AtMost n b -> AtMost n a
$c<$ :: forall (n :: Nat) a b. a -> AtMost n b -> AtMost n a
fmap :: forall a b. (a -> b) -> AtMost n a -> AtMost n b
$cfmap :: forall (n :: Nat) a b. (a -> b) -> AtMost n a -> AtMost n b
Functor, Int -> AtMost n a -> ShowS
forall (n :: Nat) a. Show a => Int -> AtMost n a -> ShowS
forall (n :: Nat) a. Show a => [AtMost n a] -> ShowS
forall (n :: Nat) a. Show a => AtMost n a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AtMost n a] -> ShowS
$cshowList :: forall (n :: Nat) a. Show a => [AtMost n a] -> ShowS
show :: AtMost n a -> String
$cshow :: forall (n :: Nat) a. Show a => AtMost n a -> String
showsPrec :: Int -> AtMost n a -> ShowS
$cshowsPrec :: forall (n :: Nat) a. Show a => Int -> AtMost n a -> ShowS
Show, AtMost n a -> AtMost n a -> Bool
forall (n :: Nat) a. Eq a => AtMost n a -> AtMost n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AtMost n a -> AtMost n a -> Bool
$c/= :: forall (n :: Nat) a. Eq a => AtMost n a -> AtMost n a -> Bool
== :: AtMost n a -> AtMost n a -> Bool
$c== :: forall (n :: Nat) a. Eq a => AtMost n a -> AtMost n a -> Bool
Eq)

deriving instance (KnownNat n) => IsString (AtMost n Char)

instance (KnownNat n) => Applicative (AtMost n) where
  pure :: forall a. a -> AtMost n a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b. AtMost n (a -> b) -> AtMost n a -> AtMost n b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (KnownNat n) => Monad (AtMost n) where
  return :: forall a. a -> AtMost n a
return a
x = forall (n :: Nat) a. [a] -> AtMost n a
AtMost [a
x]
  AtMost [a]
xs >>= :: forall a b. AtMost n a -> (a -> AtMost n b) -> AtMost n b
>>= a -> AtMost n b
f = forall (n :: Nat) a. [a] -> AtMost n a
AtMost forall a b. (a -> b) -> a -> b
$ [[b]] -> [b]
join forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (n :: Nat) a. AtMost n a -> [a]
unAtMost forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> AtMost n b
f) [a]
xs 
   where
    join :: [[b]] -> [b]
join [[b]]
xss | forall a. [a] -> Bool
isSingle [[b]]
xss Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. [a] -> Bool
isSingle [[b]]
xss                                = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[b]]
xss
             | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[b]]
xss                                                    = []
             | forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[b]]
xss) forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[b]]
xss
             | Bool
otherwise                                                       = []

instance (KnownNat n) => IsList (AtMost n a) where
  type Item (AtMost n a) = a
  toList :: AtMost n a -> [Item (AtMost n a)]
toList   = forall (n :: Nat) a. AtMost n a -> [a]
unAtMost
  fromList :: [Item (AtMost n a)] -> AtMost n a
fromList = forall (n :: Nat) a. [a] -> AtMost n a
AtMost

instance (KnownNat n) => ListMonad (AtMost n)

-----------------------------------
-- The Continuum-of-Monads monad --
-----------------------------------

-- $continuum-monads
--
-- The "Continuum of Monads" monad construction was introduced in
-- [this
-- paper](https://cla.tcs.uj.edu.pl/pdfs/McDermott-Pirog-Uustalu-Abstract.pdf)
-- to show that the set of list monads is a
-- [continuum](https://en.wikipedia.org/wiki/Cardinality_of_the_continuum)
-- (that is, that there are as many list monads in the category of
-- sets as there are real numbers, and more than there are natural
-- numbers).
--
-- We define a family of monads @'ContinuumOfMonads'@, which is
-- parameterised by a subset of the set of natural numbers
-- (@'SetOfNats'@).

-- | The @SetOfNats@ class defines a subset of the set of natural
-- numbers (from which we are actually interested in odd numbers
-- only). We give two instances, @Primes@ and @Fib@, as examples, so
-- if one wants to construct their own monad, they need to define an
-- instance first: any total @'elemOf'@ gives a monad.
--
-- For example:
--
-- >>> filter (elemOf @"Primes") [0..100]
-- [2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97]
-- >>> filter (elemOf @"Fib") [0..100]
-- [0,1,2,3,5,8,13,21,34,55,89]
class SetOfNats (a :: Symbol) where
  -- | The characteristic function of the defined set.
  elemOf :: Int -> Bool

-- Example sets:

primes :: [Int]
primes :: [Int]
primes = forall {a}. Integral a => [a] -> [a]
sieve [Int
2..] where sieve :: [a] -> [a]
sieve [a]
ps = forall a. [a] -> a
head [a]
ps forall a. a -> [a] -> [a]
: [a] -> [a]
sieve [a
x | a
x <- forall a. [a] -> [a]
tail [a]
ps, a
x forall a. Integral a => a -> a -> a
`mod` forall a. [a] -> a
head [a]
ps forall a. Ord a => a -> a -> Bool
> a
0]

-- | The set of prime numbers.
instance SetOfNats "Primes" where elemOf :: Int -> Bool
elemOf Int
n = Int
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a. Ord a => a -> a -> Bool
<= Int
n) [Int]
primes

fib :: [Int]
fib :: [Int]
fib = Int
0 forall a. a -> [a] -> [a]
: Int
1 forall a. a -> [a] -> [a]
: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. Num a => a -> a -> a
(+) [Int]
fib (forall a. [a] -> [a]
tail [Int]
fib)

-- | The set of Fibonacci numbers.
instance SetOfNats "Fib" where elemOf :: Int -> Bool
elemOf Int
n = Int
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a. Ord a => a -> a -> Bool
<= Int
n) [Int]
fib

-- | The @'ContinuumOfMonads'@ monad is parameterised by a set of
-- natural numbers (a symbol that instantiates @'SetOfNats'@).
--
-- The @join@ of @ContinuumOfMonads s@ is defined as follows:
--
-- @
-- join xss       | isSingle xss    || all isSingle xss      = concat xss
--                | null xss        || any null xss          = []
-- join [[x], xs] | odd (length xs) && elemOf @s (length xs) = x : xs
-- join _                                                    = []
-- @
--
-- For example:
--
-- >>> join [[0],[1,2,3]] :: ContinuumOfMonads "Primes" Int
-- ContinuumOfMonads [0,1,2,3]
-- >>> join [[0],[1,2,3,4]] :: ContinuumOfMonads "Primes" Int
-- ContinuumOfMonads []
-- >>> join [[0,1],[1,2,3,4,5]] :: ContinuumOfMonads "Primes" Int
-- ContinuumOfMonads []
newtype ContinuumOfMonads (s :: Symbol) a = ContinuumOfMonads { forall (s :: Symbol) a. ContinuumOfMonads s a -> [a]
unContinuumOfMonads :: [a] }
 deriving (forall a b. a -> ContinuumOfMonads s b -> ContinuumOfMonads s a
forall a b.
(a -> b) -> ContinuumOfMonads s a -> ContinuumOfMonads s b
forall (s :: Symbol) a b.
a -> ContinuumOfMonads s b -> ContinuumOfMonads s a
forall (s :: Symbol) a b.
(a -> b) -> ContinuumOfMonads s a -> ContinuumOfMonads s b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> ContinuumOfMonads s b -> ContinuumOfMonads s a
$c<$ :: forall (s :: Symbol) a b.
a -> ContinuumOfMonads s b -> ContinuumOfMonads s a
fmap :: forall a b.
(a -> b) -> ContinuumOfMonads s a -> ContinuumOfMonads s b
$cfmap :: forall (s :: Symbol) a b.
(a -> b) -> ContinuumOfMonads s a -> ContinuumOfMonads s b
Functor, Int -> ContinuumOfMonads s a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (s :: Symbol) a.
Show a =>
Int -> ContinuumOfMonads s a -> ShowS
forall (s :: Symbol) a. Show a => [ContinuumOfMonads s a] -> ShowS
forall (s :: Symbol) a. Show a => ContinuumOfMonads s a -> String
showList :: [ContinuumOfMonads s a] -> ShowS
$cshowList :: forall (s :: Symbol) a. Show a => [ContinuumOfMonads s a] -> ShowS
show :: ContinuumOfMonads s a -> String
$cshow :: forall (s :: Symbol) a. Show a => ContinuumOfMonads s a -> String
showsPrec :: Int -> ContinuumOfMonads s a -> ShowS
$cshowsPrec :: forall (s :: Symbol) a.
Show a =>
Int -> ContinuumOfMonads s a -> ShowS
Show, ContinuumOfMonads s a -> ContinuumOfMonads s a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (s :: Symbol) a.
Eq a =>
ContinuumOfMonads s a -> ContinuumOfMonads s a -> Bool
/= :: ContinuumOfMonads s a -> ContinuumOfMonads s a -> Bool
$c/= :: forall (s :: Symbol) a.
Eq a =>
ContinuumOfMonads s a -> ContinuumOfMonads s a -> Bool
== :: ContinuumOfMonads s a -> ContinuumOfMonads s a -> Bool
$c== :: forall (s :: Symbol) a.
Eq a =>
ContinuumOfMonads s a -> ContinuumOfMonads s a -> Bool
Eq)

deriving instance IsString (ContinuumOfMonads s Char)

instance (SetOfNats s) => Applicative (ContinuumOfMonads s) where
  pure :: forall a. a -> ContinuumOfMonads s a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b.
ContinuumOfMonads s (a -> b)
-> ContinuumOfMonads s a -> ContinuumOfMonads s b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (SetOfNats s) => Monad (ContinuumOfMonads s) where
  return :: forall a. a -> ContinuumOfMonads s a
return a
x = forall (s :: Symbol) a. [a] -> ContinuumOfMonads s a
ContinuumOfMonads [a
x]
  ContinuumOfMonads [a]
xs >>= :: forall a b.
ContinuumOfMonads s a
-> (a -> ContinuumOfMonads s b) -> ContinuumOfMonads s b
>>= a -> ContinuumOfMonads s b
f = forall (s :: Symbol) a. [a] -> ContinuumOfMonads s a
ContinuumOfMonads forall a b. (a -> b) -> a -> b
$ [[b]] -> [b]
join forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (s :: Symbol) a. ContinuumOfMonads s a -> [a]
unContinuumOfMonads forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ContinuumOfMonads s b
f) [a]
xs 
   where
    join :: [[b]] -> [b]
join [[b]]
xss | forall a. [a] -> Bool
isSingle [[b]]
xss Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. [a] -> Bool
isSingle [[b]]
xss               = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[b]]
xss
             | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[b]]
xss Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[b]]
xss                       = []
    join [[b
x], [b]
xs] | forall a. Integral a => a -> Bool
odd (forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
xs) Bool -> Bool -> Bool
&& forall (a :: Symbol). SetOfNats a => Int -> Bool
elemOf @s (forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
xs) = b
x forall a. a -> [a] -> [a]
: [b]
xs
    join [[b]]
_                                                    = []

instance IsList (ContinuumOfMonads s a) where
  type Item (ContinuumOfMonads s a) = a
  toList :: ContinuumOfMonads s a -> [Item (ContinuumOfMonads s a)]
toList   = forall (s :: Symbol) a. ContinuumOfMonads s a -> [a]
unContinuumOfMonads
  fromList :: [Item (ContinuumOfMonads s a)] -> ContinuumOfMonads s a
fromList = forall (s :: Symbol) a. [a] -> ContinuumOfMonads s a
ContinuumOfMonads

instance (SetOfNats s) => ListMonad (ContinuumOfMonads s)

------------------------------------
-- The Short Stutter-Keeper monad --
------------------------------------

-- | This monad works just like the 'StutterKeeper' monad but it takes
-- a prefix of the result of join of length @p+2@ (unless the unit
-- laws say otherwise). Thus, its join is defined as follows (omitting
-- the conversion of the type-level 'Nat' @p@ to a run-time value):
--
-- @
-- join xss | isSingle xss     = concat xss
--          | all isSingle xss = concat xss
--          | otherwise        = take (p + 2) $ toList
--                                 ((Control.Monad.join $ StutterKeeper $ fmap StutterKeeper xss)
--                                   :: StutterKeeper n _)
-- @
--
-- For example:
--
-- >>> join ["1", "2", "buckle", "my", "shoe"] :: ShortStutterKeeper 5 2 Char
-- ShortStutterKeeper "12bu"
-- >>> join ["1", "2", "buckle"] :: ShortStutterKeeper 5 2 Char
-- ShortStutterKeeper "12bu"
-- >>> join ["1", "2", "", "my", "shoe"] :: ShortStutterKeeper 5 2 Char
-- ShortStutterKeeper "1222"
--
-- Compare the 'Control.Monad.List.NonEmpty.Exotic.ShortFront' monad
-- on non-empty lists.
newtype ShortStutterKeeper (n :: Nat) (p :: Nat) a =
  ShortStutterKeeper { forall (n :: Nat) (p :: Nat) a. ShortStutterKeeper n p a -> [a]
unShortStutterKeeper :: [a] }
 deriving (forall (n :: Nat) (p :: Nat) a b.
a -> ShortStutterKeeper n p b -> ShortStutterKeeper n p a
forall (n :: Nat) (p :: Nat) a b.
(a -> b) -> ShortStutterKeeper n p a -> ShortStutterKeeper n p b
forall a b.
a -> ShortStutterKeeper n p b -> ShortStutterKeeper n p a
forall a b.
(a -> b) -> ShortStutterKeeper n p a -> ShortStutterKeeper n p b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b.
a -> ShortStutterKeeper n p b -> ShortStutterKeeper n p a
$c<$ :: forall (n :: Nat) (p :: Nat) a b.
a -> ShortStutterKeeper n p b -> ShortStutterKeeper n p a
fmap :: forall a b.
(a -> b) -> ShortStutterKeeper n p a -> ShortStutterKeeper n p b
$cfmap :: forall (n :: Nat) (p :: Nat) a b.
(a -> b) -> ShortStutterKeeper n p a -> ShortStutterKeeper n p b
Functor, Int -> ShortStutterKeeper n p a -> ShowS
forall (n :: Nat) (p :: Nat) a.
Show a =>
Int -> ShortStutterKeeper n p a -> ShowS
forall (n :: Nat) (p :: Nat) a.
Show a =>
[ShortStutterKeeper n p a] -> ShowS
forall (n :: Nat) (p :: Nat) a.
Show a =>
ShortStutterKeeper n p a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ShortStutterKeeper n p a] -> ShowS
$cshowList :: forall (n :: Nat) (p :: Nat) a.
Show a =>
[ShortStutterKeeper n p a] -> ShowS
show :: ShortStutterKeeper n p a -> String
$cshow :: forall (n :: Nat) (p :: Nat) a.
Show a =>
ShortStutterKeeper n p a -> String
showsPrec :: Int -> ShortStutterKeeper n p a -> ShowS
$cshowsPrec :: forall (n :: Nat) (p :: Nat) a.
Show a =>
Int -> ShortStutterKeeper n p a -> ShowS
Show, ShortStutterKeeper n p a -> ShortStutterKeeper n p a -> Bool
forall (n :: Nat) (p :: Nat) a.
Eq a =>
ShortStutterKeeper n p a -> ShortStutterKeeper n p a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ShortStutterKeeper n p a -> ShortStutterKeeper n p a -> Bool
$c/= :: forall (n :: Nat) (p :: Nat) a.
Eq a =>
ShortStutterKeeper n p a -> ShortStutterKeeper n p a -> Bool
== :: ShortStutterKeeper n p a -> ShortStutterKeeper n p a -> Bool
$c== :: forall (n :: Nat) (p :: Nat) a.
Eq a =>
ShortStutterKeeper n p a -> ShortStutterKeeper n p a -> Bool
Eq)

deriving instance (KnownNat n, KnownNat p) => IsString (ShortStutterKeeper n p Char)

instance (KnownNat n, KnownNat p) => Applicative (ShortStutterKeeper n p) where
  pure :: forall a. a -> ShortStutterKeeper n p a
pure  = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b.
ShortStutterKeeper n p (a -> b)
-> ShortStutterKeeper n p a -> ShortStutterKeeper n p b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (KnownNat n, KnownNat p) => Monad (ShortStutterKeeper n p) where
  return :: forall a. a -> ShortStutterKeeper n p a
return a
x = forall (n :: Nat) (p :: Nat) a. [a] -> ShortStutterKeeper n p a
ShortStutterKeeper [a
x]
  ShortStutterKeeper [a]
xs >>= :: forall a b.
ShortStutterKeeper n p a
-> (a -> ShortStutterKeeper n p b) -> ShortStutterKeeper n p b
>>= a -> ShortStutterKeeper n p b
f = forall (n :: Nat) (p :: Nat) a. [a] -> ShortStutterKeeper n p a
ShortStutterKeeper forall a b. (a -> b) -> a -> b
$ forall {a}. [[a]] -> [a]
join forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (n :: Nat) (p :: Nat) a. ShortStutterKeeper n p a -> [a]
unShortStutterKeeper forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ShortStutterKeeper n p b
f) [a]
xs
   where
    join :: forall x. [[x]] -> [x]
    join :: forall {a}. [[a]] -> [a]
join [[x]]
xss | forall a. [a] -> Bool
isSingle [[x]]
xss = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[x]]
xss
             | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. [a] -> Bool
isSingle [[x]]
xss = forall {t :: * -> *} {a}. Foldable t => t [a] -> [a]
concat [[x]]
xss
             | Bool
otherwise =
                  let p :: Int
p = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy p)
                  in  forall a. Int -> [a] -> [a]
take (Int
p forall a. Num a => a -> a -> a
+ Int
2) forall a b. (a -> b) -> a -> b
$ forall l. IsList l => l -> [Item l]
toList
                      ((forall (m :: * -> *) a. Monad m => m (m a) -> m a
Control.Monad.join forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) a. [a] -> StutterKeeper n a
StutterKeeper forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat) a. [a] -> StutterKeeper n a
StutterKeeper [[x]]
xss)
                        :: StutterKeeper n x)

instance (KnownNat n, KnownNat p) => IsList (ShortStutterKeeper n p a) where
  type Item (ShortStutterKeeper n p a) = a
  toList :: ShortStutterKeeper n p a -> [Item (ShortStutterKeeper n p a)]
toList   = forall (n :: Nat) (p :: Nat) a. ShortStutterKeeper n p a -> [a]
unShortStutterKeeper
  fromList :: [Item (ShortStutterKeeper n p a)] -> ShortStutterKeeper n p a
fromList = forall (n :: Nat) (p :: Nat) a. [a] -> ShortStutterKeeper n p a
ShortStutterKeeper 

instance (KnownNat n, KnownNat p) => ListMonad (ShortStutterKeeper n p)