함수 종속성을 사용하여 해당 유형을 단순화 할 수있는 유형 패밀리가 발생합니다.

Question

HFC에 대해 유형의 좋은 속성을 가진 map tagSelf :: [a] -> [Tagged a a] 및 을 구현하려고합니다. 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 

그것은 FD 버전으로 같은 동작을 유지하면서 TF의 더 나은 구문을 얻을 수 있습니까?

Answer 1

TF 버전을 그대로 사용하지 않는 이유는 무엇입니까? 이 맥락에서 기능을 넣을 때마다 유형 Tagged t t -> HList (UntagR '[Tagged t t])가 제대로 줄일 :

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 

유형 주석이 너무 잘 작동 : 또한

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

, 종류는 당신이 그것을 조금 교란 경우 감소 열망 것 같다 :

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

그것은 추론 유형이 완전히 감소되지 않는 어떤 수준에 확실히 성가신하지만 무해한 유물보다 더 될 것 같지 않습니다.