haskell – 类型族被卡在可以简化使用函数依赖的等效类型的地方

2023年10月13日 245次阅读

我正在尝试实现map tagSelf :: [a] – > [标记为a]和

map untag :: [标记为a] – > [a]具有良好的类型推理

HList的属性. TF版本很接近,但我有一个

FD时类型函数卡住的情况

版本简化了类型.

这是一个自包含的示例,可以使用doctest运行.

{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, FunctionalDependencies, GADTs, MultiParamTypeClasses, TypeFamilies, TypeOperators #-}
{-# LANGUAGE PolyKinds, UndecidableInstances #-}
module NEquivTFFD where
{- $ex

These two types are equal, as they should be.

>>> :t \x -> hUntagFD $HCons x HNil
\x -> hUntagFD $HCons x HNil :: Tagged x x -> HList '[x]

>>> :t \x -> hUntagTF $HCons x HNil
\x -> hUntagTF $HCons x HNil :: Tagged t t -> HList '[t]


If I replace HCons with hBuild, the FD solution infers
the same type

>>> :t \x -> hUntagFD $hBuild x
\x -> hUntagFD $hBuild x :: Tagged x x -> HList '[x]

But the TF solution is unable to simplify the UntagR type family
in ghc-7.8.2:

>>> :t \x -> hUntagTF $hBuild x
\x -> hUntagTF $hBuild x
  :: Tagged t t -> HList (UntagR '[Tagged t t])

while in ghc-7.6.2, there is some suggestion that hBuild is the
problem, and that -XPolyKinds is not a problem:

  \x -> hUntagTF $hBuild x
      :: (HBuild' ('[] *) (t -> HList (TagR [*] a)), TagUntagTF a) =>
        t -> HList a


If there 'x' type variable is fixed to something (like ()), the two
functions are the same again 

>>> :t hUntagFD $hBuild (Tagged ())
hUntagFD $hBuild (Tagged ()) :: HList '[()]

>>> :t hUntagTF $hBuild (Tagged ())
hUntagTF $hBuild (Tagged ()) :: HList '[()]
-}

-- * Type family implementation 
type family TagR (xs :: k) :: k
type instance TagR '[] = '[]
type instance TagR (x ': xs) = TagR x ': TagR xs
type instance TagR (x :: *) = Tagged x x

-- | inverse of TagR
type family UntagR (xs :: k) :: k
type instance UntagR '[] = '[]
type instance UntagR (x ': xs) = UntagR x ': UntagR xs
type instance UntagR (Tagged x x) = x

class (UntagR (TagR a) ~ a) => TagUntagTF (a :: [*]) where
    hTagTF :: HList a -> HList (TagR a)
    hUntagTF :: HList (TagR a) -> HList a

instance TagUntagTF '[] where
    hTagTF _ = HNil
    hUntagTF _ = HNil

instance TagUntagTF xs => TagUntagTF (x ': xs) where
    hTagTF (HCons x xs) = Tagged x `HCons` hTagTF xs
    hUntagTF (HCons (Tagged x) xs) = x `HCons` hUntagTF xs

-- * Functional dependency implementation
class TagUntagFD a ta | a -> ta, ta -> a where
    hTagFD :: HList a -> HList ta
    hUntagFD :: HList ta -> HList a

instance TagUntagFD '[] '[] where
    hTagFD _ = HNil
    hUntagFD _ = HNil

instance (y ~ Tagged x x, TagUntagFD xs ys)
      => TagUntagFD (x ': xs) (y ': ys) where
    hTagFD (HCons x xs) = Tagged x `HCons` hTagFD xs
    hUntagFD (HCons (Tagged x) xs) = x `HCons` hUntagFD xs


-- * Parts of HList that are needed
data HList x where
    HNil :: HList '[]
    HCons :: a -> HList as -> HList (a ': as)

newtype Tagged x y = Tagged y

hBuild :: (HBuild' '[] r) => r
hBuild =  hBuild' HNil

class HBuild' l r where
    hBuild' :: HList l -> r

instance (l' ~ HRevApp l '[])
      => HBuild' l (HList l') where
  hBuild' l = hReverse l

instance HBuild' (a ': l) r
      => HBuild' l (a->r) where
  hBuild' l x = hBuild' (HCons x l)

type family HRevApp (l1 :: [k]) (l2 :: [k]) :: [k]
type instance HRevApp '[] l = l
type instance HRevApp (e ': l) l' = HRevApp l (e ': l')

hRevApp :: HList l1 -> HList l2 -> HList (HRevApp l1 l2)
hRevApp HNil l = l
hRevApp (HCons x l) l' = hRevApp l (HCons x l')

hReverse l = hRevApp l HNil

是否有可能在保持TF的同时获得更好的TF语法
与FD版本相同的行为？

最佳答案 为什么不直接使用TF版本呢？标签类型t t – >只要将函数放在上下文中,HList(UntagR'[Tagged t t])就会正确缩小：

(\x -> hUntagTF $hBuild x) (Tagged ()) :: HList '[()]

此外,如果你稍微扰乱它,这种类型似乎急于减少：

hUntagTF . hBuild :: Tagged t t -> HList '[t]

hHead :: HList (x ': xs) -> x
hHead (HCons x xs) = x

(\x -> hHead $hUntagTF $hBuild x) :: Tagged x x -> x

类型注释也可以正常工作：

let f = (\x -> hUntagTF $hBuild x) :: Tagged t t -> HList '[t]

在某种程度上,推断类型并没有完全降低,这肯定令人讨厌,但它似乎不仅仅是一个无害的工件.

点赞