How to fetch type parameters?

Question

This is a data type represents real world physics unit:

import qualified Prelude as P
import Prelude hiding ((+), (*), (/), (-), Int, pi)

data Int = Zero | Succ Int | Pred Int

data Unit :: Int -> Int -> Int -> * where
    U :: Double -> Unit m s kg

(+) :: Unit m s kg -> Unit m s kg -> Unit m s kg
(-) :: Unit m s kg -> Unit m s kg -> Unit m s kg
(*) :: Unit m1 s1 kg1 -> Unit m2 s2 kg2 -> Unit (Plus m1 m2) (Plus s1 s2) (Plus kg1 kg2)
(/) :: Unit m1 s1 kg1 -> Unit m2 s2 kg2 -> Unit (Minus m1 m2) (Minus s1 s2) (Minus kg1 kg2)

and the Show instance:

instance Show (Unit m s kg) where
    show (U a) = show a

In this way, I can only show the value but not the type (is it time or velocity or length type). I wonder how to get the type parameters m, s, kg and then show it?

The full code is here.

Answer 1

You'll need some more extensions:

{-# LANGUAGE PolyKinds, ScopedTypeVariables #-}

PolyKinds turns on more evil type hackery and ScopedTypeVariables allows you to reference type variables bound in instance heads and type signatures, in the definition of a function.

Then we can write the following:

data Proxy a = Proxy

class IntRep (n :: Int) where
    natToInt :: Proxy (n :: Int) -> Integer
instance IntRep Zero where
    natToInt _ = 0
instance (IntRep n) => IntRep (Succ n) where
    natToInt _ = 1 P.+ (natToInt (Proxy :: Proxy n)) 
instance (IntRep n) => IntRep (Pred n) where
    natToInt _ = (natToInt (Proxy :: Proxy n)) P.- 1

Proxy combined with PolyKinds lets you reference n defined in the instance declaration of IntRep. The usual strategy for computation on phantom types is to just use undefined :: t, but undefined has kind * so undefined :: Zero is a kind mismatch. Because you defined Unit as Unit :: Int -> Int -> Int -> * and not Unit :: * -> * -> * -> * this extra misdirection is required.

Finally the Show instance:

instance (IntRep m, IntRep s, IntRep kg) => Show (Unit m s kg) where
    show (U a) = unwords [show a, "m^" ++ u0, "s^" ++ u1, "kg^" ++ u2] 
        where u0 = show $ natToInt (Proxy :: Proxy m) 
              u1 = show $ natToInt (Proxy :: Proxy s)
              u2 = show $ natToInt (Proxy :: Proxy kg)  

and

Prelude> main
0.1 m^1 s^-1 kg^0

Additional reading: http://comments.gmane.org/gmane.comp.lang.haskell.glasgow.user/22159