Add terminating machines

[tel]

As seen here.

data FoldF m a r b
  = FoldF
    { reducer :: r -> a -> m (Either b r)
    , state   :: Either b r
    , output  :: r -> m b
    }

-- | We forget the state variable to make it more composable
data Fold m a b where Fold :: FoldF m a r b -> Fold m a b

[tel]

Ignore the monadic bit, actually. I could never figure out the right place to put it anyway.

data FoldF a r b
  = FoldF
    { reducer :: r -> a -> Either b r
    , state   :: Either b r
    , output  :: r -> b
    }

-- | We forget the state variable to make it more composable
data Fold a b where Fold :: FoldF a r b -> Fold a b

[tel]

type (-'a, +'b) spec = 
  { step : 'a -> 's -> ('b, 's) sum
  ; state : ('b, 's) sum
  ; output : 's -> 'b
  }

type (-_, +_) t = Ex : ('a, 'b, 's) state -> ('a, 'b) t