我认为这是我做过的最深入的 Haskell 类型系统扩展，我遇到了一个我无法弄清楚的错误。提前为篇幅道歉，这是我可以创建的最短示例，它仍然说明了我遇到的问题。我有一个递归 GADT，它的种类是提升列表，如下所示：
GADT 定义
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
data DataKind = A | B | C
-- 'parts' should always contain at least 1 element which is enforced by the GADT.
-- Lets call the first piece of data 'val' and the second 'subdata'.
-- All data constructors have these 2 fields, although some may have
-- additional fields which I've omitted for simplicity.
data SomeData (parts :: [DataKind]) where
MkA :: Maybe Char -> Maybe (SomeData subparts) -> SomeData ('A ': subparts)
MkB :: Maybe Char -> Maybe (SomeData subparts) -> SomeData ('B ': subparts)
MkC :: Maybe Char -> Maybe (SomeData subparts) -> SomeData ('C ': subparts)
deriving instance Show (SomeData parts)
问题
我想要做的是遍历数据并执行一些操作，例如将Just Char找到的第一个传播到顶部。
烦人的缺失功能 - 下一节需要
现在，因为显然没有对 GADT 的记录语法支持（https://ghc.haskell.org/trac/ghc/ticket/2595），您需要手动编写它们，所以它们是：
getVal :: SomeData parts -> Maybe Char
getVal (MkA val _) = val
getVal (MkB val _) = val
getVal (MkC val _) = val
-- The lack of record syntax for GADTs is annoying.
updateVal :: Maybe Char -> SomeData parts -> SomeData parts
updateVal val (MkA _val sub) = MkA val sub
updateVal val (MkB _val sub) = MkB val sub
updateVal val (MkC _val sub) = MkC val sub
-- really annoying...
getSubData :: SomeData (p ': rest) -> Maybe (SomeData rest)
getSubData (MkA _ sub) = sub
getSubData (MkB _ sub) = sub
getSubData (MkC _ sub) = sub
测试数据
所以，我想做的事情。从顶部向下走结构，直到找到一个值为Just. 所以给定以下初始值：
a :: SomeData '[ 'A ]
a = MkA (Just 'A') Nothing
b :: SomeData '[ 'B ]
b = MkB (Just 'B') Nothing
c :: SomeData '[ 'C ]
c = MkC (Just 'C') Nothing
bc :: SomeData '[ 'B, 'C ]
bc = MkB Nothing (Just c)
abc :: SomeData '[ 'A, 'B, 'C ]
abc = MkA Nothing (Just bc)
预期结果
我想要这样的东西：
> abc
MkA Nothing (Just (MkB Nothing (Just (MkC (Just 'C') Nothing))))
> propogate abc
MkA (Just 'C') (Just (MkB (Just 'C') (Just (MkC (Just 'C') Nothing))))
以前的尝试
我试了几次，首先是一个常规功能：
propogate sd =
case getVal sd of
Just _val ->
sd
Nothing ->
let
newSubData = fmap propogate (getSubData sd)
newVal = join . fmap getVal $ newSubData
in
updateVal newVal sd
这给出了错误：
Broken.hs:(70,1)-(81,35): error: …
• Occurs check: cannot construct the infinite type: rest ~ p : rest
Expected type: SomeData rest -> SomeData (p : rest)
Actual type: SomeData (p : rest) -> SomeData (p : rest)
• Relevant bindings include
propogate :: SomeData rest -> SomeData (p : rest)
(bound at Broken.hs:70:1)
Compilation failed.
我还尝试了一个类型类并尝试在结构上进行匹配：
class Propogate sd where
propogateTypeClass :: sd -> sd
-- Base case: We only have 1 element in the promoted type list.
instance Propogate (SomeData parts) where
propogateTypeClass sd = sd
-- Recursie case: More than 1 element in the promoted type list.
instance Propogate (SomeData (p ': parts)) where
propogateTypeClass sd =
case getVal sd of
Just _val ->
sd
Nothing ->
let
-- newSubData :: Maybe subparts
-- Recurse on the subdata if it exists.
newSubData = fmap propogateTypeClass (getSubData sd)
newVal = join . fmap getVal $ newSubData
in
updateVal newVal sd
这会导致错误：
Broken.hs:125:5-26: error: …
• Overlapping instances for Propogate (SomeData '['A, 'B, 'C])
arising from a use of ‘propogateTypeClass’
Matching instances:
instance Propogate (SomeData parts)
-- Defined at Broken.hs:91:10
instance Propogate (SomeData (p : parts))
-- Defined at Broken.hs:95:10
• In the expression: propogateTypeClass abc
In an equation for ‘x’: x = propogateTypeClass abc
Compilation failed.
我也尝试过匹配的组合，SomeData '[]但SomeData '[p]无济于事。
我希望我遗漏了一些简单的东西，但我还没有在任何地方找到关于如何处理这样的结构的文档，而且我对 Haskell 类型系统的理解有限，反正现在:)。再一次，很抱歉这篇长文，任何帮助将不胜感激:)