Type Family as Argument to Type Synonym

Question

I have a data type that looks like

data G f n a where 
  G :: a -> G f n a -> G f (f n) a

It's a container indexed by naturals, which takes a function that determines how to proceed inductively.

I can define a type synonym easily like

type G' n a = G S n a

But I'd like to be able to use the identity function.

I tried using Data.Functor.Identity, but even when redefined with PolyKinds, I can't get a type-level function on Naturals (:k Identity => Nat -> Nat), so I turned to type families, defining

type family Id a where 
  Id a = a

which, cool, it compiles. Unfortunately, I supply type G'' n a = G Id n a and I get the error message of

The type family ‘Id’ should have 1 argument, but has been given none
In the type synonym declaration for ‘G''’

So is there a way I can use a type family in a type synonym? That seems like the ideal end state.

(The extensions I'm currently using are {-# LANGUAGE GADTs, TypeFamilies, DataKinds, TypeInType, PolyKinds #-})

Benjamin Hodgson Benjamin Hodgson · Accepted Answer · 2018-05-23T17:54:35

You can't pass type families (or type synonyms) around unsaturated, but you can pass around a token which represents that type family. Then when it's time to apply the type family to an argument, you can look up the token you were given.

type family Apply (token :: *) (n :: Nat) :: Nat

data G token n a where
    G :: a -> G token n a -> G token (Apply token n) a

Now you can define tokens and how to apply them.

data SToken
type instance Apply SToken n = S n

data IdToken
type instance Apply IdToken n = n

And your synonyms:

type G' = G SToken
type GId = G IdToken

This trick - passing around representations of functions, rather than functions themselves - is called defunctionalisation and was originally developed in the 70s as an implementation technique for higher-order functional programming languages. (That paper's a terrific read, by the way.)

I don't know if this is the only way to do what you want, but it's more or less how singletons does it. More info on the singletons author's blog.

Type Family as Argument to Type Synonym

1 Answers