Functors for the "Generic Extensions to Type Operators"

[CMCDragonkai]

I sometimes find it easier to understand if I relate the PFPL to equivalent constructs in Haskell.

Regarding today's meeting for page 123. We have a 5 polynomial type operators. Here are some equivalences I've found:

For 14.3.a:

map{t.t}(x.e')(e) -> [e/x]e'

> import Data.Functor.Identity
> instance (Show a) => Show (Identity a) where
> |     show (Identity a) = "Identity " ++ show a
> |
> fmap (\x -> x + 1) (Identity 3)
Identity 4
> :info Identity
newtype Identity a = Identity {runIdentity :: a}
        -- Defined in ‘Data.Functor.Identity’
instance Show a => Show (Identity a)
  -- Defined at <interactive>:24:10
instance Monad Identity -- Defined in ‘Data.Functor.Identity’
instance Functor Identity -- Defined in ‘Data.Functor.Identity’

For 14.3b:

map{t.unit}(x.e')(e) -> e

> import Data.Proxy
> fmap (\x -> x) Proxy
Proxy
it :: Proxy b
> :info Proxy
type role Proxy phantom
data Proxy (t :: k) = Proxy
        -- Defined in ‘Data.Proxy’
instance Bounded (Proxy s) -- Defined in ‘Data.Proxy’
instance Enum (Proxy s) -- Defined in ‘Data.Proxy’
instance Eq (Proxy s) -- Defined in ‘Data.Proxy’
instance Monad Proxy -- Defined in ‘Data.Proxy’
instance Functor Proxy -- Defined in ‘Data.Proxy’
instance Ord (Proxy s) -- Defined in ‘Data.Proxy’
instance Read (Proxy s) -- Defined in ‘Data.Proxy’
instance Show (Proxy s) -- Defined in ‘Data.Proxy’

There used to be a Data.Unit in category-extras package, but it was removed.

For 14.3c:

map{t.tau1 * tau2}(x.e')(e) -> <map{t.tau1}(x.e')(e.l),map{t.tau2}(x.e')(e.r)>

Unknown. Originally I thought it was a tuple. But it isn't. Also this is close data Pair a = Pair a a but it doesn't exactly match {t.tau1 * tau2}, it would be more like {t.t * t}.

For 14.3d:

map{t.void}(x.e')(e) -> abort(e)

Could be Data.Void, but it's not an instance of the Functor type class. Also I couldn't make it an instance of Functor because the kind is * and Functor needs a kind of * -> *.

> import Data.Void
> instance Functor Void where
> |     fmap _ v = absurd v
> |
    The first argument of ‘Functor’ should have kind ‘* -> *’,
      but ‘Void’ has kind ‘*’
    In the instance declaration for ‘Functor Void’

The closest thing to the same behaviour is...

> fmap (\x -> x) undefined
*** Exception: Prelude.undefined

For 14.3e:

map{t.tau1 + tau2}(x.e')(e) -> case e { l.x1 -> l.map{t.tau1}(x.e')(x1) | r.x2 -> r.map{t.tau2}(x.e')(x2) }

Not sure, could it be the Either functor?

[thsutton]

For 14.3c: you probably want something like

data Prod u v t = Prod (u t, v t)

instance (Functor u, Functor v) => Functor (Prod u v) where
  fmap f (Prod (l, r)) = Prod (fmap f l, fmap f r)

[thsutton]

Or maybe implementing map in terms of bimap would make the intention clearer:

type Prod u v t = (u t, v t)

instance (Functor u, Functor v) => Functor (Prod u v) where
    fmap f = bimap (fmap f) (fmap f)

[CMCDragonkai]

@thsutton

Oh that's really nice. I wonder what the usecase for such a functor could be? Is the list functor more general or length 2 vector functors.

[thsutton]

It's the {..} parameter which should be the type for the Functor instance, so for 14.3d you need something like t.void, not void:

type Voidish a = Void

instance Functor Voidish where 
    fmap f v = absurd v

[thsutton]

@CMCDragonkai In this case (the products) we have three functor instances (ignoring any thing "inside" the u and v):

• The functor to the left
• The functor to the right
• The functor of the pair

In a list or (properly) a vector we'd have two:

• The functor for elements
• The functor of the structure

If "more general" means "can be correctly applied to more things" then the former is more general because we can always choose u and v to be identical and, thus, subsume the 2-vector case.

[jberthold]

How about this definition for 14.[13]e

-- | Sum type with two constructors (l and r prefix)
data Sum a b t = L (a t) | R (b t) deriving (Eq, Show)

instance (PolyFunc tau1, PolyFunc tau2) -- 14.1e, premises
    => PolyFunc (Sum tau1 tau2)
    where pfmap f e
              = case e of                -- 14.3e. Confusing part is
                  L x1 -> L (pfmap f x1) -- that the target type is
                  R x2 -> R (pfmap f x2) -- again the same sum type

I got distracted and wrote all rules in a file here:
https://gist.github.com/jberthold/0f090e20d85abc7a3a4377ce358e3fd4

[rowandavies]

@jberthold I think I agree with the revision @thsutton made earlier to use type definitions instead of data, since the intention in PFPL is that applying a type operator like Prod or Sum yields an ordinary (already existing) product type or sum type.

So, I guess Either is the pre-existing Haskell sum type, and then:

type Sum a b t = Either (a t) (b t)

Also, I added a comment to your gist - basically I think case v of { } is closer to the PFPL abort(v).

[mjhopkins]

It's perhaps more common (and a little nicer) in Haskell land to use infix operators :+: and :*: for sum and product of functors.

[thsutton]

Was I on crack yesterday? None of the synonym stuff works today. :-/

[jberthold]

@mjhopkins True, infix constructors would be closer to the book as well. However, note that I am not switching on any Haskell extensions. :-)

EDIT: by "note" I mean "go on a network that does allow you to see..." :-S

[mjhopkins]

@jberthold 😄