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 #-}
)
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With