Printf.hs

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

import GHC.TypeLits
import GHC.Types
import Data.Singletons
import Data.Singletons.Prelude

data Format = Lit Symbol | Str | Shown Type

data instance Sing (x :: Format) where
    SLit :: (KnownSymbol s) => Sing s -> Sing (Lit s)
    SStr :: Sing Str
    SShown :: (Show a) => Sing (Shown a)

instance (KnownSymbol s) => SingI (Lit s) where
    sing = SLit sing

instance SingI Str where
    sing = SStr

instance (Show a) => SingI (Shown a) where
    sing = SShown

type family Printf (fmt :: [Format]) :: Type where
    Printf '[] = String
    Printf (Lit s ': fmt) = Printf fmt
    Printf (Str ': fmt) = String -> Printf fmt
    Printf (Shown a ': fmt) = a -> Printf fmt

printf' :: [String] -> Sing fmt -> Printf fmt
printf' ss SNil = concat $ reverse ss
printf' ss (SCons elt elts) = case elt of
    SLit s -> printf' (symbolVal s : ss) elts
    SStr -> \s -> printf' (s : ss) elts
    SShown -> \x -> printf' (show x : ss) elts

-- -- I wish we could write this, and rely on explicit type applications at use sites...
-- printf :: forall fmt. (SingI fmt) => Printf fmt
-- printf = printf' [] (sing :: SingI fmt)

printf :: Sing fmt -> Printf fmt
printf = printf' []

-- -- The type of x is correctly inferred:
-- x :: String -> Int -> String
x = printf @[Lit "Hello, ", Str, Lit ". You have ", Shown Int, Lit " new messages."] sing

-- -- Of course, what we'd really want to write is
-- x = printf @"Hello, %s. You have %d new messages."
-- -- But that's not yet possible; see e.g. http://stackoverflow.com/q/39686354/477476