如何更改构造函数的类型应用程序参数的顺序

Question

我有以下数据类型定义：

type DynamicF' :: k -> (k -> Type) -> Type
data DynamicF' k f where
  DynamicF :: Typeable a => f a -> DynamicF' k f

问题是，一般来说，我会专注于

k

到

Type

。所以我提供了以下类型别名：

type DynamicF f = DynamicF' Type f

然后我可以做这样的事情：

data Showable a where
  Showable :: Show a => a -> Showable a

f :: DynamicF Showable -> String
f (DynamicF @_ @a x) = g x where
  g :: Showable a -> String
  g (Showable y) = show y

这可能是一个愚蠢的例子，但希望能够说明问题，但请注意模式匹配：

DynamicF @_ @a x

特别是第一个参数需要下划线。

这是因为在

f

构造函数中，第一个类型应用程序参数似乎反对

a

，而不是

DynamicF

。

显然我可以使用

forall blah.

来更改这些顺序，也许还可以使用

forall {blah}.

之类的构造。

但我不确定在这段代码中实际放置

forall.

的位置，这样我就可以这样做：

f (DynamicF @a x)

在模式匹配中，而不是需要愚蠢的下划线。

Answer 1

放置

forall

的正确位置是在

data

声明中：

type DynamicF' :: k -> (k -> Type) -> Type
data DynamicF' k f where
  DynamicF :: forall a f k. Typeable a => f a -> DynamicF' k f

如果您担心

f

和

k

无法在

forall

中指定，因为它们是

DynamicF' k f

类型的一部分，请不要担心。构造函数“结果”的类型决定了哪些变量成为最终类型的一部分。例如，以下声明的工作方式与原始声明完全相同：

data DynamicF' doesn't match where
  DynamicF :: forall whatever you want. 
              Typeable whatever => you whatever -> DynamicF' want you

但是，请注意，我无法重复您的问题。此构造函数的顺序已经是

forall a f k

（因为

Typeable a =>

将

a

放在第一个位置）。