2

使用DataKindsand KindSignatures，我可以执行以下操作：

data T = T1 | T2 | ... | TN

data D (t :: T) where ...
  D1 :: ... -> D t
  D2 :: ... -> D t
  .
  .
  .
  DN :: ... -> D t

当然，Haskell 在运行时删除了这种类型。我可以通过分离构造函数来保留这些信息：

data D' (t :: T) where ...
  D1T1 :: ... -> D' T1
  D1T2 :: ... -> D' T2
  .
  .
  .
  D1TN :: ... -> D' TN
  D2T1 :: ... -> D' T1
  D2T2 :: ... -> D' T2
  .
  .
  .
  D2TN :: ... -> D' TN
  .
  .
  .
  DNT1 :: ... -> D' T1
  DNT2 :: ... -> D' T2
  .
  .
  .
  DNTN :: ... -> D' TN

然后当我进行模式匹配时，我也得到了类型。但现在我已经用完了所需的构造函数数量，我怀疑这将是一场维护噩梦。

我想做这样的事情：

data DWrap (t :: T) where
  DWrap :: t -> D t -> DWrap t

然后我可以进行模式匹配DWrap以确定类型：

g :: D T1 -> ...
g = ...

f (DWrap T1 x) = g x

这应该没问题，因为一旦我们匹配T1我们就知道t然后我们知道我们是开始传递给的正确类型g。

当然，如果我只想忽略我喜欢的类型：

h :: D t -> ...
h = ...

f (DWrap _ x) = h x

无论哪种方式，完整性检查都应该确保我不会做任何愚蠢的事情。

除了这种方法行不通。首先，因为t不是普通类型的 kind *，它是 kind T。其次T1甚至不是 type 'T1，它是 type 的成员T，就像等一样T2，T3所以这是区分类型的无用方法。

为了尝试解决第一个问题，我可以更改t为Proxy t：

data DWrap (t :: T) where
  DWrap :: Proxy t -> D t -> DWrap t

现在这个data定义可以编译了，但是这对于区分类型是毫无用处的，因为Proxy只有一个构造函数。

我可以这样做：

data TConstructor (t :: T) where
  T1Con :: TConstructor T1
  T2Con :: TConstructor T2
  .
  .
  .
  TNCon :: TConstructor TN

然后这个：

data DWrap (t :: T) where
  DWrap :: TConstructor t -> D t -> DWrap t

然后我可以这样匹配：

g :: D T1 -> ...
g = ...

f (DWrap T1Con x) = g x

这应该可以完成工作，但我必须写出data TConstructor，这几乎是data T. 无论如何我可以避免这个额外的样板并仍然实现我想要做的事情吗？

4

0 回答 0