{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE GADTs, TypeFamilies, UndecidableInstances #-}

-- Derivation of progressively simpler type-safe printf
module Undp where

import Prelude hiding ((^))

-- A sample format string, for C printf
fmtC :: String
fmtC = "The value of %c is %d"

data Desc a where
    LIT  :: String -> Desc ()
    INT  :: Desc Int
    CHAR :: Desc Char
    (:^) :: Desc a -> Desc b -> Desc (a,b)

-- A parsed format descriptor, as a GADT
fmtG = LIT "The value of " :^ CHAR :^ LIT " is " :^ INT
-- fmtG :: Desc ((((), Char), ()), Int)

type PS a = PFormat a String
printf :: Desc a -> PS a

-- The non-dependent type function to compute the type of 
-- the type-safe printf from the type annotation of the descriptor
type family PFormat a w :: *
type instance PFormat () w    = w
type instance PFormat Int w   = Int -> w
type instance PFormat Char w  = Char -> w
type instance PFormat (a,b) w = PFormat a (PFormat b w)

-- The implementation of the type-safe printf to match the above
-- signature
printf desc = interp desc id

-- Compositional interpreter
interp :: Desc a -> (String -> w) -> PFormat a w
interp (LIT str)  = \k -> k str
interp INT        = \k -> k . show
interp CHAR       = \k -> k . \c -> [c]
interp (x :^ y)   = \k -> interp x (\sx -> interp y (\sy -> k (sx ++ sy)))


tG = printf fmtG
tGr = printf fmtG 'x' 1
-- "the value of x is 1"

-- The next step: naming the applications of interp to primitive descriptors

lit :: String -> (String -> w) -> w   -- cf. PFormat () w  = w
lit str = \k -> k str                 -- which is, interp (LIT str)

int :: (String -> w) -> (Int -> w)    -- cf. PFormat Int w = Int -> w 
int = \k -> k . show                  -- which is, interp INT

char :: (String -> w) -> (Char -> w)  -- cf. PFormat Char w = Int -> w 
char = \k -> k . \c -> [c]            -- which is, interp CHAR

-- The defining equality for (^) is
--    interp (desc1 :^ desc2) === (interp desc1) ^ (interp desc2)
(^)  :: ((String -> t1) -> t) -> ((String -> t2) -> t1) -> (String -> t2) -> t
(^) x y = \k -> x (\sx -> y (\sy -> k (sx ++ sy)))

-- compare the type of (^) with the composition rule for the 
-- effect system for shift

printf' idesc = idesc id		-- compare with printf above
                                        -- (interp desc) became desc
-- The interpreted descriptor: interp fmtG
fmtI = lit "The value of " ^ char ^ lit " is " ^ int
-- fmtI :: (String -> w) -> Char -> Int -> w

tI = printf' fmtI
-- tI :: Char -> Int -> String

tIr = printf' fmtI 'x' 3
-- "The value of x is 3"