所以我有一個資料建構式，我只在包含Nat. 通常，如果我在型別級別傳遞它并且我想將其反映Nat到術語級別，我需要一個KnownNat約束。我想要做的是將此KnownNat約束編碼到型別本身中，因此如果此型別出現在某處的簽名中，則會在KnownNat函式體中推斷出約束。這意味著我不再需要KnownNat在使用站點撰寫約束。我只需要確保KnownNat在施工時滿足約束。
我想為此使用 GADT 并做到了這一點：
data Foo = Foo Nat Nat
type family GetA (f :: Foo) :: Nat where
GetA ('Foo a _) = a
type family GetB (f :: Foo) :: Nat where
GetB ('Foo _ b) = b
data KnownFoo (f :: Foo) where
KnownFoo :: (KnownNat (GetA f), KnownNat (GetB f)) => KnownFoo f
foo :: forall (f :: Foo) (kf :: KnownFoo f). Proxy kf -> Integer
foo _ = natVal $ Proxy @(GetA f)
但這不起作用，因為型別檢查器不理解這GetA f是 aKnownNat即使KnownFoo傳入了 a 。有沒有辦法讓這樣的事情起作用？
我還嘗試將f :: Foo完全移動到KnownFoo約束中，如下所示：
data Foo = Foo Nat Nat
type family GetA (f :: Foo) :: Nat where
GetA ('Foo a _) = a
type family GetB (f :: Foo) :: Nat where
GetB ('Foo _ b) = b
data KnownFoo where
KnownFoo :: forall f. (KnownNat (GetA f), KnownNat (GetB f)) => Proxy f -> KnownFoo
type family GetFoo (kf :: KnownFoo) :: Foo where
GetFoo ('KnownFoo (Proxy f)) = f
但是我沒有辦法寫GetFoo型別族，因為它抱怨這KnownNat是不可推廣的。
任何幫助表示贊賞！
uj5u.com熱心網友回復：
我不確定我是否完全理解您的需求，但如果您想存盤一個KnownNat約束，您必須有一些運行時表示。也許這樣的事情可能對你有用：
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
import GHC.TypeLits
data FooC a b where
FooR :: (KnownNat a, KnownNat b) => FooC a b
type family GetA x where GetA (FooC a b) = a
type family GetB x where GetB (FooC a b) = b
withKnowledge :: FooC a b -> ((KnownNat a, KnownNat b) => r) -> r
withKnowledge FooR r = r
請注意，DataKinds這里甚至沒有：我們直接定義我們想要的新型別，而不是間接定義它的降低形式。Known我猜你可以為此做一個類似的課程。
class KnownFoo f where witness :: f
instance (KnownNat a, KnownNat b) => KnownFoo (FooC a b) where witness = FooR
withKnownFoo :: forall f a b r. (KnownFoo f, f ~ FooC a b) => ((KnownNat (GetA f), KnownNat (GetB f)) => r) -> r
withKnownFoo = withKnowledge (witness @f)
不過，它似乎不是超級有用。任何時候你可以寫withKnownFoo x，你已經KnownNat在范圍內有適當的實體來寫x，并且無論如何都要滿足它的約束。
轉載請註明出處，本文鏈接：https://www.uj5u.com/shujuku/446073.html