Data type that's a pair of functions?

Question

I have a data type that's a pair of chainable functions. In Idris this is

data Foo i o = MkFoo (i -> ty) (ty -> o)

I hope it's fairly obvious what that means in Haskell. Is this a widely used construct, with a name perhaps?

Answer 1

Are you wanting ty to be an existential type?

type Foo :: Cat Type
data Foo i o where
 MkFoo :: (i -> ty) -> (ty -> o) -> Foo i o
                ^^      ^^
                |       |
             does not appear in the result type

---

In Data.Profunctor.Composition there is

type Pro :: Type
type Pro = Type -> Type -> Type

type Procompose :: Pro -> Pro -> Pro
data Procompose pro2 pro1 іn out where
  Procompose :: pro2 xx out -> pro1 іn xx -> Procompose pro2 pro1 іn out

which Foo can be defined in terms of

type Foo :: Cat Type
type Foo = Procompose (->) (->)

                 we quantify `ty` here because it's existential
                                      |
                                      vvvvvvvvv
pattern MkFoo :: forall іn out. () => forall ty. (іn -> ty) -> (ty -> out) -> Foo іn out
pattern MkFoo one two = Procompose two one

There is also the concept of a free category is a type-aligned list; i.e. a list of chainable functions

type (~>) :: Cat (k -> Type)
type f ~> g = (forall x. f x -> g x)

type Quiver :: Type -> Type
type Quiver ob = ob -> ob -> Type

type Cat :: Type -> Type
type Cat ob = Quiver ob

infixr 5 :>>>

type FreeCategory :: Quiver ~> Cat
data FreeCategory cat a b where
 Id     :: FreeCategory cat a a
 (:>>>) :: cat a b -> FreeCategory cat b c -> FreeCategory cat a c

which can be written as a type-aligned list of length 2:

type Foo :: Cat Type
type Foo = FreeCategory (->)

                 we quantify `ty` here because it's existential
                                      |
                                      vvvvvvvvv
pattern MkFoo :: forall іn out. () => forall ty. (іn -> ty) -> (ty -> out) -> Foo іn out
pattern MkFoo one two = one :>>> two :>>> Id

---

Free categories can also be defined as Free2 Category by passing the Category class to Free2.. a bit of a rambly answer

type (~~>) :: Cat (k1 -> k2 -> Type)
type f ~~> g = (forall x. f x ~> g x)

type Free2 :: (Cat ob -> Constraint) -> Quiver ob -> Cat ob
type Free2 cls cat a b = (forall xx. cls xx => (cat ~~> xx) -> xx a b)

type FreeCategory :: Quiver ~> Cat
type FreeCategory cat a b = Free2 Category cat a b