diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# exotic-list-monad changelog
+
+## v1.0.0
+
+- Initial version
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,7 @@
+Copyright 2020 Dylan McDermott, Maciej Piróg, Tarmo Uustalu
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,13 @@
+# exotic-list-monads
+
+[![Build Status](https://api.travis-ci.com/maciejpirog/exotic-list-monads.png?branch=master)](http://travis-ci.com/maciejpirog/exotic-list-monads)
+
+A Haskell library that defines a few non-standard monads on lists and non-empty lists 
+
+## Description
+
+The usual [list monad](https://hackage.haskell.org/package/base-4.14.0.0/docs/src/GHC.Base.html#line-1133) is only one of infinitely many ways to turn the list functor into a monad. The same applies to the usual [non-empty list monad](https://hackage.haskell.org/package/base-4.14.0.0/docs/src/GHC.Base.html#line-1105) and the non-empty list functor. This library collects such non-standard "list" and "non-empty list" monads.
+
+Most of the constructions implemented in this library have been first introduced in the paper [Degrading lists](degrading-lists.pdf) by Dylan McDermott, Maciej Piróg, and Tarmo Uustalu (PPDP 2020), but there are some new specimens as well.
+
+It is quite possible that there exist "list" and "non-empty list" monads that we are not aware of, so pull requests are appreciated. Moreover, not every monad in this library has been formally verified to be a monad (because of the combinatorial explosion of the number of cases to be considered in the proof of associativity), so if you're currently playing around with tools like Coq and have a spare afternoon...
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/degrading-lists.pdf b/degrading-lists.pdf
new file mode 100644
Binary files /dev/null and b/degrading-lists.pdf differ
diff --git a/exotic-list-monads.cabal b/exotic-list-monads.cabal
new file mode 100644
--- /dev/null
+++ b/exotic-list-monads.cabal
@@ -0,0 +1,62 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.33.0.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: d8bad60fc0a7573c702039797f7320d100d283efcb79d5789c85819c1c7ff760
+
+name:           exotic-list-monads
+version:        1.0.0
+synopsis:       Non-standard monads on lists and non-empty lists
+description:    The usual list monad is only one of infinitely many ways to turn the list functor into a monad. The same applies to the usual non-empty list monad and the non-empty list functor. This library collects such non-standard "list" and "non-empty list" monads.
+category:       List, Monads
+homepage:       http://github.com/maciejpirog/exotic-list-monads
+bug-reports:    http://github.com/maciejpirog/exotic-list-monads/issues
+author:         Maciej Piróg <maciej.adam.pirog@gmial.com>
+maintainer:     Maciej Piróg <maciej.adam.pirog@gmail.com>
+copyright:      (c) 2020 Dylan McDermott, Maciej Piróg, Tarmo Uustalu
+license:        MIT
+license-file:   LICENSE
+tested-with:    GHC ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.3 || ==8.10.1
+build-type:     Simple
+extra-source-files:
+    README.md
+    CHANGELOG.md
+    degrading-lists.pdf
+
+source-repository head
+  type: git
+  location: https://github.com/maciejpirog/exotic-list-monads
+
+library
+  exposed-modules:
+      Control.Monad.List.Exotic
+      Control.Monad.List.NonEmpty.Exotic
+  other-modules:
+      Paths_exotic_list_monads
+  hs-source-dirs:
+      src
+  ghc-options: -Wall -Wno-name-shadowing -fno-warn-partial-type-signatures
+  build-depends:
+      base >=4.9 && <5
+  default-language: Haskell2010
+
+test-suite spec
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      Control.Monad.List.ExoticSpec
+      Control.Monad.List.NonEmpty.ExoticSpec
+      Paths_exotic_list_monads
+  hs-source-dirs:
+      test
+  ghc-options: -Wall -Wno-name-shadowing -fno-warn-partial-type-signatures
+  build-depends:
+      QuickCheck
+    , base >=4.9 && <5
+    , exotic-list-monads
+    , hspec ==2.*
+    , hspec-core
+  default-language: Haskell2010
+  build-tool-depends: hspec-discover:hspec-discover == 2.*
diff --git a/src/Control/Monad/List/Exotic.hs b/src/Control/Monad/List/Exotic.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/List/Exotic.hs
@@ -0,0 +1,1009 @@
+{-# 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 #-}
+
+-- 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 exotic "list monads". Most of them have been introduced in the
+-- paper [Degrading Lists](https://raw.githubusercontent.com/maciejpirog/exotic-list-monads/master/degrading-lists.pdf)
+-- by Dylan McDermott, Maciej Piróg, Tarmo Uustalu (PPDP 2020).
+--
+-- __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 presented in terms of @join@ rather
+-- than '>>='. In each case 'return' 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@ extensions, which allow
+-- us 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.
+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(..)
+
+  -- * Other monads
+
+  -- $no_finite_presentation
+  
+  -- ** The Mini monad
+
+  , Mini(..)
+  
+  -- ** The Odd monad (?)
+
+  , Odd(..)
+  
+  -- ** 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 = fromList
+  
+  unwrap :: m a -> [a]
+  default unwrap :: (IsList (m a), Item (m a) ~ a) => m a -> [a]
+  unwrap = toList
+
+instance ListMonad []
+
+liftListFun :: (ListMonad m) => ([a] -> [a]) -> m a -> m a
+liftListFun f = wrap . f . 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 { unDualListMonad :: m a }
+ deriving (Functor)
+
+instance (ListMonad m) => Applicative (DualListMonad m) where
+  pure  = return
+  (<*>) = ap
+
+instance (ListMonad m) => Monad (DualListMonad m) where
+  return = DualListMonad . liftListFun reverse . return
+  DualListMonad m >>= f = DualListMonad $ liftListFun reverse $
+    liftListFun reverse m >>= liftListFun reverse . unDualListMonad . f
+
+instance (ListMonad m, IsList (m a)) => IsList (DualListMonad m a) where
+  type Item (DualListMonad m a) = Item (m a)
+  toList (DualListMonad m) = toList m
+  fromList xs = DualListMonad (fromList xs)
+
+instance (ListMonad m) => ListMonad (DualListMonad m) where
+  wrap   = DualListMonad . wrap
+  unwrap = unwrap . unDualListMonad 
+
+-- | Checks if a given list is a singleton (= list of length one).
+isSingle :: [a] -> Bool
+isSingle [_] = True
+isSingle _   = 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 have 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 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 _ (unwrap -> []) = eps
+  foldRBPM f (unwrap -> xs) = foldr1 (<>) (map f 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 { unGlobalFailure :: [a] }
+ deriving (Functor, Show, Eq)
+
+deriving instance IsString (GlobalFailure Char)
+
+instance Applicative GlobalFailure where
+  pure  = return
+  (<*>) = ap
+
+instance Monad GlobalFailure where
+  return x = GlobalFailure [x]
+  GlobalFailure xs >>= f = GlobalFailure $ join $ map (unGlobalFailure . f) xs 
+   where
+    join xss | any null xss = []
+             | otherwise    = concat xss
+
+instance IsList (GlobalFailure a) where
+  type Item (GlobalFailure a) = a
+  toList   = unGlobalFailure
+  fromList = GlobalFailure
+
+instance ListMonad GlobalFailure
+
+instance PointedMagma (GlobalFailure a) where
+  m <> t = join $ GlobalFailure $ [m, t]
+  eps    = 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 [] = []
+palindromize xs = xs ++ reverse (init 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 \"▶\"):
+--
+-- @
+--  ┌──┬───┐
+--  │LU│NGO│
+--  ├╴A│I┌─┘
+--  ▶JPGR│
+-- ┌┘O│E┌┘
+-- │NH│O└─┐
+-- └──┤RGE│
+--    └───┘
+-- @
+--
+-- 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 { unMazeWalk :: [a] }
+ deriving (Functor, Show, Eq)
+
+deriving instance IsString (MazeWalk Char)
+
+instance Applicative MazeWalk where
+  pure  = return
+  (<*>) = ap
+
+instance Monad MazeWalk where
+  return x = MazeWalk [x]
+  MazeWalk xs >>= f = MazeWalk $ join $ map (unMazeWalk . f) xs 
+   where
+    join xss | null xss || any null xss
+             = []
+             | otherwise
+             = concatMap palindromize (init xss) ++ last xss
+
+instance IsList (MazeWalk a) where
+  type Item (MazeWalk a) = a
+  toList   = unMazeWalk
+  fromList = MazeWalk
+  
+instance ListMonad MazeWalk
+
+instance PointedMagma (MazeWalk a) where
+  m <> t = join $ MazeWalk $ [m, t]
+  eps    = 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 [] = []
+safeLast xs = [last 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"
+--
+-- Different versions of hybrid monads originate from Renato Neves's
+-- [PhD thesis](http://alfa.di.uminho.pt/~nevrenato/pdfs/thesis.pdf).
+newtype DiscreteHybrid a = DiscreteHybrid { unDiscreteHybrid :: [a] }
+ deriving (Functor, Show, Eq)
+
+deriving instance IsString (DiscreteHybrid Char)
+
+instance Applicative DiscreteHybrid where
+  pure  = return
+  (<*>) = ap
+
+instance Monad DiscreteHybrid where
+  return x = DiscreteHybrid [x]
+  DiscreteHybrid xs >>= f = DiscreteHybrid $ join $ map (unDiscreteHybrid . f) xs 
+   where
+    join xss | null xss        = []
+             | null (last xss) = []
+             | otherwise       = concatMap safeLast (init xss) ++ last xss
+
+instance IsList (DiscreteHybrid a) where
+  type Item (DiscreteHybrid a) = a
+  toList   = unDiscreteHybrid
+  fromList = DiscreteHybrid
+  
+instance ListMonad DiscreteHybrid
+
+instance PointedMagma (DiscreteHybrid a) where
+  m <> t = join $ DiscreteHybrid $ [m, t]
+  eps    = 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 { unListUnfold :: [a] }
+ deriving (Functor, Show, Eq)
+
+deriving instance IsString (ListUnfold Char)
+
+instance Applicative ListUnfold where
+  pure  = return
+  (<*>) = ap
+
+instance Monad ListUnfold where
+  return x = ListUnfold [x]
+  ListUnfold xs >>= f = ListUnfold $ join $ map (unListUnfold . f) xs 
+   where
+    join xss | null xss || any null xss
+             = []
+             | any (not . isSingle) (init xss)
+             = []
+             | otherwise
+             = concat xss
+
+instance IsList (ListUnfold a) where
+  type Item (ListUnfold a) = a
+  toList   = unListUnfold
+  fromList = ListUnfold
+  
+instance ListMonad ListUnfold
+
+instance PointedMagma (ListUnfold a) where
+  m <> t = join $ ListUnfold $ [m, t]
+  eps    = 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 _ [] = []
+replicateLast n xs = xs ++ replicate n (last 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 { unStutter :: [a] }
+ deriving (Functor, Show, Eq)
+
+deriving instance (KnownNat n) => IsString (Stutter n Char)
+
+instance (KnownNat n) => Applicative (Stutter n) where
+  pure  = return
+  (<*>) = ap
+
+instance (KnownNat n) => Monad (Stutter n) where
+  return x = Stutter [x]
+  Stutter xs >>= f = Stutter $ join $ map (unStutter . f) xs
+   where
+    join xss | null xss
+             = []
+             | any (not . isSingle) (init xss) || null (last xss)
+             = let n = fromIntegral $ natVal (Proxy :: Proxy n)
+               in  replicateLast (n + 1) (concat $ takeWhile isSingle (init xss))
+             | otherwise
+             = concat xss
+
+instance (KnownNat n) => IsList (Stutter n a) where
+  type Item (Stutter n a) = a
+  toList   = unStutter
+  fromList = Stutter 
+
+instance (KnownNat n) => ListMonad (Stutter n) 
+
+instance (KnownNat n) => PointedMagma (Stutter n a) where
+  m <> t = join $ Stutter $ [m, t]
+  eps    = Stutter []
+
+instance (KnownNat n) => StutterAlgebra n (Stutter n a)
+
+instance (KnownNat n) => FreeRBPM (Stutter n) (StutterAlgebra n)
+
+-- $no_finite_presentation
+--
+-- While all list monads have presentations in terms of operations and
+-- equations, some require infinitely many operations. This section
+-- contains monads that are either known to require infinitely many
+-- operations, or those for which no finite presentation is known, but
+-- we don't know for sure that such a presentation doesn't exist.
+
+------------------------------
+-- 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
+
+-- | This 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 { unStutterKeeper :: [a] }
+ deriving (Functor, Show, Eq)
+
+deriving instance (KnownNat n) => IsString (StutterKeeper n Char)
+
+instance (KnownNat n) => Applicative (StutterKeeper n) where
+  pure  = return
+  (<*>) = ap
+
+instance (KnownNat n) => Monad (StutterKeeper n) where
+  return x = StutterKeeper [x]
+  StutterKeeper xs >>= f = StutterKeeper $ join $ map (unStutterKeeper . f) xs
+   where
+    join xss | null xss
+             = []
+             | null (head (dropWhile isSingle (init xss) ++ [last xss]))
+             = let n = fromIntegral $ natVal (Proxy :: Proxy n)
+               in  replicateLast (n + 1) (concat $ takeWhile isSingle (init xss))
+             | otherwise
+             = map head (takeWhile isSingle (init xss))
+                ++ head (dropWhile isSingle (init xss) ++ [last xss])
+
+instance (KnownNat n) => IsList (StutterKeeper n a) where
+  type Item (StutterKeeper n a) = a
+  toList   = unStutterKeeper
+  fromList = StutterKeeper 
+
+instance (KnownNat n) => ListMonad (StutterKeeper n) 
+
+instance (KnownNat n) => PointedMagma (StutterKeeper n a) where
+  m <> t = join $ StutterKeeper $ [m, t]
+  eps    = StutterKeeper []
+
+instance (KnownNat n) => StutterKeeperAlgebra n (StutterKeeper n a)
+
+instance (KnownNat n) => FreeRBPM (StutterKeeper n) (StutterKeeperAlgebra n)
+
+------------------------------
+-- The StutterStutter monad --
+------------------------------
+
+-- | A stutter-keeper algebra (for given natural numbesr @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
+
+-- |
+--
+-- @
+-- 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 { unStutterStutter :: [a] }
+ deriving (Functor, Show, Eq)
+
+deriving instance (KnownNat n, KnownNat m) => IsString (StutterStutter n m Char)
+
+instance (KnownNat n, KnownNat m) => Applicative (StutterStutter n m) where
+  pure  = return
+  (<*>) = ap
+
+instance (KnownNat n, KnownNat m) => Monad (StutterStutter n m) where
+  return x = StutterStutter [x]
+  StutterStutter xs >>= f = StutterStutter $ join $ map (unStutterStutter . f) xs
+   where
+    join xss | null xss
+             = []
+             | null (head (dropWhile isSingle (init xss) ++ [last xss]))
+             = let n = fromIntegral $ natVal (Proxy :: Proxy n)
+               in  replicateLast (n + 1) (concat $ takeWhile isSingle (init xss))
+             | any (not . isSingle) (init xss) || null (last xss)
+             = let m = fromIntegral $ natVal (Proxy :: Proxy m)
+               in  concat (takeWhile isSingle (init xss))
+                    ++ replicate (m + 2) (head (head (dropWhile isSingle (init xss))))
+             | otherwise
+             = concat xss
+
+instance (KnownNat n, KnownNat m) => IsList (StutterStutter n m a) where
+  type Item (StutterStutter n m a) = a
+  toList   = unStutterStutter
+  fromList = StutterStutter 
+
+instance (KnownNat n, KnownNat m) => ListMonad (StutterStutter n m) 
+
+instance (KnownNat n, KnownNat m) => PointedMagma (StutterStutter n m a) where
+  m <> t = join $ StutterStutter $ [m, t]
+  eps    = 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)
+
+--------------------
+-- The Mini monad --
+--------------------
+
+-- | The Mini monad is the 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     = concat xss
+--          | all isSingle xss = concat xss
+--          | otherwise        = []
+-- @
+--
+-- For example:
+--
+-- >>> join ["HelloThere"] :: Mini Char
+-- Mini "HelloThere"
+-- >>> join ["Hello", "There"] :: Mini Char
+-- Mini ""
+--
+-- 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 { unMini :: [a] }
+ deriving (Functor, Show, Eq)
+
+deriving instance IsString (Mini Char)
+
+instance Applicative Mini where
+  pure  = return
+  (<*>) = ap
+
+instance Monad Mini where
+  return x = Mini [x]
+  Mini xs >>= f = Mini $ join $ map (unMini . f) xs 
+   where
+    join xss | isSingle xss || all isSingle xss
+             = concat xss
+             | otherwise
+             = []
+
+instance IsList (Mini a) where
+  type Item (Mini a) = a
+  toList   = unMini
+  fromList = 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               = concat 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 ""
+--
+-- At the moment, it is unclear whether it comes from a finite
+-- algebraic theory (or that it is indeed a monad).
+newtype Odd a = Odd { unOdd :: [a] }
+ deriving (Functor, Show, Eq)
+
+deriving instance IsString (Odd Char)
+
+instance Applicative Odd where
+  pure  = return
+  (<*>) = ap
+
+instance Monad Odd where
+  return x = Odd [x]
+  Odd xs >>= f = Odd $ join $ map (unOdd . f) xs 
+   where
+    join xss | isSingle xss || all isSingle xss
+             = concat xss
+             | odd (length xss) && all (odd . length) xss
+             = concat xss
+             | otherwise
+             = []
+
+instance IsList (Odd a) where
+  type Item (Odd a) = a
+  toList   = unOdd
+  fromList = Odd
+
+instance ListMonad Odd
+
+------------------------------------
+-- 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 { unShortStutterKeeper :: [a] }
+ deriving (Functor, Show, Eq)
+
+deriving instance (KnownNat n, KnownNat p) => IsString (ShortStutterKeeper n p Char)
+
+instance (KnownNat n, KnownNat p) => Applicative (ShortStutterKeeper n p) where
+  pure  = return
+  (<*>) = ap
+
+instance (KnownNat n, KnownNat p) => Monad (ShortStutterKeeper n p) where
+  return x = ShortStutterKeeper [x]
+  ShortStutterKeeper xs >>= f = ShortStutterKeeper $ join $ map (unShortStutterKeeper . f) xs
+   where join xss | isSingle xss = concat xss
+                  | all isSingle xss = concat xss
+                  | otherwise
+                  = let p = fromIntegral $ natVal (Proxy :: Proxy p)
+                    in  take (p + 2) $ toList
+                        ((Control.Monad.join $ StutterKeeper $ fmap StutterKeeper xss)
+                          :: StutterKeeper n _)
+
+instance (KnownNat n, KnownNat p) => IsList (ShortStutterKeeper n p a) where
+  type Item (ShortStutterKeeper n p a) = a
+  toList   = unShortStutterKeeper
+  fromList = ShortStutterKeeper 
+
+instance (KnownNat n, KnownNat p) => ListMonad (ShortStutterKeeper n p) 
diff --git a/src/Control/Monad/List/NonEmpty/Exotic.hs b/src/Control/Monad/List/NonEmpty/Exotic.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/List/NonEmpty/Exotic.hs
@@ -0,0 +1,1071 @@
+{-# LANGUAGE Trustworthy #-} -- can't use Safe due to IsList instance
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE OverloadedLists #-}
+
+-- {-# LANGUAGE OverloadedStrings #-}
+
+-- |
+-- Module      : Control.Monad.List.NonEmpty.Exotic
+-- Description : Non-standard monads on the non-empty 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 'NonEmpty.NonEmpty' (list) functor into a monad. This module
+-- collects a number of such exotic "non-empty list monads".  Most of
+-- them have been introduced in the paper [Degrading
+-- Lists](https://raw.githubusercontent.com/maciejpirog/exotic-list-monads/master/degrading-lists.pdf)
+-- by Dylan McDermott, Maciej Piróg, Tarmo Uustalu (PPDP 2020).
+--
+-- __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 presented in terms of @join@ rather
+-- than '>>=', while 'return' is singleton, unless stated otherwise
+-- for a particular monad (e.g., 'HeadTails', 'HeadsTail', or
+-- 'IdXList').
+--
+-- * For readability, code snippets in this documentation assume the
+-- @OverloadedLists@ and @OverloadedStrings@ extensions, which allow
+-- us 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 $ 'fmap' ('unwrap' . f) $ 'unwrap' m
+--  where
+--   join = ...
+-- @
+--
+-- * Sometimes it is more readable to define the join in terms of
+-- possibly-empty lists. In such a case, we call the local function
+-- @joinList@:
+--
+-- @
+-- m '>>=' f = 'wrap' $ 'GHC.Exts.fromList' $ joinList $ 'map' ('GHC.Exts.toList' . 'unwrap' . f) $ 'GHC.Exts.toList' $ 'unwrap' m
+--  where
+--   joinList = ...
+-- @
+--
+-- 
+-- * 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.
+
+
+module Control.Monad.List.NonEmpty.Exotic
+  (
+  -- * Non-empty monads in general
+
+    IsNonEmpty(..)
+  , NonEmptyMonad(..)
+    
+  -- ** More on non-empty lists
+
+  , isSingle
+  , splitSnoc
+  , nonEmptyConcat
+  , (+++)
+  , nonEmptyAll
+  , nonEmptyAny
+    
+  -- * Monads from magmas
+
+  -- $magmas
+  
+  , Magma(..)
+  , FreeRBM(..)
+
+  -- ** The Keeper monad
+
+  , XY
+  , Keeper(..)
+  
+  -- ** The Non-Empty Discrete Hybrid monad
+
+  , YZ
+  , DiscreteHybridNE(..)
+  
+  -- ** The Non-Empty Discrete Op-Hybrid monad
+
+  , XZ
+  , OpDiscreteHybridNE(..)
+
+  -- ** The Non-Empty Maze Walk monad
+
+  , PalindromeMagma
+  , MazeWalkNE(..)
+
+  -- ** The Non-Empty Stutter monad
+
+  , StutterMagma
+  , StutterNE(..)
+  
+  -- * Other monads with finite presentation
+
+  -- $others
+  
+  -- ** The Head-Tails monad
+
+  , HeadTailTail(..)
+  , HeadTails(..)
+  , foldHeadTails
+
+  -- ** The Heads-Tail monad
+
+  , HeadHeadTail(..)
+  , HeadsTail(..)
+  , foldHeadsTail
+  
+  -- * Other monads
+
+  -- ** The ΑΩ monad (?)
+
+  , AlphaOmega(..)
+
+  -- * Constructions on non-empty monads
+
+  -- ** The dual non-empty list monad
+
+  , DualNonEmptyMonad(..)
+
+  -- ** The @Identity@ ⨉ @List@ monad
+
+  , IdXList(..)
+
+  -- ** Short-front monads
+
+  , HasShortFront
+  , ShortFront(..)
+
+  -- ** Short-rear monads
+
+  , HasShortRear
+  , ShortRear(..)
+  
+  ) where
+
+import Data.List.NonEmpty (NonEmpty(..))
+import qualified Data.List.NonEmpty as NonEmpty
+import Prelude hiding ((<>))
+import Control.Monad (ap, join)
+import GHC.Exts (IsList(..), IsString(..), Constraint)
+import GHC.TypeLits
+import Data.Proxy
+import qualified Data.Semigroup (Semigroup)
+import Control.Monad.List.Exotic (ListMonad, palindromize)
+import qualified Control.Monad.List.Exotic as List.Exotic (ListMonad(..))
+
+---------------------------
+-- Non-empty list monads --
+---------------------------
+
+-- | This class collects types that are isomorphic to non-empty
+-- lists. It mimics the 'GHC.Exts.IsList' class.
+class IsNonEmpty l where
+  type ItemNE l
+  fromNonEmpty :: NonEmpty (ItemNE l) -> l
+  toNonEmpty   :: l -> NonEmpty (ItemNE l)
+
+instance IsNonEmpty (NonEmpty a) where
+  type ItemNE (NonEmpty a) = a
+  fromNonEmpty = id
+  toNonEmpty   = id
+
+-- | In this module, a \"non-empty monad\" is a monad in which the
+-- underlying functor is isomorphic to 'Data.List.NonEmpty.NonEmpty'.
+class (Monad m) => NonEmptyMonad m where
+
+  wrap   :: NonEmpty a -> m a
+  default wrap   :: (IsNonEmpty (m a), ItemNE (m a) ~ a) => NonEmpty a -> m a
+  wrap = fromNonEmpty
+  
+  unwrap :: m a -> NonEmpty a
+  default unwrap :: (IsNonEmpty (m a), ItemNE (m a) ~ a) => m a -> NonEmpty a
+  unwrap = toNonEmpty
+
+instance NonEmptyMonad NonEmpty
+
+-- | Split a non empty list to reveal the last element.
+splitSnoc :: NonEmpty a -> ([a], a)
+splitSnoc (x :| []) = ([], x)
+splitSnoc (x :| xs) = (x : init xs, last xs)
+
+-- | Check if a list is a singleton.
+isSingle :: NonEmpty a -> Bool
+isSingle (_ :| []) = True
+isSingle _         = False
+
+-- | 'concat' for non-empty lists.
+nonEmptyConcat :: NonEmpty (NonEmpty a) -> NonEmpty a
+nonEmptyConcat = join
+
+-- | '++' for non-empty lists.
+(+++) :: NonEmpty a -> NonEmpty a -> NonEmpty a
+a +++ b = nonEmptyConcat [a, b]  -- OverloadedLists
+
+-- | 'all' for non-empty lists.
+nonEmptyAll :: (a -> Bool) -> NonEmpty a -> Bool
+nonEmptyAll p (x :| xs) = p x && all p xs
+
+-- | 'any' for non-empty lists.
+nonEmptyAny :: (a -> Bool) -> NonEmpty a -> Bool
+nonEmptyAny p (x :| xs) = p x || any p xs
+
+------------
+-- Magmas --
+------------
+
+-- $magmas
+--
+-- This section contains monads that come about from free algebras of
+-- theories with one binary operation, that is, subcalsses of 'Magma'
+-- with no additional methods, but additional equations.
+
+-- | A very simple algebraic theory with one binary operations and no
+-- equations.
+class Magma a where
+  (<>) :: a -> a -> a
+
+-- | The name of the class stands for __free right-braketed__
+-- (subclass of) __magma__. (compare
+-- 'Control.Monad.List.Exotic.FreeRBPM' for more detailed
+-- explanation).
+--
+-- We consider theories @c@ with one equation of the following shape:
+--
+-- @
+-- (x '<>' y) '<>' z  ==  ...
+-- @
+--
+-- and normal forms of the following shape:
+--
+-- @
+-- x '<>' (y '<>' ( ... (z '<>' t) ... ))
+-- @
+--
+-- An instance @FreeRBM m c@ means that the monad @m@ comes about from
+-- free algebras of the theory @c@. For such monads and theories, we
+-- can define the following function:
+--
+-- @
+-- foldRBM f (toNonEmpty -> toList -> xs) = foldr1 (<>) (map f xs)
+-- @
+--
+-- which is the unique lifting of an interpretation of generators to a
+-- homomorphism (between algebras of this theory) from the list monad
+-- to any algebra (an instance) of @c@.
+--
+-- Note that the default definition of 'foldRBM' is always the right
+-- one for right-bracketed subclasses of 'Magma', so it is
+-- enough to declare the relationship, for example:
+--
+-- @
+-- instance FreeRBM 'NonEmpty' 'Data.Semigroup.Semigroup'
+-- @
+class (NonEmptyMonad m) => FreeRBM m (c :: * -> Constraint) | m -> c where
+  foldRBM :: (Magma a, c a) => (x -> a) -> m x -> a
+  foldRBM f (unwrap -> toList -> xs) = foldr1 (<>) (map f xs)
+
+instance FreeRBM NonEmpty Data.Semigroup.Semigroup
+
+----------------------
+-- The Keeper monad --
+----------------------
+
+-- | Instances should satisfy the following equation:
+--
+-- @
+-- (x '<>' y) '<>' z  ==  x '<>' y
+-- @
+class (Magma a) => XY a
+
+-- | The keeper monad arises from free 'XY' magmas. Its join (in terms
+-- of @joinList@) is given as follows:
+--
+-- @
+-- joinList xss = map head (takeWhile 'Control.Monad.List.Exotic.isSingle' (init xss))
+--                 ++ head (dropWhile 'Control.Monad.List.Exotic.isSingle' (init xss) ++ [last xss])
+-- @
+--
+-- Examples:
+--
+-- >>> toList $ unwrap (join ["a", "b", "c", "hello", "there"] :: Keeper Char)
+-- "abchello"
+-- >>> toList $ unwrap (join ["a", "b", "c", "hello"] :: Keeper Char)
+-- "abchello"
+newtype Keeper a = Keeper { unKeeper :: NonEmpty a }
+ deriving (Functor, Show, Eq)
+
+instance Applicative Keeper where
+  pure  = return
+  (<*>) = ap
+
+instance Monad Keeper where
+  return a = Keeper $ [a]  -- OverloadedLists
+  Keeper xs >>= f =
+    Keeper $ join $ NonEmpty.map (unKeeper . f) xs
+   where
+    join (splitSnoc -> (xss, xs)) = fromList $
+      map NonEmpty.head (takeWhile isSingle xss)
+       ++ toList (head (dropWhile isSingle xss ++ [xs])) -- OverloadedLists
+
+instance IsNonEmpty (Keeper a) where
+  type ItemNE (Keeper a) = a
+  fromNonEmpty = Keeper
+  toNonEmpty = unKeeper
+
+instance NonEmptyMonad Keeper
+
+instance Magma (Keeper a) where
+  m <> t = join $ Keeper $ [m, t]
+
+instance XY (Keeper a)
+
+instance FreeRBM Keeper XY
+
+-- The following two are needed for examples in the docs:
+
+instance IsList (Keeper a) where
+  type Item (Keeper a) = a
+  fromList = fromNonEmpty . fromList
+  toList = toList . toNonEmpty
+
+instance IsString (Keeper Char) where
+  fromString = fromList
+
+-----------------------------------------
+-- The Non-Empty Discrete Hybrid monad --
+-----------------------------------------
+
+-- | Instances should satisfy the following equation:
+--
+-- @
+-- (x '<>' y) '<>' z  ==  y '<>' z
+-- @
+class (Magma a) => YZ a
+
+-- | The non-empty discrete hybrid monad arises from free 'YZ'
+-- magmas. Its join (in terms of @joinList@) can be given as follows:
+--
+-- @
+-- joinList xss = map last (init xss) ++ last xss
+-- @
+--
+-- See the possibly-empty version
+-- ('Control.Monad.List.Exotic.DiscreteHybrid') for more details.
+newtype DiscreteHybridNE a =
+  DiscreteHybridNE { unDiscreteHybridNE :: NonEmpty a }
+ deriving (Functor, Show, Eq)
+
+instance Applicative DiscreteHybridNE where
+  pure  = return
+  (<*>) = ap
+
+instance Monad DiscreteHybridNE where
+  return a = DiscreteHybridNE $ [a]  -- OverloadedLists
+  DiscreteHybridNE xs >>= f =
+    DiscreteHybridNE $ join $ NonEmpty.map (unDiscreteHybridNE . f) xs
+   where
+    join (splitSnoc -> (xss, xs)) = fromList (map NonEmpty.last xss ++ toList xs)
+  
+instance IsNonEmpty (DiscreteHybridNE a) where
+  type ItemNE (DiscreteHybridNE a) = a
+  fromNonEmpty = DiscreteHybridNE
+  toNonEmpty = unDiscreteHybridNE
+
+instance NonEmptyMonad DiscreteHybridNE
+
+instance Magma (DiscreteHybridNE a) where
+  m <> t = join $ DiscreteHybridNE $ [m, t]
+
+instance YZ (DiscreteHybridNE a)
+
+instance FreeRBM DiscreteHybridNE YZ
+
+--------------------------------------------
+-- The Non-Empty Discrete Op-Hybrid monad --
+-------------------------------------------
+
+-- | Instances should satisfy the following equation:
+--
+-- @
+-- (x '<>' y) '<>' z  ==  x '<>' z
+-- @
+class (Magma a) => XZ a
+
+-- | The non-empty discrete op-hybrid monad arises from free 'XZ'
+-- magmas. It is dual to the 'DiscreteHybridNE' monad (but in a
+-- different dimension than 'DualNonEmptyMonad'). Its join (in terms
+-- of @joinList@) can be given as follows:
+--
+-- @
+-- joinList xss = map head (init xss) ++ last xss
+-- @
+--
+-- Examples:
+--
+-- >>> toList $ unwrap (join ["John", "Ronald", "Reuel", "Tolkien"] :: OpDiscreteHybridNE Char)
+-- "JRRTolkien"
+--
+-- Surprisingly, while the 'DiscreteHybridNE' monad has a counterpart
+-- for possibly-empty lists
+-- ('Control.Monad.List.Exotic.DiscreteHybrid'), the would-be
+-- counterpart of @OpDiscreteHybridNE@ obtained by taking first
+-- elements in the init is __not__ a monad.
+newtype OpDiscreteHybridNE a =
+  OpDiscreteHybridNE { unOpDiscreteHybridNE :: NonEmpty a }
+ deriving (Functor, Show, Eq)
+
+instance Applicative OpDiscreteHybridNE where
+  pure  = return
+  (<*>) = ap
+
+instance Monad OpDiscreteHybridNE where
+  return a = OpDiscreteHybridNE $ [a]  -- OverloadedLists
+  OpDiscreteHybridNE xs >>= f =
+    OpDiscreteHybridNE $ join $ NonEmpty.map (unOpDiscreteHybridNE . f) xs
+   where
+    join (splitSnoc -> (xss, xs)) = fromList (map NonEmpty.head xss ++ toList xs)
+
+instance IsNonEmpty (OpDiscreteHybridNE a) where
+  type ItemNE (OpDiscreteHybridNE a) = a
+  fromNonEmpty = OpDiscreteHybridNE
+  toNonEmpty = unOpDiscreteHybridNE
+
+instance NonEmptyMonad OpDiscreteHybridNE
+
+instance Magma (OpDiscreteHybridNE a) where
+  m <> t = join $ OpDiscreteHybridNE $ [m, t]
+
+instance XZ (OpDiscreteHybridNE a)
+
+instance FreeRBM OpDiscreteHybridNE XZ
+
+-- The following two are needed for examples in the docs:
+
+instance IsList (OpDiscreteHybridNE a) where
+  type Item (OpDiscreteHybridNE a) = a
+  fromList = fromNonEmpty . fromList
+  toList = toList . toNonEmpty
+
+instance IsString (OpDiscreteHybridNE Char) where
+  fromString = fromList
+
+--------------------------------------------
+-- The Non-empty Maze Walk monad --
+-------------------------------------------
+
+-- | Instances should satisfy the following equation:
+--
+-- @
+-- (x '<>' y) '<>' z  ==  x '<>' (y '<>' (x '<>' z))
+-- @
+class (Magma a) => PalindromeMagma a
+
+-- | The non-empty maze walk monad arises from free
+-- 'PalindromeMagma'-s. Its join (in terms of @joinList@) can be given
+-- as follows:
+--
+-- @
+-- joinList xss = map 'Control.Monad.List.Exotic.palindromize' (init xss) ++ last xss
+-- @
+--
+-- See the possibly-empty version
+-- ('Control.Monad.List.Exotic.MazeWalk') for more details.
+newtype MazeWalkNE a =
+  MazeWalkNE { unMazeWalkNE :: NonEmpty a }
+ deriving (Functor, Show, Eq)
+
+instance Applicative MazeWalkNE where
+  pure  = return
+  (<*>) = ap
+
+instance Monad MazeWalkNE where
+  return a = MazeWalkNE $ [a]  -- OverloadedLists
+  MazeWalkNE xs >>= f =
+    MazeWalkNE $ join $ NonEmpty.map (unMazeWalkNE . f) xs
+   where
+    join :: NonEmpty (NonEmpty a) -> NonEmpty a
+    join (splitSnoc -> (xss, xs)) = fromList $
+      concatMap (palindromize . toList) xss ++ toList xs 
+
+instance IsNonEmpty (MazeWalkNE a) where
+  type ItemNE (MazeWalkNE a) = a
+  fromNonEmpty = MazeWalkNE
+  toNonEmpty = unMazeWalkNE
+
+instance NonEmptyMonad MazeWalkNE
+
+instance Magma (MazeWalkNE a) where
+  m <> t = join $ MazeWalkNE $ [m, t]
+
+instance PalindromeMagma (MazeWalkNE a)
+
+instance FreeRBM MazeWalkNE PalindromeMagma
+
+---------------------------------
+-- The Non-empty Stutter monad --
+---------------------------------
+
+-- | Instances should satisfy the following equation:
+--
+-- @
+-- (x '<>' y) '<>' z  ==  'foldr1' ('<>') ('replicate' (n + 2) x)
+-- @
+class (KnownNat n, Magma a) => StutterMagma n a
+
+-- | The non-empty stutter monad arises from free 'StutterMagma'-s.
+-- Its join (in terms of @joinList@) can be given as follows:
+--
+-- @
+-- joinList xss | any (not . 'Control.Monad.List.Exotic.isSingle') (init xss)
+--              = map head (takeWhile 'Control.Monad.List.Exotic.isSingle' (init xss))
+--                 ++ replicate (n + 2) (head (head (dropWhile 'Control.Monad.List.Exotic.isSingle' (init xss))))
+--              | otherwise
+--              = map head (init xss) ++ last xss
+-- @
+--
+-- Examples:
+--
+-- >>> toList $ unwrap (join ["a", "b", "c", "hello", "there"] :: StutterNE 5 Char)
+-- "abchhhhhhh"
+-- >>> toList $ unwrap (join ["a", "b", "c", "hello"] :: StutterNE 5 Char)
+-- "abchello"
+
+newtype StutterNE (n :: Nat) a =
+  StutterNE { unStutterNE :: NonEmpty a }
+ deriving (Functor, Show, Eq)
+
+instance (KnownNat n) => Applicative (StutterNE n) where
+  pure  = return
+  (<*>) = ap
+
+instance (KnownNat n) => Monad (StutterNE n) where
+  return a = StutterNE $ [a]  -- OverloadedLists
+  StutterNE xs >>= f =
+    StutterNE $ join $ NonEmpty.map (unStutterNE . f) xs
+   where
+    join :: NonEmpty (NonEmpty a) -> NonEmpty a
+    join (splitSnoc -> (xss', xs))
+      | any (not . isSingle) xss'
+      = let n = fromIntegral $ natVal (Proxy :: Proxy n)
+        in  fromList $
+              map NonEmpty.head (takeWhile isSingle xss')
+               ++ replicate (n + 2)
+                  (NonEmpty.head $ head $ dropWhile isSingle xss')
+      | otherwise
+      = fromList $ map NonEmpty.head xss' ++ toList xs
+      
+instance (KnownNat n) => IsNonEmpty (StutterNE n a) where
+  type ItemNE (StutterNE n a) = a
+  fromNonEmpty = StutterNE
+  toNonEmpty = unStutterNE
+
+instance (KnownNat n) => NonEmptyMonad (StutterNE n)
+
+instance (KnownNat n) => Magma (StutterNE n a) where
+  m <> t = join $ StutterNE $ [m, t]
+
+instance (KnownNat n) => StutterMagma n (StutterNE n a)
+
+instance (KnownNat n) => FreeRBM (StutterNE n) (StutterMagma n)
+
+-- The following two are needed for examples in the docs:
+
+instance (KnownNat n) => IsList (StutterNE n a) where
+  type Item (StutterNE n a) = a
+  fromList = fromNonEmpty . fromList
+  toList = toList . toNonEmpty
+
+instance (KnownNat n) => IsString (StutterNE n Char) where
+  fromString = fromList
+
+--------------------------
+-- The Head-Tails monad --
+--------------------------
+
+-- $others
+--
+-- In contrast to the possibly-empty-list case, there are known
+-- non-empty monads that arise from algebraic theories, but ones that
+-- cannot be presented with one binary operations (as in monads that
+-- come about from subclasses of 'Magma').
+
+-- | The head-tail-tail algebra has two operations: unary 'hd'
+-- (intuitively, it produces a singleton list with the head of the
+-- argument as the element) and ternary 'htt' (intuitively, it
+-- produces the concat of the head of the first argument and tails of
+-- the other two arguments).
+--
+-- Instances should satisfy the following equations:
+--
+-- @
+-- x                         ==  'htt' x x ('hd' x)
+-- 'hd' ('hd' x)                 ==  'hd' x
+-- 'hd' ('htt' x y z)            ==  'hd' x
+-- 'htt' x y ('hd' z)            ==  'htt' x y ('hd' y)
+-- 'htt' x y ('htt' z v w)       ==  'htt' x y ('htt' y v w)
+-- 'htt' x ('hd' y) ('hd' z)       ==  'hd' x
+-- 'htt' x ('hd' y) ('htt' z v w)  ==  'htt' x v w
+-- 'htt' x ('htt' y z v) w       ==  'htt' x z ('htt' z v w)
+-- 'htt' ('hd' x) y z            ==  'htt' x y z
+-- 'htt' ('htt' x y z) v w       ==  'htt' x v w
+-- @
+--
+-- Moreover, when read left-to-right they form a terminating and
+-- confluent rewriting system with normal forms of the following
+-- shape:
+--
+-- @
+-- 'htt' x y $ 'htt' y z $ 'htt' z v $ ... $ 'htt' w t ('hd' t)
+-- @
+class HeadTailTail a where
+  hd  :: a -> a
+  htt :: a -> a -> a -> a
+
+-- | The Head-Tails monad arises from free head-tail-tail algebras. Its unit is a dubleton, that is:
+--
+-- @
+-- return x = HeadTails (x :| [x])
+-- @
+--
+-- Its join is defined as:
+--
+-- @
+-- join ((x :| _) :| xss) = x :| concatMap NonEmpty.tail xss
+-- @
+--
+-- For example:
+--
+-- >>> toList $ unwrap (join ["John", "Paul", "George", "Ringo"] :: HeadTails Char)
+-- "Jauleorgeingo"
+newtype HeadTails a = HeadTails { unHeadTails :: NonEmpty a }
+ deriving (Functor, Show, Eq)
+
+instance Applicative HeadTails where
+  pure  = return
+  (<*>) = ap
+
+instance Monad HeadTails where
+  return a = HeadTails $ [a,a]  -- OverloadedLists
+  HeadTails xs >>= f = HeadTails $ join $ NonEmpty.map (unHeadTails . f) xs
+   where
+    join ((x :| _) :| xss) = x :| concatMap NonEmpty.tail xss
+
+instance IsNonEmpty (HeadTails a) where
+  type ItemNE (HeadTails a) = a
+  fromNonEmpty = HeadTails
+  toNonEmpty = unHeadTails
+
+instance NonEmptyMonad HeadTails
+
+instance HeadTailTail (HeadTails a) where
+  hd  a     = join $ HeadTails [a]        -- OverloadedLists
+  htt a b c = join $ HeadTails [a, b, c]  -- OverloadedLists
+
+-- | The 'HeadTails' monad arises from free head-tail-tail algebras,
+-- so an interpretation of generators @g@ to a head-tail-tail algebra
+-- @a@ can be (uniquely) lifted to a homomorphism between
+-- head-tail-tail algebras.
+foldHeadTails :: (HeadTailTail a) => (g -> a) -> HeadTails g -> a
+foldHeadTails f (HeadTails (x :| [])) = hd (f x)
+foldHeadTails f (HeadTails (x :| (y : ys))) =
+  htt (f x) (f y) (foldHeadTails f $ HeadTails $ y :| ys)
+  
+-- The following two are needed for examples in the docs:
+
+instance IsList (HeadTails a) where
+  type Item (HeadTails a) = a
+  fromList = fromNonEmpty . fromList
+  toList = toList . toNonEmpty
+
+instance IsString (HeadTails Char) where
+  fromString = fromList
+
+--------------------------
+-- The Heads-Tail monad --
+--------------------------
+
+-- | Instances should satisfy the following equations:
+--
+-- @
+-- x                    ==  'ht' x x
+-- 'hd'' ('hd'' x)          ==  'hd'' x
+-- 'hd'' ('ht' x y)         ==  'hd'' x
+-- 'hd'' ('hht' x y z)      ==  'hd'' x
+-- 'ht' x ('hd'' y)         ==  'hd'' x
+-- 'ht' x ('ht' y z)        ==  'ht' x z
+-- 'ht' x ('hht' y z v)     ==  'hht' x z v
+-- 'ht' ('hd'' x) y         ==  'ht' x y
+-- 'ht' ('ht' x y) z        ==  'ht' x z
+-- 'ht' ('hht' x y z) v     ==  'ht' x v
+-- 'hht' x y ('hd'' z)      ==  'hd'' x
+-- 'hht' x y ('ht' z v)     ==  'hht' x y v
+-- 'hht' x y ('hht' z v w)  ==  'hht' x y ('hht' y v w)
+-- 'hht' x ('hd'' y) z      ==  'hht' x y z
+-- 'hht' x ('ht' y z) v     ==  'hht' x y v
+-- 'hht' x ('hht' y z v) w  ==  'hht' x y w
+-- 'hht' ('hd'' x) y z      ==  'hht' x y z
+-- 'hht' ('ht' x y) z v     ==  'hht' x z v
+-- 'hht' ('hht' x y z) v w  ==  'hht' x v w
+-- @
+--
+-- Moreover, when read left-to-right they form a terminating and
+-- confluent rewriting system with normal forms of the following
+-- shape:
+--
+-- @
+-- 'hd'' x
+-- 'ht' x y
+-- 'hht' x y $ 'hht' y z $ 'hht' z v $ ... $ 'hht' w t u
+-- @
+class HeadHeadTail a where
+  hd' :: a -> a
+  ht  :: a -> a -> a
+  hht :: a -> a -> a -> a
+  
+-- | The Heads-Tail monad arises from free head-head-tail algebras. Its unit is a dubleton, that is:
+--
+-- @
+-- return x = HeadsTail (x :| [x])
+-- @
+--
+-- Its join is defined as:
+--
+-- @
+-- join xss\@('splitSnoc' -> (xss', xs\@(_:|ys)))
+--   | 'isSingle' xss || 'isSingle' xs
+--   = (NonEmpty.head $ NonEmpty.head xss) :| []
+--   | otherwise
+--   = fromList $ map NonEmpty.head xss' ++ ys
+-- @
+--
+-- For example:
+--
+-- >>> toList $ unwrap (join ["John", "Paul", "George", "Ringo"] :: HeadsTail Char)
+-- "JPGingo"
+newtype HeadsTail a = HeadsTail { unHeadsTail :: NonEmpty a }
+ deriving (Functor, Show, Eq)
+
+instance Applicative HeadsTail where
+  pure  = return
+  (<*>) = ap
+
+instance Monad HeadsTail where
+  return a = HeadsTail $ [a,a]  -- OverloadedLists
+  HeadsTail xs >>= f = HeadsTail $ join $ NonEmpty.map (unHeadsTail . f) xs
+   where
+    join xss@(splitSnoc -> (xss', xs@(_:|ys)))
+      | isSingle xss || isSingle xs
+      = [NonEmpty.head $ NonEmpty.head xss]  -- OverloadedLists 
+      | otherwise
+      = fromList $ map NonEmpty.head xss' ++ ys
+                                       
+instance IsNonEmpty (HeadsTail a) where
+  type ItemNE (HeadsTail a) = a
+  fromNonEmpty = HeadsTail
+  toNonEmpty = unHeadsTail
+
+instance NonEmptyMonad HeadsTail
+
+instance HeadHeadTail (HeadsTail a) where
+  hd' a     = join $ HeadsTail [a]        -- OverloadedLists
+  ht  a b   = join $ HeadsTail [a, b]     -- OverloadedLists
+  hht a b c = join $ HeadsTail [a, b, c]  -- OverloadedLists
+
+-- | The 'HeadsTail' monad arises from free head-head-tail algebras,
+-- so an interpretation of generators @g@ to a head-head-tail algebra
+-- @a@ can be (uniquely) lifted to a homomorphism between
+-- head-head-tail algebras.
+foldHeadsTail :: (HeadHeadTail a) => (g -> a) -> HeadsTail g -> a
+foldHeadsTail f (HeadsTail (x :| []))       = hd' (f x)
+foldHeadsTail f (HeadsTail (x :| [y]))      = ht (f x) (f y)
+foldHeadsTail f (HeadsTail (x :| [y, z]))   = hht (f x) (f y) (f z)
+foldHeadsTail f (HeadsTail (x :| (y : ys))) =
+  hht (f x) (f y) (foldHeadsTail f $ HeadsTail $ y :| ys)
+
+-- The following two are needed for examples in the docs:
+
+instance IsList (HeadsTail a) where
+  type Item (HeadsTail a) = a
+  fromList = fromNonEmpty . fromList
+  toList = toList . toNonEmpty
+
+instance IsString (HeadsTail Char) where
+  fromString = fromList
+
+------------------
+-- The ΑΩ monad --
+------------------
+
+-- | The join of the ΑΩ (Alpha-Omega) monad takes the first element of
+-- the first list and the last element of the last list (unless the
+-- unit laws require otherwise):
+--
+-- @
+-- join xss | isSingle xss || nonEmptyAll isSingle xss
+--          = nonEmptyConcat xss
+--          | otherwise
+--          =  NonEmpty.head (NonEmpty.head xss)
+--          :| NonEmpty.last (NonEmpty.last xss) : []
+-- @
+--
+-- For example:
+--
+-- >>> toList $ unwrap (join ["John", "Paul", "George", "Ringo"] :: AlphaOmega Char)
+-- "Jo"
+newtype AlphaOmega a = AlphaOmega { unAlphaOmega :: NonEmpty a }
+ deriving (Functor, Show, Eq)
+
+instance Applicative AlphaOmega where
+  pure  = return
+  (<*>) = ap
+
+instance Monad AlphaOmega where
+  return a = AlphaOmega [a]                          -- OverloadedLists
+  AlphaOmega xs >>= f = AlphaOmega $ join $ NonEmpty.map (unAlphaOmega . f) xs
+   where
+    join xss | isSingle xss || nonEmptyAll isSingle xss
+             = nonEmptyConcat xss
+             | otherwise
+             = [ NonEmpty.head (NonEmpty.head xss)   -- OverloadedLists
+               , NonEmpty.last (NonEmpty.last xss) ]
+
+instance IsNonEmpty (AlphaOmega a) where
+  type ItemNE (AlphaOmega a) = a
+  fromNonEmpty = AlphaOmega
+  toNonEmpty = unAlphaOmega
+
+instance NonEmptyMonad AlphaOmega
+
+-- The following two are needed for examples in the docs:
+
+instance IsList (AlphaOmega a) where
+  type Item (AlphaOmega a) = a
+  fromList = fromNonEmpty . fromList
+  toList = toList . toNonEmpty
+
+instance IsString (AlphaOmega Char) where
+  fromString = fromList
+
+-------------------------------
+-- Dual non-empty list monad --
+-------------------------------
+
+liftNEFun :: (NonEmptyMonad m)
+          => (NonEmpty a -> NonEmpty a) -> m a -> m a
+liftNEFun f = wrap . f . unwrap
+
+-- | Every non-empty 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 DualNonEmptyMonad m a =
+  DualNonEmptyMonad { unDualNonEmptyMonad :: m a }
+ deriving (Functor, Show, Eq)
+
+instance (NonEmptyMonad m) => Applicative (DualNonEmptyMonad m) where
+  pure  = return
+  (<*>) = ap
+
+instance (NonEmptyMonad m) => Monad (DualNonEmptyMonad m) where
+  return = DualNonEmptyMonad . liftNEFun NonEmpty.reverse . return
+  DualNonEmptyMonad m >>= f = DualNonEmptyMonad $ liftNEFun NonEmpty.reverse $
+    liftNEFun NonEmpty.reverse m >>=
+      liftNEFun NonEmpty.reverse . unDualNonEmptyMonad . f
+
+instance (IsNonEmpty (m a)) => IsNonEmpty (DualNonEmptyMonad m a) where
+  type ItemNE (DualNonEmptyMonad m a) = ItemNE (m a)
+  toNonEmpty (DualNonEmptyMonad m)    = toNonEmpty m
+  fromNonEmpty xs                     = DualNonEmptyMonad (fromNonEmpty xs)
+
+instance (NonEmptyMonad m) => NonEmptyMonad (DualNonEmptyMonad m) where
+  wrap   = DualNonEmptyMonad . wrap
+  unwrap = unwrap . unDualNonEmptyMonad
+
+---------------------------------------
+-- Product of Identity and ListMonad --
+---------------------------------------
+
+-- | @'NonEmpty' a@ is isomorphic to the product @(a, [a])@. Thus, we
+-- can define a monadic structure on it by a product of the identity
+-- monad with any list monad. In particular:
+--
+-- @
+-- return x          = IdXList x (return x)
+-- IdXList x m >>= f = IdXList (componentId $ f x) (m >>= componentM . f)
+-- @
+--
+-- where 'return' and '>>=' in definition bodies come from the
+-- transformed monad.
+data IdXList m a = IdXList { componentId :: a, componentM :: m a }
+ deriving (Functor, Show, Eq)
+
+instance (ListMonad m) => Applicative (IdXList m) where
+  pure  = return
+  (<*>) = ap
+
+instance (ListMonad m) => Monad (IdXList m) where
+  return x          = IdXList x (return x)
+  IdXList x m >>= f = IdXList (componentId $ f x) (m >>= componentM . f)
+
+instance (ListMonad m) => IsNonEmpty (IdXList m a) where
+  type ItemNE (IdXList m a)  = a
+  fromNonEmpty (x :| xs)     = IdXList x $ List.Exotic.wrap xs
+  toNonEmpty   (IdXList x m) = x :| List.Exotic.unwrap m
+  
+instance (ListMonad m) => NonEmptyMonad (IdXList m)
+
+---------------------------
+-- The Short Front monad --
+---------------------------
+
+-- | Instances of this class are non-empty list monads for which the
+-- 'ShortFront' construction gives a monad.
+class (NonEmptyMonad m) => HasShortFront m
+
+-- | This is a transformer for a number of monads (instances of the
+-- 'HasShortFront' class), whose return is singleton and join takes
+-- the prefix of length @p + 2@ of the result of the join of the
+-- transformed monad (unless the unit laws require otherwise):
+--
+-- @
+-- joinList xss | 'Control.Monad.List.Exotic.isSingle' xss || all 'Control.Monad.List.Exotic.isSingle' xss = concat xss
+--              | otherwise = take (p + 2) (joinList xss)
+-- @
+--
+-- where @joinList@ in the @otherwise@ branch is the @joinList@ of the transformed monad.
+--
+-- While there are quite a few \"short front\" monads on non-empty
+-- lists, only one such monad on possibly-empty lists is known,
+-- 'Control.Monad.List.Exotic.StutterKeeper' (the short version is
+-- 'Control.Monad.List.Exotic.ShortStutterKeeper').
+newtype ShortFront m (p :: Nat) a = ShortFront { unShortFront :: m a }
+ deriving (Functor, Show, Eq)
+
+instance (HasShortFront m, KnownNat p) => Applicative (ShortFront m p) where
+  pure  = return
+  (<*>) = ap
+
+instance (HasShortFront m, KnownNat p) => Monad (ShortFront m p) where
+  return = ShortFront . return
+  ShortFront m >>= f | isSingle (unwrap m)
+                     = ShortFront $ m >>= unShortFront . f
+                     | nonEmptyAll isSingle
+                         $ unwrap (unwrap . unShortFront . f <$> m)
+                     = ShortFront $ m >>= unShortFront . f
+                     | otherwise
+                     = let p = fromIntegral $ natVal (Proxy :: Proxy p)
+                       in  ShortFront $ liftNEFun (fromList . NonEmpty.take (p + 2))
+                                      $ m >>= unShortFront . f
+
+instance (IsNonEmpty (m a), KnownNat p) => IsNonEmpty (ShortFront m p a) where
+  type ItemNE (ShortFront m p a) = ItemNE (m a)
+  toNonEmpty (ShortFront m) = toNonEmpty m
+  fromNonEmpty xs = ShortFront (fromNonEmpty xs)
+
+instance (HasShortFront m, KnownNat p) => NonEmptyMonad (ShortFront m p) where
+  wrap   = ShortFront . wrap
+  unwrap = unwrap . unShortFront
+
+instance HasShortFront NonEmpty
+
+-- | (?)
+instance HasShortFront Keeper
+
+-- | (?)
+instance HasShortFront OpDiscreteHybridNE
+
+-- | (?)
+instance HasShortFront MazeWalkNE
+
+-- | (?)
+instance (KnownNat n) => HasShortFront (StutterNE n)
+
+-- | (?)
+instance HasShortFront AlphaOmega
+
+instance (HasShortRear m) => HasShortFront (DualNonEmptyMonad m)
+
+---------------------------
+-- The Short Rear monad --
+---------------------------
+
+-- | Instances of this class are non-empty list monads for which the
+-- 'ShortRear' construction gives a monad.
+class (NonEmptyMonad m) => HasShortRear m
+
+-- | Similar to 'ShortFront', but gives a monad if restricted to a
+-- suffix of the length @p + 2@.
+newtype ShortRear m (p :: Nat) a = ShortRear { unShortRear :: m a }
+ deriving (Functor, Show, Eq)
+
+instance (HasShortRear m, KnownNat p) => Applicative (ShortRear m p) where
+  pure  = return
+  (<*>) = ap
+
+nonEmptyTakeRear :: Int -> NonEmpty a -> [a]
+nonEmptyTakeRear p = reverse . NonEmpty.take p . NonEmpty.reverse
+
+instance (HasShortRear m, KnownNat p) => Monad (ShortRear m p) where
+  return = ShortRear . return
+  ShortRear m >>= f | isSingle (unwrap m)
+                    = ShortRear $ m >>= unShortRear . f
+                    | nonEmptyAll isSingle
+                        $ unwrap (unwrap . unShortRear . f <$> m)
+                    = ShortRear $ m >>= unShortRear . f
+                    | otherwise
+                    = let p = fromIntegral $ natVal (Proxy :: Proxy p)
+                      in  ShortRear $ liftNEFun (fromList . nonEmptyTakeRear (p + 2))
+                                    $ m >>= unShortRear . f
+
+instance (IsNonEmpty (m a), KnownNat p) => IsNonEmpty (ShortRear m p a) where
+  type ItemNE (ShortRear m p a) = ItemNE (m a)
+  toNonEmpty (ShortRear m) = toNonEmpty m
+  fromNonEmpty xs = ShortRear (fromNonEmpty xs)
+
+instance (HasShortRear m, KnownNat p) => NonEmptyMonad (ShortRear m p) where
+  wrap   = ShortRear . wrap
+  unwrap = unwrap . unShortRear
+
+instance HasShortRear NonEmpty
+
+-- | (?)
+instance HasShortRear DiscreteHybridNE
+
+-- | (?)
+instance HasShortRear AlphaOmega
+
+instance (HasShortFront m) => HasShortRear (DualNonEmptyMonad m)
diff --git a/test/Control/Monad/List/ExoticSpec.hs b/test/Control/Monad/List/ExoticSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Control/Monad/List/ExoticSpec.hs
@@ -0,0 +1,137 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+module Control.Monad.List.ExoticSpec (spec) where
+
+import Prelude hiding ((<>))
+import Test.Hspec
+import Test.QuickCheck
+import Test.Hspec.Core.QuickCheck (modifyMaxSuccess)
+import Control.Monad.List.Exotic
+import Control.Monad (join)
+import Data.Proxy
+import GHC.Exts (IsList(..))
+
+deriving instance (Arbitrary a) => Arbitrary (GlobalFailure a)
+deriving instance (Arbitrary a) => Arbitrary (MazeWalk a)
+deriving instance (Arbitrary a) => Arbitrary (DiscreteHybrid a)
+deriving instance (Arbitrary a) => Arbitrary (ListUnfold a)
+deriving instance (Arbitrary a) => Arbitrary (Stutter 0 a)
+deriving instance (Arbitrary a) => Arbitrary (Stutter 1 a)
+deriving instance (Arbitrary a) => Arbitrary (Stutter 5 a)
+deriving instance (Arbitrary a) => Arbitrary (StutterKeeper 0 a)
+deriving instance (Arbitrary a) => Arbitrary (StutterKeeper 1 a)
+deriving instance (Arbitrary a) => Arbitrary (StutterKeeper 5 a)
+deriving instance (Arbitrary a) => Arbitrary (StutterStutter 0 0 a)
+deriving instance (Arbitrary a) => Arbitrary (StutterStutter 0 1 a)
+deriving instance (Arbitrary a) => Arbitrary (StutterStutter 1 0 a)
+deriving instance (Arbitrary a) => Arbitrary (StutterStutter 1 1 a)
+deriving instance (Arbitrary a) => Arbitrary (StutterStutter 5 3 a)
+deriving instance (Arbitrary a) => Arbitrary (StutterStutter 3 5 a)
+deriving instance (Arbitrary a) => Arbitrary (Mini a)
+deriving instance (Arbitrary a) => Arbitrary (Odd a)
+deriving instance (Arbitrary a) => Arbitrary (ShortStutterKeeper 0 0 a)
+deriving instance (Arbitrary a) => Arbitrary (ShortStutterKeeper 0 1 a)
+deriving instance (Arbitrary a) => Arbitrary (ShortStutterKeeper 1 0 a)
+deriving instance (Arbitrary a) => Arbitrary (ShortStutterKeeper 1 1 a)
+deriving instance (Arbitrary a) => Arbitrary (ShortStutterKeeper 5 3 a)
+deriving instance (Arbitrary a) => Arbitrary (ShortStutterKeeper 3 5 a)
+
+testMonad :: forall m. (Eq (Item (m Int)), ListMonad m, Arbitrary (m Int),
+                        Arbitrary (m (m (m Int))),
+                        IsList (m Int),
+                        Show (m Int), Show (m (m (m Int))))
+          => String -> Proxy m -> SpecWith ()
+testMonad name _ =
+  describe (name ++ " is a monad") $ do
+    it "left unit:" $ property $
+      \xs -> toList (join (fmap return xs)) == toList ((xs :: m Int)) 
+    it "right unit:" $ property $
+      \xs -> toList (join (return xs))      == toList ((xs :: m Int))
+    modifyMaxSuccess (const 150) $ it "associativity:" $ property $
+      \xsss -> toList (join (join xsss))    == toList (join (fmap join xsss) :: m Int)
+      
+spec :: Spec
+spec = do
+  describe "palindromize" $ do
+    it "palindromizes a non-empty list" $
+      palindromize "abcd" `shouldBe` "abcdcba"
+    it "palindromizes an empty list" $
+      palindromize "" `shouldBe` ""
+      
+  describe "isSingle" $ do
+    it "knows that empty is not a singleton" $
+      isSingle "" `shouldBe` False
+    it "knows that a singleton is a singleton" $
+      isSingle "a" `shouldBe` True
+    it "knows that a long list is not a singleton" $
+      isSingle "ab" `shouldBe` False
+
+  describe "safeLast" $ do
+    it "knows that last of empty is empty" $
+      safeLast "" `shouldBe` ""
+    it "knows that last of non-empty is non-empty" $
+      safeLast "Roy" `shouldBe` "y"
+
+  testMonad  "GlobalFailure"      (Proxy :: Proxy GlobalFailure)
+  describe  "GlobalFailure is ZeroSemigroup" $ do
+    it                                             "x <> eps       ==  eps"
+      $ property $ \(x :: GlobalFailure Int)     -> x <> eps       ==  eps
+    it                                             "eps <> x       ==  eps"
+      $ property $ \(x :: GlobalFailure Int)     -> eps <> x       ==  eps
+    it                                             "(x <> y) <> z  ==  x <> (y <> z)"
+      $ property $ \(x :: GlobalFailure Int) y z -> (x <> y) <> z  ==  x <> (y <> z)
+  testMonad  "MazeWalk"           (Proxy :: Proxy MazeWalk)
+  describe  "MazeWalk is PalindromeAlgebra" $ do
+    it                                        "x <> eps       ==  eps"
+      $ property $ \(x :: MazeWalk Int)     -> x <> eps       ==  eps
+    it                                        "eps <> x       ==  eps"
+      $ property $ \(x :: MazeWalk Int)     -> eps <> x       ==  eps
+    it                                        "(x <> y) <> z  ==  x <> (y <> (x <> z))"
+      $ property $ \(x :: MazeWalk Int) y z -> (x <> y) <> z  ==  x <> (y <> (x <> z))
+  testMonad  "DiscreteHybrid"     (Proxy :: Proxy DiscreteHybrid)
+  describe  "DiscreteHybrid is LeaningAlgebra" $ do
+    it                                              "x <> eps       ==  eps"
+      $ property $ \(x :: DiscreteHybrid Int)     -> x <> eps       ==  eps
+    it                                              "eps <> x       ==  x"
+      $ property $ \(x :: DiscreteHybrid Int)     -> eps <> x       ==  x
+    it                                              "(x <> y) <> z  ==  y <> z"
+      $ property $ \(x :: DiscreteHybrid Int) y z -> (x <> y) <> z  ==  y <> z
+  testMonad  "ListUnfold"         (Proxy :: Proxy ListUnfold)
+  describe  "ListUnfold is SkewedAlgebra" $ do
+    it                                          "x <> eps       ==  eps"
+      $ property $ \(x :: ListUnfold Int)     -> x <> eps       ==  eps
+    it                                          "eps <> x       ==  eps"
+      $ property $ \(x :: ListUnfold Int)     -> eps <> x       ==  eps
+    it                                          "(x <> y) <> z  ==  eps"
+      $ property $ \(x :: ListUnfold Int) y z -> (x <> y) <> z  ==  eps
+  testMonad  "Stutter 1"          (Proxy :: Proxy (Stutter 0))
+  testMonad  "Stutter 2"          (Proxy :: Proxy (Stutter 1))
+  testMonad  "Stutter 5"          (Proxy :: Proxy (Stutter 5))
+  testMonad  "StutterKeeper 0"    (Proxy :: Proxy (StutterKeeper 0))
+  testMonad  "StutterKeeper 1"    (Proxy :: Proxy (StutterKeeper 1))
+  testMonad  "StutterKeeper 5"    (Proxy :: Proxy (StutterKeeper 5))
+  testMonad  "StutterStutter 0 0" (Proxy :: Proxy (StutterStutter 0 0))
+  testMonad  "StutterStutter 0 1" (Proxy :: Proxy (StutterStutter 0 1))
+  testMonad  "StutterStutter 1 0" (Proxy :: Proxy (StutterStutter 1 0))
+  testMonad  "StutterStutter 1 1" (Proxy :: Proxy (StutterStutter 1 1))
+  testMonad  "StutterStutter 5 3" (Proxy :: Proxy (StutterStutter 5 3))
+  testMonad  "StutterStutter 3 5" (Proxy :: Proxy (StutterStutter 3 5))
+  testMonad  "Mini"               (Proxy :: Proxy Mini)
+  testMonad  "Odd"                (Proxy :: Proxy Odd)
+  testMonad  "ShortStutterKeeper 0 0" (Proxy :: Proxy (ShortStutterKeeper 0 0))
+  testMonad  "ShortStutterKeeper 0 1" (Proxy :: Proxy (ShortStutterKeeper 0 1))
+  testMonad  "ShortStutterKeeper 0 1" (Proxy :: Proxy (ShortStutterKeeper 1 0))
+  testMonad  "ShortStutterKeeper 1 1" (Proxy :: Proxy (ShortStutterKeeper 1 1))
+  testMonad  "ShortStutterKeeper 5 3" (Proxy :: Proxy (ShortStutterKeeper 5 3))
+  testMonad  "ShortStutterKeeper 3 5" (Proxy :: Proxy (ShortStutterKeeper 3 5))
diff --git a/test/Control/Monad/List/NonEmpty/ExoticSpec.hs b/test/Control/Monad/List/NonEmpty/ExoticSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Control/Monad/List/NonEmpty/ExoticSpec.hs
@@ -0,0 +1,209 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+module Control.Monad.List.NonEmpty.ExoticSpec (spec) where
+
+import Prelude hiding ((<>))
+import Test.Hspec
+import Test.QuickCheck
+import Test.Hspec.Core.QuickCheck (modifyMaxSuccess)
+import Data.List.NonEmpty (NonEmpty(..))
+import qualified Data.List.NonEmpty as NonEmpty
+import Control.Monad.List.NonEmpty.Exotic
+import Control.Monad.List.Exotic (MazeWalk(..))
+import Control.Monad (join, liftM2)
+import Data.Proxy
+-- import GHC.Exts (IsList(..))
+
+instance (Arbitrary a) => Arbitrary (NonEmpty.NonEmpty a) where
+  arbitrary = liftM2 (:|) (arbitrary :: Gen a) (arbitrary :: Gen [a])
+
+deriving instance (Arbitrary a) => Arbitrary (MazeWalk a)
+
+instance (Arbitrary a, Arbitrary (m a)) =>  Arbitrary (IdXList m a) where
+  arbitrary = liftM2 IdXList (arbitrary :: Gen a) (arbitrary :: Gen (m a))
+
+deriving instance (Arbitrary a, Arbitrary (m a)) => Arbitrary (DualNonEmptyMonad m a)
+deriving instance (Arbitrary a) => Arbitrary (Keeper a)
+deriving instance (Arbitrary a) => Arbitrary (DiscreteHybridNE a)
+deriving instance (Arbitrary a) => Arbitrary (OpDiscreteHybridNE a)
+deriving instance (Arbitrary a) => Arbitrary (MazeWalkNE a)
+deriving instance (Arbitrary a) => Arbitrary (StutterNE 0 a)
+deriving instance (Arbitrary a) => Arbitrary (StutterNE 1 a)
+deriving instance (Arbitrary a) => Arbitrary (StutterNE 2 a)
+deriving instance (Arbitrary a) => Arbitrary (StutterNE 5 a)
+deriving instance (Arbitrary a) => Arbitrary (HeadTails a)
+deriving instance (Arbitrary a) => Arbitrary (HeadsTail a)
+deriving instance (Arbitrary a) => Arbitrary (AlphaOmega a)
+deriving instance (Arbitrary (m a)) => Arbitrary (ShortFront m 0 a)
+deriving instance (Arbitrary (m a)) => Arbitrary (ShortFront m 1 a)
+deriving instance (Arbitrary (m a)) => Arbitrary (ShortFront m 2 a)
+deriving instance (Arbitrary (m a)) => Arbitrary (ShortFront m 5 a)
+deriving instance (Arbitrary (m a)) => Arbitrary (ShortRear m 0 a)
+deriving instance (Arbitrary (m a)) => Arbitrary (ShortRear m 1 a)
+deriving instance (Arbitrary (m a)) => Arbitrary (ShortRear m 2 a)
+deriving instance (Arbitrary (m a)) => Arbitrary (ShortRear m 5 a)
+
+testMonad :: forall m. (Monad m, Eq (m Int), Arbitrary (m Int),
+                        Arbitrary (m (m (m Int))),
+                        Show (m Int), Show (m (m (m Int))))
+          => String -> Proxy m -> SpecWith ()
+testMonad name _ =
+  describe (name ++ " is a monad") $ do
+    it "left unit:" $ property $
+      \xs -> join (fmap return xs) == (xs :: m Int)
+    it "right unit:" $ property $
+      \xs -> join (return xs)      == (xs :: m Int)
+    modifyMaxSuccess (const 100) $ it "associativity:" $ property $
+      \xsss -> join (join xsss)    == (join (fmap join xsss) :: m Int)
+
+spec :: Spec
+spec = do
+
+  testMonad "DualNonEmptyMonad Keeper"  (Proxy :: Proxy (DualNonEmptyMonad Keeper))
+  testMonad "DualNonEmptyMonad DiscreteHybridNE"  (Proxy :: Proxy (DualNonEmptyMonad DiscreteHybridNE))
+  testMonad "IdXList MazeWalk"  (Proxy :: Proxy (IdXList MazeWalk))
+  testMonad "Keeper"  (Proxy :: Proxy HeadTails)
+  describe  "Keeper is XY" $ it "(x <> y) <> z  ==  x <> y" $ property $
+       \(x :: Keeper Int) y z -> (x <> y) <> z  ==  x <> y
+  testMonad "DiscreteHybridNE"  (Proxy :: Proxy HeadTails)
+  describe  "DiscreteHybridNE is YZ" $ it "(x <> y) <> z  ==  y <> z" $ property $
+       \(x :: DiscreteHybridNE Int) y z -> (x <> y) <> z  ==  y <> z
+  testMonad "OpDiscreteHybridNE" (Proxy :: Proxy OpDiscreteHybridNE)
+  describe  "OpDiscreteHybridNE is XZ" $ it "(x <> y) <> z  ==  x <> z" $ property $
+       \(x :: OpDiscreteHybridNE Int) y z -> (x <> y) <> z  ==  x <> z
+  testMonad "MazeWalkNE" (Proxy :: Proxy MazeWalkNE)
+  describe  "MazeWalkNE is PalindromeMagma" $ it "(x <> y) <> z  ==  x <> (y <> (x <> z))" $ property $
+                    \(x :: MazeWalkNE Int) y z -> (x <> y) <> z  ==  x <> (y <> (x <> z))
+  testMonad "StutterNE 0" (Proxy :: Proxy (StutterNE 0))
+  describe  "StutterNE 0 is StutterMagma 0" $ it "(x <> y) <> z  ==  foldr1 (<>) (replicate (0 + 2) x)" $ property $
+                   \(x :: StutterNE 0 Int) y z -> (x <> y) <> z  ==  foldr1 (<>) (replicate (0 + 2) x)
+  testMonad "StutterNE 1" (Proxy :: Proxy (StutterNE 1))
+  describe  "StutterNE 1 is StutterMagma 1" $ it "(x <> y) <> z  ==  foldr1 (<>) (replicate (1 + 2) x)" $ property $
+                   \(x :: StutterNE 1 Int) y z -> (x <> y) <> z  ==  foldr1 (<>) (replicate (1 + 2) x)
+  testMonad "StutterNE 2" (Proxy :: Proxy (StutterNE 2))
+  describe  "StutterNE 2 is StutterMagma 2" $ it "(x <> y) <> z  ==  foldr1 (<>) (replicate (2 + 2) x)" $ property $
+                    \(x :: StutterNE 2 Int) y z -> (x <> y) <> z  ==  foldr1 (<>) (replicate (2 + 2) x)
+  testMonad "StutterNE 5" (Proxy :: Proxy (StutterNE 5))
+  describe  "StutterNE 5 is StutterMagma 5" $ it "(x <> y) <> z  ==  foldr1 (<>) (replicate (5 + 2) x)" $ property $
+                   \(x :: StutterNE 5 Int) y z -> (x <> y) <> z  ==  foldr1 (<>) (replicate (5 + 2) x)
+
+  testMonad "HeadTails"  (Proxy :: Proxy HeadTails)
+  describe  "HeadTails is HeadTailTail" $ do
+    it "equaitons:"
+      $ property $ \(x :: HeadTails Int) y z v w ->
+            x                         ==  htt x x (hd x)
+         && hd (hd x)                 ==  hd x
+         && hd (htt x y z)            ==  hd x
+         && htt x y (hd z)            ==  htt x y (hd y)
+         && htt x y (htt z v w)       ==  htt x y (htt y v w)
+         && htt x (hd y) (hd z)       ==  hd x
+         && htt x (hd y) (htt z v w)  ==  htt x v w
+         && htt x (htt y z v) w       ==  htt x z (htt z v w)
+         && htt (hd x) y z            ==  htt x y z
+         && htt (htt x y z) v w       ==  htt x v w
+  testMonad "HeadsTail"  (Proxy :: Proxy HeadsTail)
+  describe  "HeadsTail is HeadHeadTail" $ do
+    it "equations:"
+      $ property $ \(x :: HeadsTail Int) y z v w ->
+            x                    ==  ht x x
+         && hd' (hd' x)          ==  hd' x
+         && hd' (ht x y)         ==  hd' x
+         && hd' (hht x y z)      ==  hd' x
+         && ht x (hd' y)         ==  hd' x
+         && ht x (ht y z)        ==  ht x z
+         && ht x (hht y z v)     ==  hht x z v
+         && ht (hd' x) y         ==  ht x y
+         && ht (ht x y) z        ==  ht x z
+         && ht (hht x y z) v     ==  ht x v
+         && hht x y (hd' z)      ==  hd' x
+         && hht x y (ht z v)     ==  hht x y v
+         && hht x y (hht z v w)  ==  hht x y (hht y v w)
+         && hht x (hd' y) z      ==  hht x y z
+         && hht x (ht y z) v     ==  hht x y v
+         && hht x (hht y z v) w  ==  hht x y w
+         && hht (hd' x) y z      ==  hht x y z
+         && hht (ht x y) z v     ==  hht x z v
+         && hht (hht x y z) v w  ==  hht x v w
+
+  testMonad "AlphaOmega" (Proxy :: Proxy AlphaOmega)
+
+  testMonad "ShortFront NonEmpty 0" (Proxy :: Proxy (ShortFront NonEmpty 0))
+  testMonad "ShortFront NonEmpty 1" (Proxy :: Proxy (ShortFront NonEmpty 1))
+  testMonad "ShortFront NonEmpty 2" (Proxy :: Proxy (ShortFront NonEmpty 2))
+  testMonad "ShortFront NonEmpty 5" (Proxy :: Proxy (ShortFront NonEmpty 5))
+
+  testMonad "ShortFront Keeper 0" (Proxy :: Proxy (ShortFront Keeper 0))
+  testMonad "ShortFront Keeper 1" (Proxy :: Proxy (ShortFront Keeper 1))
+  testMonad "ShortFront Keeper 2" (Proxy :: Proxy (ShortFront Keeper 2))
+  testMonad "ShortFront Keeper 5" (Proxy :: Proxy (ShortFront Keeper 5))
+
+  testMonad "ShortFront OpDiscreteHybridNE 0" (Proxy :: Proxy (ShortFront OpDiscreteHybridNE 0))
+  testMonad "ShortFront OpDiscreteHybridNE 1" (Proxy :: Proxy (ShortFront OpDiscreteHybridNE 1))
+  testMonad "ShortFront OpDiscreteHybridNE 2" (Proxy :: Proxy (ShortFront OpDiscreteHybridNE 2))
+  testMonad "ShortFront OpDiscreteHybridNE 5" (Proxy :: Proxy (ShortFront OpDiscreteHybridNE 5))
+
+  testMonad "ShortFront MazeWalkNE 0" (Proxy :: Proxy (ShortFront MazeWalkNE 0))
+  testMonad "ShortFront MazeWalkNE 1" (Proxy :: Proxy (ShortFront MazeWalkNE 1))
+  testMonad "ShortFront MazeWalkNE 2" (Proxy :: Proxy (ShortFront MazeWalkNE 2))
+  testMonad "ShortFront MazeWalkNE 5" (Proxy :: Proxy (ShortFront MazeWalkNE 5))
+
+  testMonad "ShortFront (StutterNE 0) 0" (Proxy :: Proxy (ShortFront (StutterNE 0) 0))
+  testMonad "ShortFront (StutterNE 0) 1" (Proxy :: Proxy (ShortFront (StutterNE 0) 1))
+  testMonad "ShortFront (StutterNE 0) 2" (Proxy :: Proxy (ShortFront (StutterNE 0) 2))
+  testMonad "ShortFront (StutterNE 0) 5" (Proxy :: Proxy (ShortFront (StutterNE 0) 5))
+
+  testMonad "ShortFront (StutterNE 1) 0" (Proxy :: Proxy (ShortFront (StutterNE 1) 0))
+  testMonad "ShortFront (StutterNE 1) 1" (Proxy :: Proxy (ShortFront (StutterNE 1) 1))
+  testMonad "ShortFront (StutterNE 1) 2" (Proxy :: Proxy (ShortFront (StutterNE 1) 2))
+  testMonad "ShortFront (StutterNE 1) 5" (Proxy :: Proxy (ShortFront (StutterNE 1) 5))
+
+  testMonad "ShortFront (StutterNE 2) 0" (Proxy :: Proxy (ShortFront (StutterNE 2) 0))
+  testMonad "ShortFront (StutterNE 2) 1" (Proxy :: Proxy (ShortFront (StutterNE 2) 1))
+  testMonad "ShortFront (StutterNE 2) 2" (Proxy :: Proxy (ShortFront (StutterNE 2) 2))
+  testMonad "ShortFront (StutterNE 2) 5" (Proxy :: Proxy (ShortFront (StutterNE 2) 5))
+
+  testMonad "ShortFront (StutterNE 5) 0" (Proxy :: Proxy (ShortFront (StutterNE 5) 0))
+  testMonad "ShortFront (StutterNE 5) 1" (Proxy :: Proxy (ShortFront (StutterNE 5) 1))
+  testMonad "ShortFront (StutterNE 5) 2" (Proxy :: Proxy (ShortFront (StutterNE 5) 2))
+  testMonad "ShortFront (StutterNE 5) 5" (Proxy :: Proxy (ShortFront (StutterNE 5) 5))
+
+  testMonad "ShortFront AlphaOmega 0" (Proxy :: Proxy (ShortFront AlphaOmega 0))
+  testMonad "ShortFront AlphaOmega 1" (Proxy :: Proxy (ShortFront AlphaOmega 1))
+  testMonad "ShortFront AlphaOmega 2" (Proxy :: Proxy (ShortFront AlphaOmega 2))
+  testMonad "ShortFront AlphaOmega 5" (Proxy :: Proxy (ShortFront AlphaOmega 5))
+
+  testMonad "ShortFront (DualNonEmptyMonad DiscreteHybridNE) 0" (Proxy :: Proxy (ShortFront (DualNonEmptyMonad DiscreteHybridNE) 0))
+  testMonad "ShortFront (DualNonEmptyMonad DiscreteHybridNE) 1" (Proxy :: Proxy (ShortFront (DualNonEmptyMonad DiscreteHybridNE) 1))
+  testMonad "ShortFront (DualNonEmptyMonad DiscreteHybridNE) 2" (Proxy :: Proxy (ShortFront (DualNonEmptyMonad DiscreteHybridNE) 2))
+  testMonad "ShortFront (DualNonEmptyMonad DiscreteHybridNE) 5" (Proxy :: Proxy (ShortFront (DualNonEmptyMonad DiscreteHybridNE) 5))
+
+  testMonad "ShortRear NonEmpty 0" (Proxy :: Proxy (ShortRear NonEmpty 0))
+  testMonad "ShortRear NonEmpty 1" (Proxy :: Proxy (ShortRear NonEmpty 1))
+  testMonad "ShortRear NonEmpty 2" (Proxy :: Proxy (ShortRear NonEmpty 2))
+  testMonad "ShortRear NonEmpty 5" (Proxy :: Proxy (ShortRear NonEmpty 5))
+
+  testMonad "ShortRear DiscreteHybridNE 0" (Proxy :: Proxy (ShortRear DiscreteHybridNE 0))
+  testMonad "ShortRear DiscreteHybridNE 1" (Proxy :: Proxy (ShortRear DiscreteHybridNE 1))
+  testMonad "ShortRear DiscreteHybridNE 2" (Proxy :: Proxy (ShortRear DiscreteHybridNE 2))
+  testMonad "ShortRear DiscreteHybridNE 5" (Proxy :: Proxy (ShortRear DiscreteHybridNE 5))
+
+  testMonad "ShortRear AlphaOmega 0" (Proxy :: Proxy (ShortRear AlphaOmega 0))
+  testMonad "ShortRear AlphaOmega 1" (Proxy :: Proxy (ShortRear AlphaOmega 1))
+  testMonad "ShortRear AlphaOmega 2" (Proxy :: Proxy (ShortRear AlphaOmega 2))
+  testMonad "ShortRear AlphaOmega 5" (Proxy :: Proxy (ShortRear AlphaOmega 5))
+
+  testMonad "ShortRear (DualNonEmptyMonad Keeper) 0" (Proxy :: Proxy (ShortRear (DualNonEmptyMonad Keeper) 0))
+  testMonad "ShortRear (DualNonEmptyMonad Keeper) 1" (Proxy :: Proxy (ShortRear (DualNonEmptyMonad Keeper) 1))
+  testMonad "ShortRear (DualNonEmptyMonad Keeper) 2" (Proxy :: Proxy (ShortRear (DualNonEmptyMonad Keeper) 2))
+  testMonad "ShortRear (DualNonEmptyMonad Keeper) 5" (Proxy :: Proxy (ShortRear (DualNonEmptyMonad Keeper) 5))
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
