hell with type-level map

good.hs

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}

module Data.HList
  ( HList(..)
  , TypeMap
  ) where

import Data.Kind (Type)
import Data.Maybe (fromJust, fromMaybe)

infixr 5 :>
data HList :: ([Type] -> Type) where
  (:>) :: a -> HList as -> HList (a ': as)
  HNil :: HList '[]

instance Show (HList '[]) where
  show HNil = "HNil"

instance (Show a, Show (HList as)) => Show (HList (a ': as)) where
  show (x :> xs) = show x <> " :> " <> show xs

class TypeMappable (f :: Type -> Type) (as :: [Type]) where
  type TypeMap f as :: [Type]
  hinject :: (forall a . a -> f a) -> HList as -> HList (TypeMap f as)
  hextract :: (forall a . f a -> a) -> HList (TypeMap f as) -> HList as

instance TypeMappable f '[] where
  type TypeMap _ '[] = '[]
  hinject _ HNil = HNil
  hextract _ HNil = HNil

instance TypeMappable f as => TypeMappable f (a ': as) where
  type TypeMap f (a ': as) = f a ': TypeMap f as
  hinject f (x :> xs) = f x :> hinject f xs
  hextract f (x :> xs) = f x :> hextract f xs

justify :: HList as -> HList (TypeMap Maybe as) 
justify HNil = HNil
justify (x :> xs) = Just x :> justify xs

unjustify :: TypeMappable Maybe as => HList (TypeMap Maybe as) -> HList as
unjustify = hextract fromJust

good_nat_trans.hs

{-# LANGUAGE AllowAmbiguousTypes, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}
{-# LANGUAGE KindSignatures, MultiParamTypeClasses, RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators #-}

module Data.HList
  ( HList(..)
  , TypeMappable(..)
  , TypeNatTrans(..)
  , TypeTraversable(..)
  ) where

import Data.Kind (Type)
import Data.Maybe (fromJust, fromMaybe, maybeToList)

infixr 5 :>
data HList :: ([Type] -> Type) where
  (:>) :: a -> HList as -> HList (a ': as)
  HNil :: HList '[]

instance Show (HList '[]) where
  show HNil = "HNil"

instance (Show a, Show (HList as)) => Show (HList (a ': as)) where
  show (x :> xs) = show x <> " :> " <> show xs

class TypeMappable (f :: Type -> Type) (as :: [Type]) where
  type TypeMap f as :: [Type]
  hinject :: (forall a . a -> f a) -> HList as -> HList (TypeMap f as)
  hextract :: (forall a . f a -> a) -> HList (TypeMap f as) -> HList as

instance TypeMappable f '[] where
  type TypeMap _ '[] = '[]
  hinject _ HNil = HNil
  hextract _ HNil = HNil

instance TypeMappable f as => TypeMappable f (a ': as) where
  type TypeMap f (a ': as) = f a ': TypeMap f as
  hinject f (x :> xs) = f x :> hinject f xs
  hextract f (x :> xs) = f x :> hextract f xs

class (TypeMappable f as, TypeMappable g as) => TypeNatTrans (f :: Type -> Type) (g :: Type -> Type) (as :: [Type]) where
  hmap :: TypeMappable g as => (forall a . f a -> g a) -> HList (TypeMap f as) -> HList (TypeMap g as)

instance TypeNatTrans f g '[] where
  hmap _ HNil = HNil

instance TypeNatTrans f g as => TypeNatTrans f g (a ': as) where
  hmap f (x :> xs) = f x :> hmap @f @g @as f xs

class (TypeMappable f as, Monad f) => TypeTraversable f as where
  hsequence :: HList (TypeMap f as) -> f (HList as)

instance Monad f => TypeTraversable f '[] where
  hsequence HNil = pure HNil

instance TypeTraversable f as => TypeTraversable f (a ': as) where
  hsequence (x :> xs) = (:>) <$> x <*> hsequence xs

justify :: HList as -> HList (TypeMap Maybe as) 
justify HNil = HNil
justify (x :> xs) = Just x :> justify xs

unjustify :: TypeMappable Maybe as => HList (TypeMap Maybe as) -> HList as
unjustify = hextract fromJust

allJust :: TypeTraversable Maybe as => HList (TypeMap Maybe as) -> Maybe (HList as)
allJust = hsequence

theWhat :: Maybe (HList [Integer, Integer, Integer])
theWhat = allJust $ Just 3 :> Just 2 :> Just 1 :> HNil

listed :: forall (as :: [Type])
        . TypeNatTrans Maybe [] as
       => HList (TypeMap Maybe as)
       -> HList (TypeMap [] as)
-- awkward 
listed = hmap @_ @_ @as maybeToList

theWho :: HList [[Integer], [String], [Bool]]
-- soooo awkward
theWho = listed @[Integer, String, Bool] $
  Just 3 :> Nothing :> Just True :> HNil

good_sequence.hs

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}

module Data.HList
  ( HList(..)
  , TypeMap
  ) where

import Data.Kind (Type)
import Data.Maybe (fromJust, fromMaybe)

infixr 5 :>
data HList :: ([Type] -> Type) where
  (:>) :: a -> HList as -> HList (a ': as)
  HNil :: HList '[]

instance Show (HList '[]) where
  show HNil = "HNil"

instance (Show a, Show (HList as)) => Show (HList (a ': as)) where
  show (x :> xs) = show x <> " :> " <> show xs

class TypeMappable (f :: Type -> Type) (as :: [Type]) where
  type TypeMap f as :: [Type]
  hinject :: (forall a . a -> f a) -> HList as -> HList (TypeMap f as)
  hextract :: (forall a . f a -> a) -> HList (TypeMap f as) -> HList as

instance TypeMappable f '[] where
  type TypeMap _ '[] = '[]
  hinject _ HNil = HNil
  hextract _ HNil = HNil

instance TypeMappable f as => TypeMappable f (a ': as) where
  type TypeMap f (a ': as) = f a ': TypeMap f as
  hinject f (x :> xs) = f x :> hinject f xs
  hextract f (x :> xs) = f x :> hextract f xs

class (TypeMappable f as, Monad f) => TypeTraversable f as where
  hsequence :: HList (TypeMap f as) -> f (HList as)

instance Monad f => TypeTraversable f '[] where
  hsequence HNil = pure HNil

instance TypeTraversable f as => TypeTraversable f (a ': as) where
  hsequence (x :> xs) = (:>) <$> x <*> hsequence xs

justify :: HList as -> HList (TypeMap Maybe as) 
justify HNil = HNil
justify (x :> xs) = Just x :> justify xs

unjustify :: TypeMappable Maybe as => HList (TypeMap Maybe as) -> HList as
unjustify = hextract fromJust

allJust :: TypeTraversable Maybe as => HList (TypeMap Maybe as) -> Maybe (HList as)
allJust = hsequence

theWhat :: Maybe (HList [Integer, Integer, Integer])
theWhat = allJust $ Just 3 :> Just 2 :> Just 1 :> HNil

nogood.hs

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators #-}
{-# LANGUAGE TypeApplications, TypeFamilies #-}

module Data.HList
  ( HList(..)
  , TypeMap
  ) where

import Data.Kind (Type)
import Data.Proxy (Proxy(..))

infixr 5 :>
data HList :: ([Type] -> Type) where
  (:>) :: a -> HList as -> HList (a ': as)
  HNil :: HList '[]

type family TypeMap (_f :: Type -> Type) (_a :: [Type]) :: [Type] where
  TypeMap _ '[] = '[]
  TypeMap f (t ': ts) = f t ': TypeMap f ts

instance Show (HList '[]) where
  show HNil = "HNil"

instance (Show a, Show (HList as)) => Show (HList (a ': as)) where
  show (x :> xs) = show x <> " :> " <> show xs

justify :: HList as -> HList (TypeMap Maybe as) 
justify HNil = HNil
justify (x :> xs) = Just x :> justify xs

unmaybefy :: HList as -> HList (TypeMap Maybe as) -> HList as
unmaybefy HNil HNil = HNil
unmaybefy (x :> xs) (Nothing :> ys) = x :> unmaybefy xs ys
unmaybefy (_ :> xs) (Just y :> ys) = y :> unmaybefy xs ys

{- why can't I write this?
unjustify :: HList (TypeMap Maybe as) -> HList as
unjustify HNil = HNil
unjustify (Nothing :> _) = error "naughty!"
unjustify (Just y :> ys) = y :> unjustify ys
-}

{- or, I don't know, something like this at least?
unjustify :: Proxy as -> HList (TypeMap Maybe as) -> HList as
unjustify (Proxy :: Proxy '[]) HNil = HNil
unjustify _ (Nothing :> _) = error "naughty!"
unjustify _ (Just y :> ys) = y :> unjustify Proxy ys
-}

ugly.hs

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators #-}
{-# LANGUAGE AllowAmbiguousTypes, TypeApplications, TypeFamilies #-}

module Data.HList
  ( HList(..)
  , TypeMap
  ) where

import Data.Functor.Identity (Identity(..))
import Data.Kind (Type)

infixr 5 :>
data HList :: ([Type] -> Type) where
  (:>) :: a -> HList as -> HList (a ': as)
  HNil :: HList '[]

instance Show (HList '[]) where
  show HNil = "HNil"

instance (Show a, Show (HList as)) => Show (HList (a ': as)) where
  show (x :> xs) = show x <> " :> " <> show xs

infixr 0 ~>
type f ~> g = forall a . f a -> g a

type family TypeMap (_f :: Type -> Type) (_a :: [Type]) :: [Type] where
  TypeMap _ '[] = '[]
  TypeMap f (t ': ts) = f t ': TypeMap f ts

{- the fundamental problem is shown here
hmap :: forall (as :: [Type]) (f :: Type -> Type) (g :: Type -> Type)
      . (f ~> g) -> HList (TypeMap f as) -> HList (TypeMap g as)
hmap _ HNil = HNil
hmap f (x :> xs) = f x :> hmap f xs
-}