RFC: User injectable evidence

[natefaubion]

Right now, Functor is the only constraint with special consideration for VariantF. Whenever you build a VariantF with inj, it captures the Functor dictionary and keeps it around with the value. Since this is the defining evidence for VariantF, dispatching it is free since we always have the appropriate dictionary on hand. For anything else (Foldable, Traversable, etc) we have to collect all possible dictionaries at the call site, and perform a lookup to dispatch the appropriate dictionary. This is inefficient all around. It would be nice if we could let users inject arbitrary evidence whenever we build a VariantF, and use that to dispatch dictionaries.

The following is an example of some machinery that accomplishes this, but I'd like to get some feedback.

module DictTest where

import Prelude

import Data.Eq (class Eq1, eq1)
import Data.Foldable (class Foldable, foldMap, foldl, foldr)
import Data.Traversable (class Traversable, sequence, traverse)

newtype FunctorDict f =
  FunctorDict
    (forall a b. (a -> b) -> f a -> f b)

data FoldableDict f =
  FoldableDict
    (forall a r. (a -> r -> r) -> r -> f a -> r)
    (forall a r. (r -> a -> r) -> r -> f a -> r)
    (forall a r. Monoid r => (a -> r) -> f a -> r)

data TraversableDict f =
  TraversableDict
    (forall a b m. Applicative m => (a -> m b) -> f a -> m (f b))
    (forall a m. Applicative m => f (m a) -> m (f a))

newtype Eq1Dict f =
  Eq1Dict
    (forall a. Eq a => f a -> f a -> Boolean)

class Gather (f :: Type -> Type) e | e -> f where
  gather :: e f

class Dict (f :: Type -> Type) d e | d e -> f where
  dict :: e f -> d f

data Boxed (e :: (Type -> Type) -> Type) (f :: Type -> Type) a = Boxed (e f) (f a)

box :: forall e f a. Gather f e => f a -> Boxed e f a
box = Boxed gather

instance functorBoxed :: Dict f FunctorDict e => Functor (Boxed e f) where
  map k (Boxed e a) = case dict e of FunctorDict map' -> Boxed e (map' k a)

instance foldableBoxed :: Dict f FoldableDict e => Foldable (Boxed e f) where
  foldr a b (Boxed e c) = case dict e of FoldableDict foldr' _ _ -> foldr' a b c
  foldl a b (Boxed e c) = case dict e of FoldableDict _ foldl' _ -> foldl' a b c
  foldMap a (Boxed e b) = case dict e of FoldableDict _ _ foldMap' -> foldMap' a b

instance traversableBoxed ::
  ( Dict f TraversableDict e
  , Dict f FoldableDict e
  , Dict f FunctorDict e
  ) => Traversable (Boxed e f) where
  traverse a (Boxed e b) = case dict e of TraversableDict traverse' _ -> Boxed e <$> traverse' a b
  sequence (Boxed e a) = case dict e of TraversableDict _ sequence' -> Boxed e <$> sequence' a

instance eq1Boxed :: Dict f Eq1Dict e => Eq1 (Boxed e f) where
  eq1 (Boxed e a) (Boxed _ b) = case dict e of Eq1Dict eq1' -> eq1' a b

---

newtype Evidence f = Evidence
  { functor :: FunctorDict f
  , foldable :: FoldableDict f
  , traversable :: TraversableDict f
  , eq1 :: Eq1Dict f
  }

instance gatherEvidence :: (Traversable f, Eq1 f) => Gather f Evidence where
  gather = Evidence
    { functor: FunctorDict map
    , foldable: FoldableDict foldr foldl foldMap
    , traversable: TraversableDict traverse sequence
    , eq1: Eq1Dict eq1
    }

instance evidenceFunctorDict :: Dict f FunctorDict Evidence where
  dict (Evidence { functor }) = functor

instance evidenceEq1Dict :: Dict f Eq1Dict Evidence where
  dict (Evidence { eq1 }) = eq1

instance evidenceFoldableDict :: Dict f FoldableDict Evidence where
  dict (Evidence { foldable }) = foldable

instance evidenceTraversableDict :: Dict f TraversableDict Evidence where
  dict (Evidence { traversable }) = traversable

The Boxed type just packages up some evidence with some functor. If we extend that with a tag, then we'd have VariantFRep, and we could implement all the instance in terms of the user injected evidence. The smart constructor ensures that it's only every built using gather, which means that we always get the same dictionaries, so they are interchangeable in the case of binary operations like eq1.

/cc @MonoidMusician @joneshf

[joneshf]

What you've written seems pretty fleshed out. What sort of feedback are you looking for?

[natefaubion]

I'm just wondering if anyone can think of any drawbacks or issues with this. I might setup a separate project purescript-typeclass-dicts or something to flesh it out more.