Is there a way to "remove" the parts of a functor that do not store its argument?

user_1172541 0
Viewed 357

Given a functor (or any type constructor) f, we can get a "version" of that functor that does not contain a value of its argument. We just define newtype NoArg f = NoArg (f Void). For example:

  • NoArg [] is just the empty list.
  • NoArg Maybe is just Nothing.
  • NoArg (Either e) is just e.
  • NoArg (Identity) is Void.
  • NoArg IO is an IO action that produces effects forever (like a server).
  • Functor f => NoArg (Free f) is Fix f.
  • etc...

My question is if we can do the opposite, and create a type of the constructors of a Functor that does use its argument. Formally, Arg :: (* -> *) -> (* -> *) should be such that there is a term forall a. Arg f a -> a or equivalently Arg f Void -> Void. For example:

  • Arg [] a is the type of non empty lists of type a.
  • Arg Maybe a is just a.
  • Arg (Either e) a is just a.
  • Arg Identity a is just a.
  • Arg IO a you would think is IO actions that produce a result. This probably will not be the case though since you there is no function from IO a to a, or even Maybe a that isn't const Nothing.
  • Functor f => Arg (Free f) a is Free (Arg f) a.
  • etc...

I'm thinking Arg f would be some sort of "supremum" of the functors g that embed in f such that there exists a term Argful g :: g Void -> Void.

EDIT: I guess the true test would be for Arg [] a to be isomorphic to NomEmpty a, where

data NonEmpty a = One a | Cons a (NonEmpty a)
type-constructor functor functional-programming haskell types
1 Answers

I doubt there's a solution in Haskell, but there's a fairly simple definition in languages with dependent pairs and equality types. I work in Idris below.

First, we say that two elements in an f functor have the same shape if they become equal after being filled with ():

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

The elements of Arg f a are elements of f a such that there are no elements of f Void with the same shape.

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

** denotes a dependent pair where the component on the right may refer to the first component. This definition excludes exactly those values which don't contain a. So, we have the desired property:

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

where Refl proves map (const ()) fv = map (const ()) fv.

This doesn't work for IO, but I don't expect there's any sensible definition for that.

user_10682320
Related