Revision Problems

These revision problems (unlike the exercises) are not assessed. Use them to test your understanding, to challenge yourself, or whatever floats your boat.

Statically checked printf with GADTS

This first question is more like a traditional practice problem than a revision problem, but I thought it would be good to have this here. Credit to Zoltan for writing this question a couple of years ago.

The `printf` function in C takes a format string, and a variable number of arguments. For example, the following piece of code:

 printf("Hey %s, your age is %d\n","Alice",26);
    

will print "Hey Alice, your age is 26". In C, this function has the following type signature:

 int printf(const char *format, ...);
    

The type of the arguments is not checked, you could write `printf("Hey %s\n", 26);`, which would result in a run-time error. There are external tools which can check this, but:

1. the usual problems with external static checkers apply;

2. if you need to write your own function that behaves similarly, you're out of luck.

You can also use the example of string formatting in Python, where it is done using the `%` operator:

`print("Hey %s, your age is %s" % ("Alice", 26))`
    

This is not statically checked at all. Using GADTs, Haskell allows us to write type-safe string formatting and printf functions. These will be statically checked at compile time, using the type checker, and will never result in a run-time error.

We begin by making the following type definition used to represent strings with formatting arguments like are seen in the argument of printf:

data Fmt :: * -> * where
  End :: Fmt ()
  Lit :: String -> Fmt args -> Fmt args
  Str :: Fmt args -> Fmt (String, args)

An example element of this type is the following:

strExample :: Fmt (String, (String, ()))
strExample = Lit "Hello " $ Str $ Lit " what's your favourite colour?" $ Str $ End

Here, we notice that the type of strExample contains two strings, which is precisely what we need to fill in the formatting gaps in this string.

Task 1: Notice that the definition of Fmt is somewhat incomplete, in that the only kind of formatting we can use is %s. Based on above definitions, write a definition for %d, which we'll call Num similar to Str.

Task 2: Write a function format which takes a format string and arguments to its formatting holes and turns it into a string. This function should have the following type:

format :: Fmt args -> args -> String

Task 3: Use the format function written in part 2 to write a printf function fitting the following type signature:

printf :: Fmt a -> a -> IO ()

Functor, Monad and Applicative Instances:

-- 1
newtype MyInt = MyInt Integer

-- 2 (Either a is the type constructor we're looking at)
data Either a b = Left a | Right b

-- 3 (Prod a is the type constructor we're looking at)
data Prod a b = Prod a b

-- 4 
newtype MyString = MyString String

-- 5 (H1 b is the type constructor we're looking at)
data H1 a b = H1 (a -> b)

-- 6 (H2 b is the type constructor we're looking at)
data H2 b a = H2 (a -> b)

-- 7
newtype Ghost a = Ghost Integer

-- 8
newtype Cont r a = Cont ((a -> r) -> r)

-- 9
data RingF a = Zero | One | Inj a | Plus a a | Times a a | Neg a

-- 10
data Hom a = Hom (a -> a)

For this, recall the functor, applicative and monad laws:

Functor laws:
fmap id x = x -- identity
fmap (f . g) x = fmap f (g x) -- composition 

Applicative laws
(pure id <*> v) == v -- Identity
(pure f <*> pure x) == (pure (f x)) -- Homomorphism
(u <*> pure y) == (pure ($ y) <*> u) -- Interchange
(pure (.) <*> u <*> v <*> w) == (u <*> (v <*> w)) -- Composition

Monad laws:
return a >>= f = f a -- left identity 
ma >>= return = ma -- right identity
(ma >>= f) >>= g == ma >>= (\x -> f x >>= g) -- associativity

Arbitrary Instances:

bezout :: Integral b => b -> b -> (b, b)
bezout a b = let (u, v) = go a b 1 0 0 1
             in if a*u + b*v == 1 then (u, v) else (-u, -v) where
    go r 0 u _ v _ = (u, v)
    go r r' u u' v v' = let q = r `quot` r'
                        in go r' (r - q*r') u' (u - q*u') v' (v - q*v')

data SL2Z = SL2Z Integer Integer Integer Integer deriving (Show, Eq)
{
SL2Z a b c d == [ a b ]
                [ c d ]
-}

det :: SL2Z -> Integer
det (SL2Z a b c d) = a*d - b*c