型安全なPrintf

Printf.hs

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, ConstraintKinds #-}
{-# LANGUAGE TypeFamilies, UndecidableInstances, FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

import GHC.Prim (Constraint)
import Data.Typeable
 
type family All (cx :: * -> Constraint) (xs :: [*]) :: Constraint
type instance All cx '[] = ()
type instance All cx (x ': xs) = (cx x, All cx xs)

data HList (as :: [*]) where
  Nil :: HList '[]
  (:::) :: a -> HList as -> HList (a ': as)
infixr :::

instance (All Show as) => Show (HList as) where
  show Nil = "[]"
  show (x ::: xs) = show x ++ ":" ++ show xs

_d :: Int -> String
_d = show

_s :: String -> String
_s = id

_f :: Float -> String
_f = show

class TextF as bs where
  textf :: HList as -> HList bs -> String

instance (TextF as bs) => TextF (String ': as) bs where
  textf (x ::: xs) y' = x ++ textf xs y'

instance (TextF as bs) => TextF ((x -> String) ': as) (x ': bs) where
  textf (x ::: xs) (y ::: ys) = x y ++ textf xs ys

instance TextF '[] '[] where
  textf _ _ = ""

printf :: (TextF as bs) => HList as -> HList bs -> IO ()
printf a b = putStrLn $ textf a b

main = do
  printf
    ("hello" ::: "world" ::: _d ::: "\n" ::: "number:" ::: _f ::: Nil)
    ((10 :: Int) ::: (1.2402 :: Float) ::: Nil)