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

Question

我正在尝试实现 map tagSelf :: [a] -> [Tagged a a]和map untag :: [Tagged a 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 语法，同时保持
与 FD 版本相同的行为？

Answer 1

为什么不直接使用 TF 版本呢？型号Tagged 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]

推断的类型没有完全减少在某种程度上肯定是令人讨厌的，但它似乎只是一个无害的神器。