Functional dependencies can "return" kinds, type families cannot

13 Feb 2014

      Hello,

Maybe this is well known already (or maybe it's a bug), but lately I've
again found that functional
dependencies are more versatile than type families. In particular, they can
be used to compute
kinds from types, whereas type families cannot. Consider the code below,
which implements a
class for generic (working for types other than lists) map:

{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE FunctionalDependencies     #-}

module MapN where

-- (Type-level) Peano naturals
data Nat = Ze | Su Nat

-- Proxy
data Proxy t = Proxy

-- Singleton type for promoted lists
data SList (l :: [*]) where
  SNil  :: SList '[]
  SCons :: h -> SList t -> SList (h ': t)

-- Apply a type to a list of variables
type family AppVars (t :: k) (vs :: [*]) :: *
type instance AppVars t '[]       = t
type instance AppVars t (v ': vs) = AppVars (t v) vs

-- Domains of a list of functions
type family Doms (funs :: [*]) :: [*]
type instance Doms '[]              = '[]
type instance Doms ((a -> b) ': ts) = a ': Doms ts

-- Codomains of a list of functions
type family CoDoms (funs :: [*]) :: [*]
type instance CoDoms '[]              = '[]
type instance CoDoms ((a -> b) ': ts) = b ': CoDoms ts

-- Generalised map
-- How can I get rid of the FD below? I know how to do so by using a proxy
-- argument of type |Proxy t|, but I don't want an extra argument. The usual
-- trick of replacing the FD by a TF doesn't work here because the TF would
have
-- to return a *kind*, not a type.
class GMap (t :: k) (fs :: [*]) | fs -> k where
  gmap :: SList fs -> AppVars t (Doms fs) -> AppVars t (CoDoms fs)

-- List instance
instance GMap [] '[a -> b] where
  gmap _                 []    = []
  -- The line below does not typecheck without the above FD
  gmap fs@(SCons f SNil) (h:t) = f h : (gmap fs t)

The most interesting part here is the functional dependency fs -> k,
where kis a kind variable!
If this is not a bug (and it does seem to work as I expect it to), then
could we have type families
return kinds too?...

Cheers,
Pedro

Functional dependencies can "return" kinds, type families cannot

José Pedro Magalhães