m-r*_*aud 1 recursion haskell gadt data-kinds
我认为这是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类型系统,我现在已经理解了,现在无论如何:).再一次,抱歉长篇文章,任何帮助将不胜感激:)
你得到的错误是红鲱鱼 - GHC无法推断GADT上的功能类型.你必须给它一个类型签名才能看到真正的错误:
propogate :: SomeData x -> SomeData x
....
这给出了错误:
* Couldn't match type `x' with `p0 : parts0'
`x' is a rigid type variable bound by
the type signature for:
propogate :: forall (x :: [DataKind]). SomeData x -> SomeData x
Expected type: SomeData (p0 : parts0)
Actual type: SomeData x
如果不清楚,这个错误消息说我们声称类型争论SomeData只是一个变量(也就是说,我们对它一无所知,除了它的类型)但是内部使用一些函数propogate要求它的形式p0 : parts0对于某些类型p0 : parts0.
但是,你在开头说:
'parts'应始终包含至少1个由GADT强制执行的元素.
但是编译器不知道这个!你必须告诉它,通常这是通过GADT构造函数上的模式匹配来完成的,它将类型相等带入范围.你唯一的问题是你必须匹配三个构造函数,所有构造函数都具有相同的代码.解决方案是从您的数据类型中删除重复:
data SomeData (parts :: [DataKind]) where
Mk :: SDataKind s -> Maybe Char -> Maybe (SomeData subparts) -> SomeData (s ': subparts)
data SDataKind (x :: DataKind) where
SA :: SDataKind A
SB :: SDataKind B
SC :: SDataKind C
类似的包singletons将SDataKind自动为您生成类型和相关函数.
所有"记录"功能都大大简化:
getVal :: SomeData parts -> Maybe Char
getVal (Mk _ v _) = v
updateVal :: Maybe Char -> SomeData parts -> SomeData parts
updateVal val (Mk t _val sub) = Mk t val sub
getSubData :: SomeData (p ': rest) -> Maybe (SomeData rest)
getSubData (Mk _ _ sub) = sub
现在,为了使你的函数得到类型检查(因为它在语义上确实是正确的),你所要做的就是在构造函数上进行模式匹配:
propogate :: SomeData x -> SomeData x
propogate sd@Mk{} =
.... -- unchanged
请注意,代码是相同的,除了添加类型签名和@Mk{}变量模式之后sd.
最后,尝试在这里使用类型类没有给你任何东西 - 你已经有一个索引类型,它包含你需要的所有(类型)信息 - 你通过模式匹配在该类型的构造函数上获得此信息.
另请注意,您不会失去任何一般性SomeData- 如果您希望特定索引具有额外信息,您只需添加另一个索引的字段part.您甚至可以在额外字段中嵌入复杂逻辑,因为该SDataKind字段允许您随意对索引进行模式匹配:
data SomeData (parts :: [DataKind]) where
Mk :: SDataKind s
-> DataPart s
-> Maybe Char
-> Maybe (SomeData subparts)
-> SomeData (s ': subparts)
type family (==?) (a :: k) (b :: k) :: Bool where
a ==? a = 'True
a ==? b = 'False
-- Example - an additional field for only one index, without duplicating
-- the constructors for each index
data DataPart x where
Nil :: ((x ==? 'A) ~ 'False) => DataPart x
A_Data :: Integer -> DataPart A
最后,如果您希望沿着原始课程跋涉,您可以这样做,但代码重复的来源应该变得非常明显:
partsUncons :: SomeData ps0 -> (forall p ps . (ps0 ~ (p : ps)) => r) -> r
partsUncons MkA{} x = x
partsUncons MkB{} x = x
partsUncons MkC{} x = x
propogate :: SomeData x -> SomeData x
propogate sd = partsUncons sd $
.... -- unchanged