a polyvariadic function returning a GADT

MkHList.hs

-- in response to https://twitter.com/Iceland_jack/status/1070073876829429760
{-# LANGUAGE AllowAmbiguousTypes, DataKinds, FlexibleInstances, GADTs, InstanceSigs, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators #-}
module Main where
import Test.DocTest

-- The challenge is to define a polymorphic 'mkHList' which can be specialized
-- to all of those types:
--
--     mkList ::                     HList                      '[]
--     mkList ::                d -> HList                (d ': '[])
--     mkList ::           b -> c -> HList           (c ': d ': '[])
--     mkList ::      b -> c -> d -> HList      (b ': c ': d ': '[])
--     mkList :: a -> b -> c -> d -> HList (a ': b ': c ': d ': '[])
--
-- My solution works well with type-inference: we only need to indicate when the
-- argument list terminates, by annotating or inferring that the type of
-- (mkList x y z) is an HList, but we don't need to annotate the length of the
-- list nor the type of its elements.


-- As a warmup, let's implement a polyvariadic 'mkList' which can be specialized
-- as follows:
--
--     mkList ::                     [a]   mkList             =             []
--     mkList ::                a -> [a]   mkList          x4 =          x4:[]
--     mkList ::           a -> a -> [a]   mkList       x3 x4 =       x3:x4:[]
--     mkList ::      a -> a -> a -> [a]   mkList    x2 x3 x4 =    x2:x3:x4:[]
--     mkList :: a -> a -> a -> a -> [a]   mkList x1 x2 x3 x4 = x1:x2:x3:x4:[]
--
-- The obvious recurrence is
--
--     mkList             = []
--     mkList          x4 = x4 : mkList
--     mkList       x3 x4 = x3 : mkList       x4
--     mkList    x2 x3 x4 = x2 : mkList    x3 x4
--     mkList x1 x2 x3 x4 = x1 : mkList x2 x3 x4
--
-- But that doesn't quite work since we cannot easily ask for and apply N
-- arguments at a time. So instead, we let the recursive 'mkList' call ask for
-- its own arguments, and we use nested 'fmap's to prepend our element to the
-- front of the output list.
--
--     mkList    = []
--     mkList x4 =                      (x4:) (mkList ::                [a])
--     mkList x3 =                fmap  (x3:) (mkList ::           a -> [a])
--     mkList x2 =        (fmap . fmap) (x2:) (mkList ::      a -> a -> [a])
--     mkList x1 = (fmap . fmap . fmap) (x1:) (mkList :: a -> a -> a -> [a])

-- |
-- >>> mkList :: [Int]
-- []
-- >>> mkList 1 :: [Int]
-- [1]
-- >>> mkList 1 2 :: [Int]
-- [1,2]
-- >>> mkList 1 2 3 :: [Int]
-- [1,2,3]
-- >>> mkList 1 2 3 4 :: [Int]
-- [1,2,3,4]
class MkList r where
  mkList   :: r
  overList :: ([Int] -> [Int]) -> r -> r

instance a ~ Int => MkList [a] where
  mkList = []
  overList = id

instance (a ~ Int, MkList r) => MkList (a -> r) where
  mkList a = overList (a:) mkList
  overList = fmap . overList


-- All right, let's move on to 'HList's.

data HList as where
  HNil  :: HList '[]
  HCons :: a -> HList as -> HList (a ': as)

-- |
-- >>> putStrLn $ showHList $ HCons "foo" $ HCons () $ HCons 42 $ HCons pi HNil
-- (HCons "foo" (HCons () (HCons 42 (HCons 3.141592653589793 HNil))))
class ShowHList as where
  showHList :: HList as -> String

instance ShowHList '[] where
  showHList HNil = "HNil"

instance (Show a, ShowHList as) => ShowHList (a ': as) where
  showHList (HCons a as) = "(HCons " ++ show a ++ " " ++ showHList as ++ ")"


-- Can we use the same trick as for 'mkList'?
--
--     mkHList    = []
--     mkHList x4 =                      (HCons x4) (mkHList ::                HList      '[])
--     mkHList x3 =                fmap  (HCons x3) (mkHList ::           d -> HList     '[d])
--     mkHList x2 =        (fmap . fmap) (HCons x2) (mkHList ::      c -> d -> HList   '[c,d])
--     mkHList x1 = (fmap . fmap . fmap) (HCons x1) (mkHList :: b -> c -> d -> HList '[b,c,d])
--
-- This looks good, except that when writing the @MkHList (a -> r)@ instance, we
-- cannot simply ask for a @MkHList r@ in our constraints, because our recursive
-- 'mkHList' call would have the wrong type! That is, if we write
--
--     class MkHList r where
--       mkHList r :: r
--
-- Then when 'r' is @a -> b -> c -> HList '[a,b,c]@, stripping off the
-- @(a ->)@ results in @b -> c -> HList '[a,b,c]@, not @b -> c -> HList '[b,c]@.
--
-- My approach is to use an associated type family 'SetIndex' to overwrite the type-level
-- list, making it easy to switch from @b -> c -> HList '[a,b,c]@ to
-- @b -> c -> HList '[b,c]@ using @SetIndex (b -> c -> HList '[a,b,c]) '[b,c]@.
-- I also defined a second type family 'IdealIndex' which maps
-- @b -> c -> HList whatever@ to @'[b, c]@. This way, I can define a 'MkHList'
-- instance for @b -> c -> HList '[a,b,c]@ by implementing a function of type
-- @b -> c -> HList '[b,c]@ (which is easy) instead of implementing a function
-- of type @b -> c -> HList '[a,b,c]@ (which is impossible).

class MkHList r where
  type SetIndex r (as :: [*])
  type IdealIndex r :: [*]
  mkIdeal   :: SetIndex r (IdealIndex r)
  overHList :: (HList as -> HList bs)
            -> SetIndex r as -> SetIndex r bs

-- |
-- The @SetIndex r (IdealIndex r) ~ r@ constraint makes sure that 'mkHList' has
-- a plausible type like @b -> c -> HList '[b,c]@ even though there are also
-- 'MkHList' instances for implausible types like @b -> c -> HList '[a,b,c]@.
--
-- >>> putStrLn $ showHList $ mkHList "foo" () 1 pi
-- (HCons "foo" (HCons () (HCons 1 (HCons 3.141592653589793 HNil))))
mkHList :: forall r. (MkHList r, SetIndex r (IdealIndex r) ~ r) => r
mkHList = mkIdeal @r

instance MkHList (HList rs) where
  type SetIndex (HList rs) as = HList as
  type IdealIndex (HList rs) = '[]

  mkIdeal :: HList '[]
  mkIdeal = HNil

  overHList :: (HList as -> HList bs)
            -> (HList as -> HList bs)
  overHList = id

instance MkHList r => MkHList (a -> r) where
  type SetIndex (a -> r) as = a -> SetIndex r as
  type IdealIndex (a -> r) = a ': IdealIndex r

  mkIdeal :: a -> SetIndex r (a ': IdealIndex r)
  mkIdeal a = overHList @r @(IdealIndex r) (HCons a) (mkIdeal @r)

  overHList :: forall as bs
             . (HList as -> HList bs)
            -> (a -> SetIndex r as)
            -> (a -> SetIndex r bs)
  overHList = fmap . overHList @r


main :: IO ()
main = doctest ["-XDataKinds", "Main.hs"]