类型级别约束编码

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 即使 < code>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 并满足其约束。