如何获取类型参数？答案

【问题标题】：How to fetch type parameters?如何获取类型参数？
【发布时间】：2013-10-13 04:20:53
【问题描述】：

这是一个代表现实世界物理单元的数据类型：

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)

和 Show 实例：

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

这样，我只能显示值而不显示类型（是时间还是速度或长度类型）。我想知道如何获取类型参数m、s、kg然后显示出来？

完整代码为here。

【问题讨论】：

标签： haskell type-families data-kinds

【解决方案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 结合使用可以引用IntRep 的实例声明中定义的n。对幻像类型进行计算的常用策略是只使用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

【讨论】：