我最近开始搞乱DataKinds，以便为算术提供编译时科学单位。我或多或少想出了一种方法来做我想做的事，但我觉得它可能会更干净。
我需要可能为负数（m^-1）的整数，所以我决定使用整数而不是自然数。但事实证明，当你这样做时，:k 5它会给你GHC.Types.Nat带来不符合我需求的东西。我最终改为制作自己的自定义代数整数类型。以及定义与它一起使用的加法和减法类型系列。
但这一切似乎都非常间接，似乎没有充分的理由我不能直接使用所有现有函数在编译时在类型族中操作数据。
基本上我希望基本上自动生成以下内容：
type family (a :: Int) + (b :: Int) :: Int where
-- Should be automatically derivable from (+) applied to Int
这可能吗，如果没有，那为什么不呢？
还有一种简单的方法可以从类型中获取运行时值吗？特别是在为所有这些类型编写Show实例时，我基本上只想引入表示单元组合的幻像类型并将其转换为字符串。我现在能想到的所有方法似乎都非常冗长。