Manifold.hs

-- | A manifold is a locally-euclidean space.
--
-- Formally, a manifold is a set @x@, together with a set @d@ of /direction
-- vectors/ and a rule @'step' :: (Signed d, x) -> x@ defining how the
-- direction vectors can be used to move around short distances on the
-- manifold. Each manifold has a /dimension/, which is the cardinality of
-- its set of direction vectors.
--
-- Instances are expected to satisfy the following laws:
--
-- prop> \d x -> step (Negative d) . step (Positive d) $ x == x
-- prop> \d x -> step (Positive d) . step (Negative d) $ x == x
-- prop> \d x -> step (Positive d) x /= x
-- prop> \d x -> step (Negative d) x /= x
--
-- Additionally, 'step' should be a continuous function.
--
-- Note that instances __do not__ necessarily satisfy the /square law/:
--
-- @
--     step (Negative d2)
--       . step (Negative d1)
--       . step (Positive d2)
--       . step (Positive d1)
--       $ x === x
-- @
--
-- A manifold that does satisfy such a law is called /flat/. For example:
-- a plane is flat, a torus is flat, a sphere is not flat.
class Manifold d x where
  step :: Signed d -> x -> x

data Signed a = Negative a | Positive a

-- | Technically manifolds are continuous, not discrete. Ignoring issues
-- of continuity, the Integers forms a one-dimensional manifold.
instance Manifold () Integer where
  step (Negative _) x = x - 1
  step (Positive _) x = x + 1

-- | The product of two manifolds is a manifold in a canonical way.
instance (Manifold dx x, Manifold dy y) => Manifold (Either dx dy) (x, y) where
  step (Negative (Left dx)) (x, y) = (step (Negative dx) x, y)
  step (Positive (Left dx)) (x, y) = (step (Positive dx) x, y)
  step (Negative (Right dy)) (x, y) = (x, step (Negative dy) y)
  step (Positive (Right dy)) (x, y) = (x, step (Positive dy) y)

-- | Follow a path along a manifold.
track :: Manifold d x => [Signed d] -> x -> x
track = appEndo . foldMap (Endo . step)