How can one name a type family as a higher-order kind function

Question

Is it possible to use a type family as a higher-order "type function" to pass to another type family? A simple example would be the following code:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Test where
import GHC.TypeLits as T

type family Apply (f :: Nat -> Nat -> Nat) (n :: Nat) (m :: Nat) :: Nat where
  Apply f n m = f n m

type family Plus (n :: Nat) (m :: Nat) :: Nat where
  Plus n m = n T.+ m

type family Plus' (n :: Nat) (m :: Nat) :: Nat where
  Plus' n m = Apply (T.+) n m

The first declaration of Plus is valid, while the second one (Plus') produces the following error:

Test.hs:19:3: error:
    • The type family ‘+’ should have 2 arguments, but has been given none
    • In the equations for closed type family ‘Plus'’
      In the type family declaration for ‘Plus'’
   |
19 |   Plus' n m = Apply (T.+) n m
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Is there a way to use the Apply type function to implement Plus?

EDIT A commenter linked to the feature request report at https://ghc.haskell.org/trac/ghc/ticket/9898. It mentions the singleton library. I would be happy with an example of using it or other "workarounds" to achieve a similiar effect of abstracting over the arithmetic operations on Nat such as +, *, - and Mod.

Answer 1

A useful approach is defunctionalization. You can implement it yourself, or find an implementation in the singletons library.

The core is an “open kind”:

data TYFUN :: Type -> Type -> Type
type TyFun a b = TYFUN a b -> Type

TyFun a b is an open kind; it is not closed like a normal, promoted, data kind. You “declare” new functions as follows.

data Plus :: TyFun Nat (TyFun Nat Nat)

You can then define this type family to link declaration and definition

type family Apply (f :: TyFun a b) (x :: a) :: b
data PlusSym1 :: Nat -> TyFun Nat Nat -- see how we curry
type instance Apply Plus x = PlusSym1 x
type instance Apply (PlusSym1 x) y = x + y

Now, Plus is a normal type constructor: a data type, not a type family. This means you are allowed to pass it to other type families. Note that they must be TyFun aware themselves.

type family Foldr (cons :: TyFun a (TyFun b b)) (nil :: b) (xs :: [a]) :: b where
    Foldr _ n '[] = n
    Foldr c n (x:xs) = Apply (Apply c x) (Foldr c n xs)
type Example = Foldr Plus 0 [1,2,3]

The idea behind the open kind is that Type is already an open kind, and kinds like A -> Type, A -> B -> Type are themselves open. TYFUN is a tag to identify things as TyFuns, and TyFun is an open kind that is effectively disjoint from other open kinds. You can also use the Type open kind straight:

type family TyFunI :: Type -> Type
type family TyFunO :: Type -> Type
type family Apply (f :: Type) (x :: TyFunI f) :: TyFunO f
data Plus :: Type
data PlusSym1 :: Nat -> Type
type instance TyFunI Plus = Nat
type instance TyFunO Plus = Type
type instance TyFunI (PlusSym1 _) = Nat
type instance TyFunO (PlusSym1 _) = Nat
type instance Apply Plus x = PlusSym1 x
type instance Apply (PlusSym1 x) y = x + y

On the plus side, this can handle dependent type functions, but, on the other hand, it only does that because it shamelessly throws out kind checking by making everything “Typely-typed”. This is not as bad is Stringly-typed code, as it’s all compile-time, but still.