数据类型是一对函数？

Question

我有一个数据类型，它是一对可链接的函数。在 Idris 中，这是

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

自由类别也可以通过将 Category class 传递给 Free2 来定义为 Free2 Category。有点乱七八糟的回答

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

Answer 2

这可能是另一种反答案。

详细说明@DanielWagner 的评论，如果您定义此类型以便它在 ty 中不被参数化，如 @Iceland_jack 的回答：

{-# LANGUAGE GADTs #-}

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

然后我相信你会发现，从字面上看，你可以用这种类型的值做的唯一有趣的事情就是将两个组件组合起来得到最终的组合函数 i -> o:

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

所以，我认为答案是不，这不是 Haskell 中广泛使用的构造，它没有名称，因为它不能以任何有意义的方式使用，使其不同于仅具有函数 i -> o.

事实上，onlyWayToUseFoo给出了Foo i o和i -> o的一半同构，另一半可以用这个：

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

所以我认为 Foo i o 只是 i -> o.

类型的不必要的复杂表示

我的意思是，我可能遗漏了一些东西，如果有人能证明我的错误，我将不胜感激。

数据类型是一对函数？

Data type that's a pair of functions?

haskell

functional-programming

idris