我有一个看起来像的数据类型
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 #-}）
您不能在不饱和对象周围传递类型族（或类型同义词），但是可以在代表该类型族的标记周围传递。然后，当需要将类型族应用于参数时，您可以查找给定的标记。
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
这种技巧-绕过函数而不是函数本身的表示形式-被称为去功能化，最初是在70年代开发的，是一种用于高阶功能编程语言的实现技术。（顺便说一下，那篇论文读起来很棒。）
我不知道这是否是您想要做的唯一方法，但是或多或少地是怎么singletons做的。更多信息在singletons作者的博客。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句