具有 Type.Reflection 和 Nats 的泛型类型

Question

我有一个 Nat 的简单定义和一个由 Nat 索引的类型的定义，Natty。

data Nat :: * where 
    Zero :: Nat
    Suc  :: Nat -> Nat              deriving(Show, Typeable)

data Natty :: Nat -> * where
    Zy :: Natty Zero
    Sy :: Natty n -> Natty (Suc n)  deriving Typeable

我想使用 Type.Reflection 模块以通用方式存储和操作这些 Natty。

将 Nat 存储为类型代表可以正常工作。

foo :: Nat -> SomeTypeRep
foo x = SomeTypeRep (typeOf x)

但是除非添加额外的约束，否则将 Natty 存储为类型代表是行不通的。

boo :: Natty n -> SomeTypeRep
boo x = SomeTypeRep (typeOf x)

boo 产生以下错误：

No instance for (Typeable n) arising from the use of 'typeOf'

我的问题是为什么 Haskell 不能识别 n 是一个 nat 并因此应该是 Typeable？

就像我说的那样，我可以通过将 Typeable n 的约束添加到 boo 的开头来解决这个问题，但是当我使用一个在另一个函数中间返回 natty 的函数时，它并不那么简单。

已使用以下扩展和导入。

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-} 
import Type.Reflection

Answer 1

你可以实现你想要的功能，但不是免费的。

boof :: Natty n -> TypeRep n
boof Zy = typeRep
boof (Sy n) = withTypeable (boof n) typeRep

更明确地说（这基本上是 boof 幕后发生的事情）：

goo :: Natty n -> TypeRep n
goo Zy = typeRep @'Zero
goo (Sy n) = App (typeRep @'Suc) (goo n)

正如goo 所示，TypeRep 的结构实际上与Natty 的结构非常相似。确实，您也可以采用其他方式，尽管您无法让模式检查器相信它是完全的：

hum :: TypeRep n -> Natty n
hum (App s n)
  | Just HRefl <- eqTypeRep s (typeRep @'S) = Sy (hum n)
  | otherwise = error "imp possible"
hum z
  | Just HRefl <- eqTypeRep z (typeRep @'Z) = Zy
  | otherwise = error "impposs ible"

---

您可以根据需要对结果进行总结：

boo :: Natty n -> SomeTypeRep
boo n = SomeTypeRep (boof n)

但您似乎应该使用比SomeTypeRep 更具体的东西。 Typeable 内部实际上使用了这个：

data SomeKindedTypeRep k where
  SomeKindedTypeRep :: forall (x :: k). Typeable x => SomeKindedTypeRep k

您可以定义它并使用SomeKindedTypeRep Nat，或者为Nat 定义一个专门的版本。这样您就不会因为故意忘记类型而忘记类型（在编译时已知）。

Answer 2

添加 Typeable n 反映了这样一个事实，即 GHC 需要将不同的 Typeable 字典传递到 boo，如果它以不同方式实例化的 n 调用。

Typeable 和 DataKinds 的相互作用有一些巧妙之处。 GHC导出的实例大致等价于

instance Typeable Nat where ...
instance Typeable 'Zero where ...
instance Typeable n => Typeable ('Suc n) where ...

您被提示添加的Typeable n 约束不会被Typeable Nat 实例填充（记住n 有一种Nat，而不是*！），而是后两个约束.

但是，我可以听到你说，为什么 GHC 不能通过简单的归纳来找出所有 n :: Nat 都是 Typeable 的这两个实例？因为'Zero 和'Suc 并不是制作类似Nat 的唯一方法...

ghci> type family Stuck :: k
ghci> :kind Natty Stuck          -- a valid type!
Natty Stuck :: *

换句话说，GHC 在编译时无法知道n :: Nat 是Typeable，您需要向它传递这个事实的运行时见证。