我试图证明类型级函数Union https://hackage.haskell.org/package/type-level-sets-0.8.5.0/docs/Data-Type-Set.html#t:Union是关联的，但我不确定应该如何完成。我证明了类型级附加函数的正确身份和结合律以及联合的正确身份：
data SList (i :: [k]) where
SNil :: SList '[]
SSucc :: SList t -> SList (h ': t)
appRightId :: SList xs -> xs :~: (xs :++ '[])
appRightId SNil = Refl
appRightId (SSucc xs) = case appRightId xs of Refl -> Refl
appAssoc
:: SList xs
-> Proxy ys
-> Proxy zs
-> (xs :++ (ys :++ zs)) :~: ((xs :++ ys) :++ zs)
appAssoc SNil _ _ = Refl
appAssoc (SSucc xs) ys zs = case appAssoc xs ys zs of Refl -> Refl
cong :: a :~: b -> f a :~: f b
cong Refl = Refl
unionRightId :: SList xs -> AsSet xs :~: Union xs '[]
unionRightId xs = case cong (appRightId xs) of Refl -> Refl
但我不知道如何证明联合具有关联性。
None
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
