Есть ли способ «удалить» те части функтора, которые не хранят его аргумент?

Question

Учитывая функтор (или любой конструктор типа) f, мы можем получить «версию» этого функтора, которая не содержит значения его аргумента. Мы просто определяем newtype NoArg f = NoArg (f Void). Например:

• NoArg [] это просто пустой список.
• NoArg Maybe - это просто Ничто.
• NoArg (Either e) это просто e.
• NoArg (Identity) - это Void.
• NoArg 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 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, но я не думаю, что для этого есть какое-то разумное определение.