Как получить параметры типа?

Question

Это тип данных представляет реальный мир блок физики:

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) 

и шоу экземпляра:

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

Таким образом, я могу показать только значение, но не тип (это время или тип скорости или длины). Интересно, как получить параметры типа m, s, kg, а затем показать его?

Полный код here.

Answer 1

Вам потребуется еще несколько расширений:

{-# LANGUAGE PolyKinds, ScopedTypeVariables #-} 

PolyKinds включает более злого типа повозка, запряженная волами и ScopedTypeVariables позволяет ссылаться на переменные типа, связанные с экземпляра головок и сигнатура типа, в определении функции.

Тогда можно записать следующее:

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 в сочетании с PolyKinds позволяет ссылаться n, определенный в объявлении экземпляра IntRep. Обычной стратегией вычисления на фантомных типах является просто использовать undefined :: t, но undefined имеет вид *, поэтому undefined :: Zero - это несовпадение. Поскольку вы определили Unit как Unit :: Int -> Int -> Int -> *, а не Unit :: * -> * -> * -> *, это дополнительное неправильное направление.

Наконец Show экземпляр:

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) 

и

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

Дополнительное чтение: http://comments.gmane.org/gmane.comp.lang.haskell.glasgow.user/22159