CODEWITHSUNDEEP
haskellfunctional-dependenciestype-familieshlist
aavogt
aavogt

Reputation: 1308

Type families get stuck where the equivalent type using functional dependencies can be simplified

I am trying to implement map tagSelf :: [a] -> [Tagged a a] and map untag :: [Tagged a a] -> [a] with good type-inference properties for HList. The TF version is close, but I have a case where a type function gets stuck while the FD version simplifies the type just fine.

Here is a self-contained example, which can be run with 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

Is it possible to get the better syntax of TF while keeping the same behavior as the FD version?

Upvotes: 4

Views: 217

Answers (1)

András Kovács
András Kovács

Reputation: 30103

Why not just use the TF version as it is? The type Tagged t t -> HList (UntagR '[Tagged t t]) will reduce properly whenever you put the function in context:

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

Also, the type seems to be eager to reduce if you perturb it a bit:

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

Type annotation works fine too:

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

It's certainly pesky on some level that the inferred type isn't fully reduced, but it doesn't seem to be more than a harmless artifact.

Upvotes: 2

Related Questions