CODEWITHSUNDEEP
haskellfunctional-programmingidris
joel
joel

Reputation: 7877

Data type that's a pair of functions?

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?

Upvotes: 2

Views: 196

Answers (2)

K. A. Buhr
K. A. Buhr

Reputation: 51119

This is maybe an alternative, anti-answer.

To elaborate on @DanielWagner's comment, if you define this type so that it is not parameterized in ty, as in @Iceland_jack's answer:

{-# LANGUAGE GADTs #-}

data Foo i o where
  Foo :: (i -> ty) -> (ty -> o) -> Foo i o

then I believe you will discover that literally the only interesting thing you can do with a value of this type is compose the two components to get the resulting composed function i -> o:

onlyWayToUseFoo :: Foo i o -> (i -> o)
onlyWayToUseFoo (Foo f g) = g . f

So, I think the answer is no, this is not a widely used construct in Haskell and it does not have a name, because it can't be used in any meaningful way that would make it different from just having a function i -> o.

In fact, onlyWayToUseFoo gives half the isomorphism between Foo i o and i -> o, and you can use this for the other half:

toFoo :: (i -> o) -> Foo i o
toFoo = Foo id

so I think Foo i o is just an unnecessarily complicated representation of the type i -> o.

I mean, I could be missing something, and I would certainly be grateful to anyone who could demonstrate my wrongness.

Upvotes: 2

Iceland_jack
Iceland_jack

Reputation: 7014

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

Upvotes: 6

Related Questions