我正在擺弄 Haskell 中型別級編程的基礎知識，并且我試圖撰寫一個函式，使用具有型別背景關系(* -> *) -> Constraint（例如，length或fmap (/= x)）的函式來“本地化”異構串列。
異構串列定義如下：
data HList ls where
HNil :: HList '[]
(:::) :: a -> HList as -> HList (a ': as)
我已經定義了一個型別族AllKind2：
type family AllKind2 c t li :: Constraint where
AllKind2 _ _ '[] = ()
AllKind2 c t ((t _) : xs)) = (c t, AllKind2 c t xs)
型別族按預期作業（據我所知，據我所知），正如這個函式所證明的那樣，如果提供了一個可以滿足的異構串列，它只回傳 unit AllKind2：
unitIfAllIsWell :: forall c t li. AllKind2 c t li => Proxy c -> Proxy t -> HList li -> ()
unitIfAllIsWell _ _ _ = ()
>>> unitIfAllIsWell (Proxy :: Proxy Foldable) (Proxy :: Proxy []) ([] ::: "ok" ::: [1,2] ::: HNil)
()
>>> unitIfAllIsWell (Proxy :: Proxy Foldable) (Proxy :: Proxy []) ("is_list" ::: 10 ::: HNil)
<interactive>:414:1: error:
? Could not deduce: AllKind2 Foldable [] '[Integer]
arising from a use of ‘unitIfAllIsWell’
但是，我撰寫的均質化函式在型別檢查中失敗了：
homogenize
:: forall c t li q. AllKind2 c t li
=> Proxy c
-> Proxy t
-> (forall p q. c t => t p -> q)
-> HList li
-> [q]
homogenize _ _ _ HNil = []
homogenize _ _ f (x ::: xs) = f x : homogenize (Proxy :: Proxy c) (Proxy :: Proxy t) f xs
? Could not deduce: a ~ t p0
from the context: AllKind2 c t li
bound by the type signature for:
homogenize :: forall (c :: (* -> *) -> Constraint)
(t :: * -> *) (li :: [*]) q.
AllKind2 c t li =>
Proxy c
-> Proxy t
-> (forall p q1. c t => t p -> q1)
-> HList li
-> [q]
at HList.hs:(134,1)-(140,8)
or from: li ~ (a : as)
bound by a pattern with constructor:
::: :: forall a (as :: [*]). a -> HList as -> HList (a : as),
in an equation for ‘homogenize’
at HList.hs:142:24-31
‘a’ is a rigid type variable bound by
a pattern with constructor:
::: :: forall a (as :: [*]). a -> HList as -> HList (a : as),
in an equation for ‘homogenize’
at HList.hs:142:24-31
Is the constraint AllKind2 not sufficient to tell the compiler that any element from the HList li will satisfy constraint c t and thus, applying the supplied function f should be valid at the type level?
Am I missing something here? Is what I am attempting even possible?
uj5u.com熱心網友回復：
即使 egAllKind2 Foldable [] '[Int]不匹配 的任何方程AllKind2，它也不能被理解為不可滿足的約束。（一般原則是未定義型別族應用程式就是：未定義，從某種意義上說它可能是某種東西，但你不知道它是什么。）這就是為什么，即使你知道AllKind2 c t (x : xs),你不能通過說“那是獲得定義約束的唯一方法。” 對于一般情況，您需要一個方程式，該方程式將分派到包含實際資訊的類。x ~ t yyAllKind2AllKind2 c t (x : xs)
-- if you know some types satisfy a typeclass, you know they satisfy the superclasses
-- this lets us store and extract the information that x needs to be of form t _
class (c t, x ~ t (UnwrapAllKind2 t x)) => AllKind2Aux c t x where
type UnwrapAllKind2 t x
instance c t => AllKind2Aux c t (t y) where
type UnwrapAllKind2 t (t y) = y
type family AllKind2 c t xs :: Constraint where
AllKind2 c t '[] = ()
AllKind2 c t (x : xs) = (AllKind2Aux c t x, AllKind2 c t xs)
然后你的homogenize通行證沒有修改。
請注意，這homogenize過于復雜。c根本不做任何事情：將實體作為輸入并將homogenize其c t轉發給正在映射的函式。該函式可以只使用它自己的c t實體，因為t它是固定的。沒有什么homogenize可以做的，以下函式不能做得更清楚（請注意，您homogenize甚至無法將映射函式“限制”為僅使用c t而不是任何其他屬性t，因此它可能比它可以澄清的要混亂得多）：
class x ~ t (UnApp t x) => IsApp t x where
type UnApp t x
instance IsApp t (t y) where
type UnApp t (t y) = y
type family AllApp t xs :: Constraint where
AllApp t '[] = ()
AllApp t (x : xs) = (IsApp t x, AllApp t xs)
homogenize' :: AllApp t xs => Proxy t -> (forall x. t x -> r) -> HList xs -> [r] -- also, the Proxy t is not strictly necessary
homogenize' t f HNil = []
homogenize' t f (x ::: xs) = f x : homogenize' t f xs -- note that dealing with Proxys is much nicer if you treat them as things that can be named and passed around instead of rebuilding them every time
-- homogenize' (Proxy :: Proxy []) length ([] ::: "ok" ::: [1,2] ::: HNil) = [0, 2, 2]
轉載請註明出處，本文鏈接：https://www.uj5u.com/qianduan/442240.html
標籤：haskell static-typing type-level-computation higher-kinded-types
上一篇：檔案打開成功時如何處理關閉函式