有没有办法"删除"不存储其参数的仿函数部分？

Question

给定一个仿函数(或任何类型的构造函数)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.
• 等等...

我的问题是,如果我们能做到的对面,并创建一个类型,函子的构造函数并使用它的参数.在形式上,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)

Answer 1

我怀疑在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,但我不认为对此有任何明智的定义.