Create a gist now

Instantly share code, notes, and snippets.

type class for covariance in any parameter, not just the first (where all parameters are of kind *)
{-# 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 ()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment