haskell - 是否可以通过“remove”函数的不存储参数的部分来实现？

给定一个函子(或任何类型构造函数)f，我们可以得到该函子的“版本”，其中不包含其参数值。我们只定义newtype NoArg f = NoArg (f Void)。例如:

NoArg []只是空列表。

NoArg Maybe没什么。

NoArg (Either e)只是e。

NoArg (Identity)是Void。

NoArg IO是可永久产生效果的IO操作(如服务器)。

Functor f => NoArg (Free f)是Fix f。

等...

我的问题是，我们是否可以做相反的事情，并创建确实使用其参数的Functor的构造函数类型。正式地，Arg :: (* -> *) -> (* -> *)应该使得存在术语forall a. Arg f a -> a或等效的Arg f Void -> Void。例如:

Arg [] a是a类型的非空列表的类型。

Arg Maybe a只是a。

Arg (Either e) a只是a。

Arg Identity a只是a。

Arg IO a您会认为是产生结果的IO操作。但是，由于您没有从IO a到a甚至没有Maybe a的const Nothing的函数，因此可能不是这样。

Functor f => Arg (Free f) a是Free (Arg f) a。

等...

我在想Arg f是嵌入g的函子f的某种“至上”，以便存在一个术语Argful g :: g Void -> Void。

编辑:我想真正的测试将是Arg [] a是NomEmpty a同构，其中

data NonEmpty a = One a | Cons a (NonEmpty a)

最佳答案

我怀疑Haskell中是否有解决方案，但是在具有依赖对和相等类型的语言中是否有一个相当简单的定义。我在下面的伊德里斯工作。

首先，我们说f函子中的两个元素在被()填充后变得相等时具有相同的形状:

SameShape : Functor f => f a -> f b -> Type
SameShape fa fb = (map (const ()) fa = map (const ()) fb)

Arg f a的元素是f a的元素，因此f Void的元素没有相同的形状。

Arg : (f : Type -> Type) -> Functor f => Type -> Type
Arg f a = (fa : f a ** ((fv : f Void) -> SameShape fa fv -> Void))

**表示一个从属对，其中右侧的组件可以引用第一个组件。此定义恰好排除了不包含a的那些值。因此，我们具有所需的属性:

lem : Functor f => Arg f Void -> Void
lem (fv ** p) = p fv Refl

其中Refl证明map (const ()) fv = map (const ()) fv。

这不适用于IO，但是我不希望对此有任何明智的定义。

关于haskell - 是否可以通过“remove”函数的不存储参数的部分来实现？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/54194572/