Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
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