我正在嘗試從型別級別的值中生成術語級別的值。我有以下代碼
class Term a where
type family Result a :: Type
term :: Result a
instance (KnownSymbol s) => Term s where
type instance Result s = String
term = symbolVal (Proxy @s)
instance (KnownNat n) => Term n where
type instance Result n = Integer
term = natVal (Proxy @n)
這作業得很好：
>>> :t term @"hello"
term @"hello" :: String
>>> term @"hello"
"hello"
我如何在型別級串列上傳播這個想法？當我嘗試這樣的事情時
instance Term '[] where
type instance Result ('[] :: [a]) = [a]
term = []
instance (Term a, Term as) => Term (a ': as) where
type instance Result (a ': as) = Result a ': Result as
term = term @a : term @as
GHC 說 RHSResult (a ': as)有種 [*]，但type在意料之中。
? Expected a type, but ‘Result a : Result as’ has kind ‘[*]’
? In the type ‘Result a : Result as’
In the type instance declaration for ‘Result’
In the instance declaration for ‘Term (a : as)’
我只有一個可以編譯的解決方案，但預計它只會評估第一個元素：
instance (Term a, Term as) => Term (a ': as) where
type instance Result (a ': as) = [Result a]
term = [term @a]
>>> term @'["hello", "world"]
["hello"]
是否可以遞回地將型別級串列轉換為術語？
完整代碼：
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Term where
import Data.Kind
import Data.Proxy
import GHC.TypeLits
class Term a where
type family Result a :: Type
term :: Result a
instance (KnownSymbol s) => Term s where
type instance Result s = String
term = symbolVal (Proxy @s)
instance (KnownNat n) => Term n where
type instance Result n = Integer
term = natVal (Proxy @n)
instance Term '[] where
type instance Result ('[] :: [a]) = [a]
term = []
instance (Term a, Term as) => Term (a ': as) where
type instance Result (a ': as) = Result a ': Result as
term = term @a : term @as
uj5u.com熱心網友回復：
當 GHC 抱怨時：
? Expected a type, but ‘Result a : Result as’ has kind ‘[*]’
? In the type ‘Result a : Result as’
In the type instance declaration for ‘Result’
In the instance declaration for ‘Term (a : as)’
問題是它Result應該為我們提供 的回傳型別term，因此這應該是術語級別串列的型別（這將是 kind Type，或者*在較舊的命名法中1）。然而，我們顯然有一個型別級別串列的運算式（這是一種型別，[*]因為Result amust be Type，它與 相同*）。
實際上，我們希望Result在這里生成[Integer]或[String]取決于型別級別串列是 kind[Nat]還是[Symbol]。我們實際上并不想Result (a ': as)根據是什么遞回地構造as。所以讓我們把它改成：
instance (Term a, Term as) => Term (a ': as) where
type instance Result (a ': as) = [Result a]
term = term @a : term @as
現在我們的錯誤是：
? Couldn't match expected type ‘[Result a1]’
with actual type ‘Result as’
? In the second argument of ‘(:)’, namely ‘term @as’
In the expression: term @a : term @as
In an equation for ‘term’: term = term @a : term @as
啊哈。我們實際上并沒有保證 GHC 的滿意度Result as將是一種Result a可以附加的清單。就 GHC 而言，這是從兩個獨立實體對型別系列的兩個獨立呼叫，沒有理由總是回傳一個型別，該型別是另一個結果的串列。但是我們從我們真正想要的實體中知道這實際上總是成立的，所以也許我們可以添加等式約束？2
instance (Term a, Term as, Result as ~ [Result a]) => Term (a ': as) where
type instance Result (a ': as) = [Result a]
term = term @a : term @as
現在根本沒有編譯器錯誤！讓我們試試：
>>> term @[1, 2, 3]
<interactive>:25:1: error:
? Couldn't match type ‘Nat’ with ‘Integer’
arising from a use of ‘term’
? In the expression: term @[1, 2, 3]
In an equation for ‘it’: it = term @[1, 2, 3]
嗯，這不是我們所期望的。
這個我花了一段時間才弄清楚，但問題出在 的基礎實體中Term '[]，而不是遞回實體中。
type instance Result ('[] :: [a]) = [a]
這表示term應用于空型別級別串列的是一個術語級別串列，其中包含與型別級別串列中相同的型別。它在您直接使用時有效term @'[]，因為該型別級別的空串列是多型的（就像術語級別的空串列是多型的一樣）。它可以是我們想要的任何型別的型別級別串列。因此，如果我們在術語級別獲取結果空串列并將其輸入到[Bool]預期為 a 的背景關系中，GHC 將盡職盡責地推斷我們必須一直在做term @('[] :: [Bool])。
但是當從非空串列實體使用這個空串列實體時，我們沒有使用文字 '[] ，它可以自由地被推斷為我們需要的任何型別。當我們深入到 kind[Nat]或的型別級別串列的末尾時，我們會使用它[Symbol]。這意味著我們最終會得到類似的東西Result ('[] :: [Nat]) = [Nat]，即我們串列的尾部是 的術語級別串列Nat。不幸的是，我們要求這樣做Result as ~ [Result a]，現在這不是真的；最后一個Result a是Integer，最后一個Result as是[Nat]。即使GHC并沒有把我們拉起來，你不能負面因素的Integer到[Nat]。
如何解決這個問題是模糊的，因為Term實際上有兩個引數，而不是一個。在Term a該樣的的a也實體之間變化。GHCI 知道這一點，并且可以告訴我們：
λ :info Term
type Term :: forall k. k -> Constraint
class Term a where
type Result :: forall {k}. k -> *
type family Result a
term :: Result a
注意這type Term條線；類似的東西Monoid會顯示type Monoid :: * -> Constraint，或者KnownNat會顯示type KnownNat :: Nat -> Constraint。
這實際上很好，否則我們早就被擊落了。因為這兩個實體頭確實看起來像是重疊3：
instance (KnownSymbol s) => Term s
instance (KnownNat n) => Term n
但是，通過以不同的方式實體化 kind 引數，它們實際上是不同的，這一事實使我們得救了k：
instance (KnownSymbol s) => Term (s :: Symbol)
instance (KnownNat n) => Term (n :: Nat)
If we make the kind parameter more explicit, we can make Result depend on the kind, rather than the type. Which is actually what we want anyway; type level 1, 2, and 3 all have a Result of Integer because they all have the kind Nat; we don't need to calculate a different resulting type for each individual Nat.
class Term (a :: k) where
type family Result k :: Type
term :: Result k
instance (KnownSymbol s) => Term (s :: Symbol) where
type instance Result Symbol = String
term = symbolVal (Proxy @s)
instance (KnownNat n) => Term (n :: Nat) where
type instance Result Nat = Integer
term = natVal (Proxy @n)
This also allows us to get rid of the annoying equality constraints in the recursive instance for lists, too. Result depends on the kind, and the compiler can see as well as we can that there is only one kind involved throughout the list (because a type-level list must have elements all of the same kind).
instance (Term a, Term as) => Term ((a ': as) :: [k]) where
type instance Result [k] = [Result k]
term = term @k @a : term @[k] @as
And now that we have the Result depending on the kind and not the type, we can do this for the base case:
instance Term ('[] :: [k]) where
type instance Result [k] = [Result k]
term = []
To be honest I'm not 100% certain why this works. We depend for Result [k] on there being another Term instance that supplies Result k, but we don't have a constraint guaranteeing that such an instance will exist (and I don't know how we would write one, without a type with kind k actually available to pass to Term). But it does work:
>>> term @_ @3
3
it :: Integer
>>> term @_ @[1, 2, 3]
[1,2,3]
it :: [Integer]
>>> term @_ @["hello", "world"]
["hello","world"]
it :: [String]
The big downside though is now there's an extra parameter we have to explicitly pass to term. GHC can infer what it is (which is why we could use @_), but it has to come first because it is the kind of a following parameter.
The simplest way I came up with to fix that was to rename term to term', and provide a new term that marks the kind parameter as inferred so that it need not (and cannot) be specified with a type application. This needs GHC 9 or later though.
term :: forall {k} (a :: k). Term (a :: k) => Result k
term = term' @k @a
But then I thought of a better way. It was already irking me slightly that we have to repeat the identical definition of type instance Result [k] = [Result k] in both of the instances pertaining to lists. That's because the instance depends on the actual type, but the type family Result depends only on its kind, so where we have two instances covering different types of the same kind we end up needing redundant definitions. To me that was already a sign that this isn't really an associated type family of the class, but would be better as a stand-alone type family.
type family Demote k where
Demote Symbol = String
Demote Nat = Integer
Demote [k] = [Demote k]
Having taken the type family out of the class, it would be great if we didn't need the explicit kind parameter k any more (it'll still be there as an implicit parameter, but it won't clutter up our type applications). Unfortunately to call Demote we still need an explicit reference to the kind. We don't have that if our class definition is class Term a rather than class Term (a :: k). But if we add another layer of indirection, we can make a type synonym (doesn't even have to be a type family!) that gets the kind of a type4:
type KindOf (a :: k) = k
class Term a where
term :: Demote (KindOf a)
Now it finally all works!
>>> term @19
19
it :: Integer
>>> term @[10, 5, 0]
[10,5,0]
it :: [Integer]
>>> term @["take", "that", "typechecker"]
["take","that","typechecker"]
it :: [String]
The only (minor?) problem is that now term @'[] no longer works on its own, because it needs to actually know what the kind of the empty list is (to resolve the Demote type family) instead of giving us a polymorphic empty list.
>>> term @'[]
<interactive>:26:1: error:
? Couldn't match type: Result k0
with: Result k
Expected: [Result k]
Actual: [Result k0]
NB: ‘Result’ is a non-injective type family
The type variable ‘k0’ is ambiguous
? In the ambiguity check for the inferred type for ‘it’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
it :: forall {k}. [Result k]
>>> term @('[] :: [Symbol])
[]
it :: [String]
Here is the final working module I ended up with:
{-# LANGUAGE AllowAmbiguousTypes, DataKinds, PolyKinds, FlexibleInstances, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators #-}
module Term
where
import GHC.Types
import GHC.TypeLits
import Data.Proxy
type KindOf (a :: k) = k
type family Demote k where
Demote Symbol = String
Demote Nat = Integer
Demote [k] = [Demote k]
class Term a where
term :: Demote (KindOf a)
instance (KnownSymbol s) => Term (s :: Symbol) where
term = symbolVal (Proxy @s)
instance (KnownNat n) => Term (n :: Nat) where
term = natVal (Proxy @n)
instance Term ('[] :: [k]) where
term = []
instance (Term a, Term as) => Term ((a ': as) :: [k]) where
term = term @a : term @as
1 I think GHC says "expected a type" to mean it expected Type/* here because that's less confusing to beginners than something like "Kind mismatch, expected *, actual [*]".
2 This is a common trick to add extra "axioms" to GHC's type inference in instances. If the constraints on an instance include foo ~ bar, then GHC will assume that is true in general when type-checking the instance, and will check that it's actually true (for the particular types involved) when using the instance. If it's something you "know" will always be true but can't prove in Haskell, then that check will always pass; this allows you to make use of a truth that you cannot actually prove in Haskell.
3 Remembering that which instances applies in a given situation must be able to be determined without considering their constraints!
4我有一種預感，我在這里重新發現了一個輪子，并且確實KindOf 在singletons包中已經存在. singletons包含許多用于執行此型別別級別對應于術語級別的作業的高級機制；我不知道直接指向什么，但實際上你可以Term用一些東西替換你所有的類，singletons它已經可以作業并且更通用。然而，這singletons是一個相當高級的軟體包，所以不是最容易學習的東西。
如果您打算將此類代碼用于持續的實際目的，我強烈建議您投入精力學習如何使用singletons. 可能比自己寫好。
如果你寫這篇文章是為了學習這些型別級別的編程概念singletons是如何作業的，那么會有很多例子說明你可以把它推多遠，但它的實作對于一個相對的新手來說可能很難理解。
轉載請註明出處，本文鏈接：https://www.uj5u.com/caozuo/386999.html