一对函数的数据类型？

Question

我有一个数据类型，它是一对可链接的函数。在伊德里斯这是

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

我希望这在 Haskell 中意味着什么是相当明显的。这是一个广泛使用的构造，也许有名字？

Answer 1

你想ty成为一个存在类型吗？

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

在Data.Profunctor.Composition有

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

这Foo可以在以下方面进行定义

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

还有一个自由类的概念是一个类型对齐的列表；即可链接函数列表

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

可以写成长度为 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

自由类别也可以定义为Free2 Category通过将Category类传递给Free2.. 有点漫不经心的答案

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