Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.