【发布时间】：2016-08-29 08:53:53
【问题描述】：
我最近开始搞乱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 实例时，我基本上只想引入表示单元组合的幻像类型并将其转换为字符串。我现在能想到的所有方法似乎都很冗长。
【问题讨论】：
-
我不认为这可以在当前的 Haskell 中完成。在类型族定义中，我们不允许使用值表达式（具有类型），只能使用类型表达式（具有种类）。因此，我相信我们目前没有办法参考
(+)的价值级别定义。 -
你熟悉Dimensional吗？
-
“我没有理由不能直接使用所有现有的函数”——原因是 Haskell 不是依赖类型的语言。值和类型之间存在分离，这意味着您必须在两个级别之间复制代码并使用单例值之类的繁琐技巧。 The Haskell designers are hard at work on lifting that restriction;同时，您可以考虑使用真正的依赖类型语言，例如 Agda 或 Idris。
-
看起来你真的只是在寻找依赖类型（正如@BenjaminHodgson 所说，Haskell 还没有）。 “还有一种简单的方法可以从类型中获取运行时值吗？”在依赖类型语言中，“类型”和“值”都是简单的术语，即没有区别。但更多表达性的权衡是更多的证明义务——你必须让编译器相信你认为公理的许多事情。
-
@chi 但以下工作：
type family Foo a where { Foo False = Nothing; Foo True = Just () }。所以我们可以清楚地使用值表达式的子集，我只是想知道为什么我们只能使用某些值表达式。
标签： haskell type-families data-kinds