键入Family作为类型同义词的参数

Question

我有一个看起来像的数据类型

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

它是一个由自然索引的容器,它采用一种函数来确定如何进行归纳.

我可以很容易地定义类型同义词

type G' n a = G S n a

但我希望能够使用身份功能.

我尝试使用Data.Functor.Identity,但即使用PolyKinds重新定义,我也无法在Naturals(:k Identity => Nat -> Nat)上获得类型级函数,所以我转向类型族,定义

type family Id a where 
  Id a = a 

哪个,很酷,它编译.不幸的是,我提供type G'' n a = G Id n a并且我收到了错误消息

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

那么有没有一种方法可以在类型同义词中使用类型族？这似乎是理想的最终状态.

(我目前使用的扩展名是 {-# LANGUAGE GADTs, TypeFamilies, DataKinds, TypeInType, PolyKinds #-})

Answer 1

您不能在不饱和的情况下传递类型族(或类型同义词),但您可以传递表示该类型族的令牌.然后,当将类型族应用于参数时,您可以查找给定的令牌.

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

现在您可以定义标记以及如何应用它们.

data SToken
type instance Apply SToken n = S n

data IdToken
type instance Apply IdToken n = n

和你的同义词:

type G' = G SToken
type GId = G IdToken

这个技巧 - 传递函数的表示而不是函数本身 - 称为defunctionalisation,最初是在70年代开发的,作为高阶函数编程语言的实现技术.(顺便说一下,那篇论文读起来很棒.)

我不知道这是否是你想要的唯一方法,但它或多或少是如何singletons做到的.更多信息在singletons作者的博客.