类型级约束编码

Question

所以我有一个数据构造函数，我只在包含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是KnownNat，即使传入了KnownFoo。有办法让这样的东西起作用吗？

我还尝试将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不可驱动。

感谢您的帮助！

Answer 1

我不确定我是否完全理解您需要什么，但如果您想存储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，并且无论如何都要满足其约束。