wsp*_*pbr 5 haskell type-level-computation
我正在尝试从类型级别的值中生成术语级别的值。我有以下代码
\nclass Term a where\n type family Result a :: Type\n term :: Result a\n\ninstance (KnownSymbol s) => Term s where\n type instance Result s = String\n term = symbolVal (Proxy @s)\n\ninstance (KnownNat n) => Term n where\n type instance Result n = Integer\n term = natVal (Proxy @n)\n这工作得很好：
\n>>> :t term @"hello"\nterm @"hello" :: String\n>>> term @"hello"\n"hello"\n我如何在类型级别列表上传播这个想法？当我尝试这样的事情时
\ninstance Term \'[] where\n type instance Result (\'[] :: [a]) = [a]\n term = []\n\ninstance (Term a, Term as) => Term (a \': as) where\n type instance Result (a \': as) = Result a \': Result as\n term = term @a : term @as\nGHC 表示 RHS 具有Result (a \': as)类型 [*]，但 atype是预期的。
\xe2\x80\xa2 Expected a type, but \xe2\x80\x98Result a : Result as\xe2\x80\x99 has kind \xe2\x80\x98[*]\xe2\x80\x99\n \xe2\x80\xa2 In the type \xe2\x80\x98Result a : Result as\xe2\x80\x99\n In the type instance declaration for \xe2\x80\x98Result\xe2\x80\x99\n In the instance declaration for \xe2\x80\x98Term (a : as)\xe2\x80\x99\n我只有一个可以编译的解决方案，但它预计仅评估第一个元素：
\ninstance (Term a, Term as) => Term (a \': as) where\n type instance Result (a \': as) = [Result a]\n term = [term @a]\n>>> term @\'["hello", "world"]\n["hello"]\n是否可以递归地将类型级列表转换为术语？
\n完整代码：
\n{-# LANGUAGE TypeApplications #-}\n{-# LANGUAGE TypeFamilies #-} \n{-# LANGUAGE TypeOperators #-} \n{-# LANGUAGE PolyKinds #-}\n{-# LANGUAGE AllowAmbiguousTypes #-}\n{-# LANGUAGE FlexibleInstances #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n\nmodule Term where\n\nimport Data.Kind\nimport Data.Proxy\nimport GHC.TypeLits\n\nclass Term a where\n type family Result a :: Type\n term :: Result a\n\ninstance (KnownSymbol s) => Term s where\n type instance Result s = String\n term = symbolVal (Proxy @s)\n\ninstance (KnownNat n) => Term n where\n type instance Result n = Integer\n term = natVal (Proxy @n)\n\ninstance Term \'[] where\n type instance Result (\'[] :: [a]) = [a]\n term = []\n\ninstance (Term a, Term as) => Term (a \': as) where\n type instance Result (a \': as) = Result a \': Result as\n term = term @a : term @as\n当 GHC 抱怨时：
\n\xe2\x80\xa2 Expected a type, but \xe2\x80\x98Result a : Result as\xe2\x80\x99 has kind \xe2\x80\x98[*]\xe2\x80\x99\n\xe2\x80\xa2 In the type \xe2\x80\x98Result a : Result as\xe2\x80\x99\n In the type instance declaration for \xe2\x80\x98Result\xe2\x80\x99\n In the instance declaration for \xe2\x80\x98Term (a : as)\xe2\x80\x99\n问题是Result应该给我们返回类型term，所以这应该是术语级列表的类型（这将是 kind Type，或者*在旧的命名法中1）。然而，我们显然有一个类型级列表的表达式（它是一种类型，[*]因为Result a必须是Type，与 相同*）。
事实上，我们希望在这里根据类型级列表是否为 kind或Result来生成[Integer]或。我们实际上不想根据实际情况进行递归构造。那么让我们将其更改为：[String][Nat][Symbol]Result (a \': as)as
instance (Term a, Term as) => Term (a \': as) where\n type instance Result (a \': as) = [Result a]\n term = term @a : term @as\n现在我们的错误是：
\n\xe2\x80\xa2 Couldn\'t match expected type \xe2\x80\x98[Result a1]\xe2\x80\x99\n with actual type \xe2\x80\x98Result as\xe2\x80\x99\n\xe2\x80\xa2 In the second argument of \xe2\x80\x98(:)\xe2\x80\x99, namely \xe2\x80\x98term @as\xe2\x80\x99\n In the expression: term @a : term @as\n In an equation for \xe2\x80\x98term\xe2\x80\x99: term = term @a : term @as\n啊哈。我们实际上并没有保证 GHC 满意，这Result as将是一种Result a可以附加的列表。据 GHC 所知，这是两个独立实例对类型族的两次独立调用，没有理由一个实例总是返回一个包含另一个实例结果的类型。但从我们真正想要的实例中我们知道，这实际上总是成立，所以也许我们可以添加等式约束？2
instance (Term a, Term as, Result as ~ [Result a]) => Term (a \': as) where\n type instance Result (a \': as) = [Result a]\n term = term @a : term @as\n现在根本没有编译器错误了！让我们尝试一下：
\n>>> term @[1, 2, 3]\n\n<interactive>:25:1: error:\n \xe2\x80\xa2 Couldn\'t match type \xe2\x80\x98Nat\xe2\x80\x99 with \xe2\x80\x98Integer\xe2\x80\x99\n arising from a use of \xe2\x80\x98term\xe2\x80\x99\n \xe2\x80\xa2 In the expression: term @[1, 2, 3]\n In an equation for \xe2\x80\x98it\xe2\x80\x99: it = term @[1, 2, 3]\n嗯，这并不完全是我们所期望的。
\n这个问题花了我一段时间才弄清楚，但问题出在 的 基本实例中Term \'[]，而不是递归实例中。
type instance Result (\'[] :: [a]) = [a]\n这表示term应用于空类型级别列表的是包含与类型级别列表中相同类型的术语级别列表。当您直接使用 时它会起作用term @\'[]，因为类型级别的空列表是多类的（就像术语级别的空列表是多态的一样）。它可以是我们想要的任何类型的类型级别列表。因此，如果我们在术语级别获取生成的空列表并将其输入到[Bool]预期 a 的上下文中，GHC 将尽职尽责地推断我们一定一直在做term @(\'[] :: [Bool])。
但是，当从非空列表实例中使用这个空列表实例时，我们没有使用文字 \'[] ，它可以自由地推断为我们需要的任何类型。[Nat]当我们到达 kind或的类型级别列表的末尾时，我们使用它[Symbol]。这意味着我们最终会得到类似的结果Result (\'[] :: [Nat]) = [Nat]，即列表的尾部是 的术语级别列表Nat。不幸的是，我们要求这样做Result as ~ [Result a]，但现在情况并非如此；最后一个Result a是Integer，最后一个Result as是[Nat]。即使 GHC 没有把我们拉上来，你也不能将一个 consInteger到一个[Nat].
如何解决这个问题并不明确，因为Term实际上有两个参数，而不是一个。不同情况下的类型Term a也有所不同。GHCI 已意识到这一点并可以告诉我们：a
\xce\xbb :info Term\ntype Term :: forall k. k -> Constraint\nclass Term a where\n type Result :: forall {k}. k -> *\n type family Result a\n term :: Result a\n注意该type Term线；诸如Monoid“将显示type Monoid :: * -> Constraint”或KnownNat“将有”之类的东西type KnownNat :: Nat -> Constraint。
这其实也不错，不然我们早就被击落了。因为这两个实例头看起来确实重叠3：
\n instance (KnownSymbol s) => Term s \n instance (KnownNat n) => Term n\n但我们被这样一个事实所拯救：它们实际上是通过k不同地实例化 kind 参数来区分的：
instance (KnownSymbol s) => Term (s :: Symbol)\n instance (KnownNat n) => Term (n :: Nat)\n如果我们使 kind 参数更加明确，我们就可以Result依赖于kind，而不是类型。无论如何，这实际上是我们想要的；类型 level 1、2、3都具有ResultofInteger因为它们都有 kind Nat；我们不需要为每个个体计算不同的结果类型Nat。
class Term (a :: k) where\n type family Result k :: Type\n term :: Result k\n\ninstance (KnownSymbol s) => Term (s :: Symbol) where\n type instance Result Symbol = String\n term = symbolVal (Proxy @s)\n\ninstance (KnownNat n) => Term (n :: Nat) where\n type instance Result Nat = Integer\n term = natVal (Proxy @n)\n这也使我们能够摆脱列表递归实例中烦人的等式约束。Result取决于类型，编译器可以像我们一样看到整个列表中只涉及一种类型（因为类型级列表必须具有所有相同类型的元素）。
instance (Term a, Term as) => Term ((a \': as) :: [k]) where\n type instance Result [k] = [Result k]\n term = term @k @a : term @[k] @as\n现在我们已经依赖Result于种类而不是类型，我们可以对基本情况执行此操作：
instance Term (\'[] :: [k]) where\n type instance Result [k] = [Result k]\n term = []\n老实说，我并不能 100% 确定这为什么有效。我们依赖于Result [k]存在另一个Term提供 的实例Result k，但是我们没有保证这样一个实例存在的约束（并且我不知道我们将如何编写一个实例，因为没有一种实际上k可以传递的类型到Term）。但它确实有效：
>>> term @_ @3\n3\nit :: Integer\n\n>>> term @_ @[1, 2, 3]\n[1,2,3]\nit :: [Integer]\n\n>>> term @_ @["hello", "world"]\n["hello","world"]\nit :: [String]\n但最大的缺点是现在有一个额外的参数，我们必须显式传递给term. GHC 可以推断它是什么（这就是我们可以使用 的原因@_），但它必须放在第一位，因为它是一种跟随参数。
我想出的解决这个问题的最简单方法是重命名term为term\'，并提供一个新的term参数，将 kind 参数标记为推断的，这样就不需要（也不能）使用类型应用程序来指定它。但这需要 GHC 9 或更高版本。
term :: forall {k} (a :: k). Term (a :: k) => Result k\nterm = term\' @k @a\n但后来我想到了一个更好的办法。type instance Result [k] = [Result k]我们必须在与列表相关的两个实例中重复相同的定义，这已经让我有点恼火了。这是因为实例取决于实际类型，但类型族Result仅取决于其类型，因此当我们有两个覆盖相同类型的不同类型的实例时，我们最终需要冗余定义。对我来说，这已经表明这实际上并不是该类的关联类型系列，但作为独立的类型系列会更好。
type family Demote k where\n Demote Symbol = String\n Demote Nat = Integer\n Demote [k] = [Demote k]\n将类型族从类中取出后，如果我们不再需要显式类型参数，那就太好了k（它仍然作为隐式参数存在，但不会弄乱我们的类型）应用程序）。不幸的是，要调用Demote我们仍然需要对该类型的显式引用。class Term a如果我们的类定义是而不是，我们就没有这个class Term (a :: k)。但是如果我们添加另一层间接，我们可以创建一个类型同义词（甚至不必是类型族！），它的类型为类型4：
type KindOf (a :: k) = k\n\nclass Term a where\n term :: Demote (KindOf a)\n现在终于一切正常了！
\n>>> term @19\n19\nit :: Integer\n\n>>> term @[10, 5, 0]\n[10,5,0]\nit :: [Integer]\n\n>>> term @["take", "that", "typechecker"]\n["take","that","typechecker"]\nit :: [String]\n唯一的（小？）问题是现在term @\'[]不再单独工作，因为它需要实际知道空列表是什么类型（以解析类型Demote族），而不是给我们一个多态空列表。
>>> term @\'[]\n\n<interactive>:26:1: error:\n \xe2\x80\xa2 Couldn\'t match type: Result k0\n with: Result k\n Expected: [Result k]\n Actual: [Result k0]\n NB: \xe2\x80\x98Result\xe2\x80\x99 is a non-injective type family\n The type variable \xe2\x80\x98k0\xe2\x80\x99 is ambiguous\n \xe2\x80\xa2 In the ambiguity check for the inferred type for \xe2\x80\x98it\xe2\x80\x99\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\n When checking the inferred type\n it :: forall {k}. [Result k]\n\n>>> term @(\'[] :: [Symbol])\n[]\nit :: [String]\n这是我最终得到的最终工作模块：
\n{-# LANGUAGE AllowAmbiguousTypes, DataKinds, PolyKinds, FlexibleInstances, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators #-}\n\nmodule Term\nwhere\n\nimport GHC.Types\nimport GHC.TypeLits\n\nimport Data.Proxy\n\ntype KindOf (a :: k) = k\n\ntype family Demote k where\n Demote Symbol = String\n Demote Nat = Integer\n Demote [k] = [Demote k]\n\n\nclass Term a where\n term :: Demote (KindOf a)\n\ninstance (KnownSymbol s) => Term (s :: Symbol) where\n term = symbolVal (Proxy @s)\n\ninstance (KnownNat n) => Term (n :: Nat) where\n term = natVal (Proxy @n)\n\ninstance Term (\'[] :: [k]) where\n term = []\n\ninstance (Term a, Term as) => Term ((a \': as) :: [k]) where\n term = term @a : term @as\n1我认为 GHC 所说的“预期类型”意味着它预期Type/*在这里，因为这比“种类不匹配，预期*，实际[*]”之类的内容更容易让初学者感到困惑。
2这是在实例中向 GHC 类型推断添加额外“公理”的常见技巧。如果实例上的约束包括foo ~ bar，则 GHC 在对实例进行类型检查时通常会假定该条件为 true，并在使用该实例时检查它实际上是否为 true（对于所涉及的特定类型）。如果你“知道”的东西总是正确的，但无法在 Haskell 中证明，那么该检查总是会通过；这使您能够利用在 Haskell 中无法实际证明的真理。
3请记住，必须能够在不考虑其限制的情况下确定哪些实例适用于给定情况！
\n4我有一种预感，我在这里重新发现了一个轮子，果然，包KindOf 中已经存在了singletons的确切定义。singletons包含许多先进的机制来完成这种类型级别对应于术语级别的工作；我一时不知道该向您指出什么，但实际上您可以用Term来自的内容替换您的所有课程singletons，并且它已经可以工作并且更加通用。然而singletons，这是一个相当高级的包，所以不是最容易学习的东西。
如果您计划将此类代码用于持续的实际目的，我强烈建议您投入精力学习如何使用singletons. 可能比自己写的更好。
如果您编写本文是为了了解这些类型级别编程概念的工作原理，那么singletons将会有很多示例来说明您可以将其推向多远，但对于相对新手来说，其实现可能很难理解。