type class for covariance in any parameter, not just the first (where all parameters are of kind *)

CovariantN.hs

{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds, TypeOperators #-}

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
 UndecidableInstances, FlexibleContexts #-} -- for the hacky bit

{-# LANGUAGE GADTs #-} -- just for an example

module CovariantN where

import GHC.Prim (Any) -- just for convenience



-- familiar preliminaries
data Proxy (t :: k) = Proxy

data Nat = Z | S Nat

type family Head (ts :: [k]) :: k
type instance Head (t ': ts) = t

type family Tail (ts :: [k]) :: [k]
type instance Tail (t ': ts) = ts



-- generalizes over Functor, Functor2, and so on
class CovariantN (t :: k) where
  covmapN :: VecR (NumArgs (t a)) ps => -- hack! explained below :)
             (a -> b) -> Uncurry t (a ': ps) -> Uncurry t (b ': ps)

-- the special ingredient
data family Uncurry (t :: k) :: [*] -> *

newtype instance Uncurry (t :: *) ps = UCZ t
newtype instance Uncurry (t :: * -> k) ps =
  UCS (Uncurry (t (Head ps)) (Tail ps))

asUCZ f = (\(UCZ x) -> x) . f . UCZ
asUCS f = (\(UCS x) -> x) . f . UCS

-- handy synonyms
asUC1 f = asUCZ (asUCS f)
asUC2 f = asUC1 (asUCS f)

-- I know how to support a closed set of useful other kinds (eg *
-- -> *, or Nat), but I don't see how to make that set
-- user-extensible...



-- wrapping an interface around the Uncurry instances
type family Recurry (t :: k) (ps :: [*]) :: *
class RecurryIso (any :: k) where
  fromUncurry :: Proxy any -> Uncurry (t :: k) ps -> Recurry t ps
  toUncurry   :: Proxy any -> Recurry (t :: k) ps -> Uncurry t ps

asUncurry :: RecurryIso (Any :: k) =>
             (Uncurry (t :: k) ps -> Uncurry (t1 :: k) ps') ->
              Recurry  t       ps -> Recurry  t1       ps'
asUncurry    f = fromUncurry p . f . toUncurry p
  where p = Proxy :: Proxy (Any :: k)
underUncurry :: RecurryIso (Any :: k) =>
                (Recurry  t       ps -> Recurry  t1       ps') ->
                 Uncurry (t :: k) ps -> Uncurry (t1 :: k) ps'
underUncurry f = toUncurry p   . f . fromUncurry p
  where p = Proxy :: Proxy (Any :: k)

type instance Recurry (t :: *) ps = t
type instance Recurry (t :: * -> k) ps = Recurry (t (Head ps)) (Tail ps)

instance RecurryIso (any :: *) where
  fromUncurry _ (UCZ x) = x  ;  toUncurry _   = UCZ
instance RecurryIso (Any :: k) => RecurryIso (any :: * -> k) where
  fromUncurry _ (UCS x) = fromUncurry (Proxy :: Proxy (Any :: k)) x
  toUncurry _           = UCS . toUncurry (Proxy :: Proxy (Any :: k))





-- now we can cleanly make CovariantN instances
instance CovariantN [] where
  covmapN = underUncurry . map
instance CovariantN (,) where
  covmapN f = underUncurry $ \(b, a) -> (f b, a)
instance CovariantN ((,) b) where
  covmapN = underUncurry . fmap

instance CovariantN Either where
  covmapN f = underUncurry $ either (Left . f) Right
instance CovariantN (Either b) where
  covmapN = underUncurry . fmap





-- inferred exampleA :: (Bool -> b) -> (Char, b)
exampleA f = covmapN f `asUC1` ('c', False)



-- exampleB f = covmapN f `asUncurry` ('c', False)
--
--   Could not deduce
--      ((Char, Bool) ~ Recurry k0 t0 ((':) * a ps0))
--   ...
--   The type variables `k0', `t0', `ps0' are ambiguous
--
-- NB the kind is ambiguous; need injective type families
--
-- so we have to explicitly provide asUCZ/asUCS in order to specify
-- the kind



-- vecR is necessary for inference
--
-- inferred exampleC :: (Char -> b) -> (b, Bool)
exampleC f = covmapN f `asUC2` ('c', False)
--
-- that is ill-typed without VecR
--
--   Couldn't match type `Head * ps0' with `Bool'
--   The type variable `ps0' is ambiguous
--
-- this is what VecR solves; without VecR, the required annotations
-- would be overwhelmingly burdensome
--
-- VecR does this by determining the spine of the list from the
-- kind of t



-- polymorphic parameters are fine
--
-- inferred exampleD :: (Num t, Num a) => (a -> b) -> (t, b)
exampleD f = covmapN f `asUC1` (0, 0)



-- VecR is just a synonym for ps ~ NonStrictTakeN n ps
class    (ps ~ NonStrictTakeN n ps) => VecR (n :: Nat) (ps :: [k])
instance (ps ~ NonStrictTakeN n ps) => VecR (n :: Nat) (ps :: [k])

-- NumArgs just counts the number of type expects
type family NumArgs (t :: k) :: Nat
type instance NumArgs (t :: *) = Z
-- the use of Any is not fundamenatally necessary, just concise
type instance NumArgs (t :: kd -> kr) = S (NumArgs (Any :: kr))

-- NonStrictTakeN is functionally equivalent to take, but it
-- crucially produces the result list's spine without "forcing"
-- that of the input list
type family NonStrictTakeN (n :: Nat) (ts :: [k]) :: [k]
type instance NonStrictTakeN Z     ts = '[]
type instance NonStrictTakeN (S n) ts =
  Head ts ': NonStrictTakeN n (Tail ts)





-- you can abstract over the asUC1/asUC2 etc, but the result type
-- is no longer determined by the input type; there's no type for
-- just functions like asUC1, asUC2, etc

{- inferred
exampleE ::
  (CovariantN t1, VecR (NumArgs (t1 a)) ps) =>
  (a -> b)
  -> ((Uncurry t1 (a ': ps)
       -> Uncurry t1 (b ': ps))
      -> (Char, Bool) -> t)
  -> t     -}
exampleE f how = covmapN f `how` ('c', False)

-- to partially recover that information, we can use (`asTypeOf`
-- asUncurry)

{- inferred
exampleF :: (CovariantN t, RecurryIso t,
   (Recurry t (a ': ps) ~ (Char, Bool)),
   VecR (NumArgs (t a)) ps) =>
  (a -> b)
  -> ((Uncurry t (a ': ps) -> Uncurry t (b ': ps))
      -> (Char, Bool) -> Recurry t (b ': ps))
  -> Recurry t (b ': ps)     -}
exampleF f how = (how `asTypeOf` asUncurry) (covmapN f) ('c', False)





-- only requires covariance wrt the first argument
data GADT :: * -> * -> * where
  GADT :: a -> GADT a Int

instance CovariantN GADT where
  covmapN f = underUncurry $ \(GADT a) -> GADT (f a)

-- inferred exampleG :: GADT [Char] Int
exampleG = covmapN show `asUC2` GADT ()