是否可以在 Idris 中对种类进行抽象？

Question

我正在使用 Idris 进行类型驱动开发，了解如何定义具有可变数量参数的函数。我有点雄心勃勃，想编写一个 mapN 函数，将 (n : Nat) 参数的函数映射到某些 Applicative 类型的 n 值上。

调查这个问题让我认为如果不至少也提供函数的参数类型可能是不可能的。这促使我尝试编写一个函数，该函数将采用 Nat 和可变数量的 Type 参数和 return 函数类型，就像您在类型之间串起箭头一样。如：

Arrows 0 Int = Int
Arrows 1 Int String = Int -> String

这是我最好的尝试，但没有用：

Arrows : (n : Nat) -> (a : Type) -> Type
Arrows Z a = a
Arrows (S k) a = f where
  f : Type -> Type
  f b = Arrows k a -> b

不幸的是，这两种类型签名都没有意义，因为有时我希望函数 return a Type 有时它 returns Type -> Type 有时它 returns Type -> Type -> Type 等等。我认为这与使用可变数量的参数编写任何其他函数大致一样简单，但似乎因为这些参数是类型，所以它可能是不可能的。

四处寻找答案，我发现 Kind Polymorphism 由 Haskell 中的 -XPolyKinds 启用，这似乎允许这里需要的东西。我是否认为这是 Idris 所缺少的才能使这成为可能？或者在 Idris 中有其他方法可以做到这一点吗？

Answer 1

好吧，Arrows 有一个从属类型，正如您所指出的：

Arrows 0 : Type -> Type
Arrows 1 : Type -> Type -> Type
Arrows 2 : Type -> Type -> Type -> Type
...

请注意，此处 Type 的出现没有任何变化。具体来说，请注意 Type : Type、(Type -> Type) : Type 等。可能是 Int。可能是 n ** Vect n (Fin n)。也就是说，没有类型和种类之分。

所以：

arrowsTy : Nat -> Type
arrowsTy Z = Type
arrowsTy (S k) = Type -> arrowTy k

可用于定义Arrows的类型。

然后你可以定义Arrows:

Arrows : (n : Nat) -> Type -> arrowTy n
Arrows Z a = a
Arrows (S k) a = compose (\b => a -> b) . Arrows k
  where compose : { n : Nat } -> (Type -> Type) -> arrowsTy n -> arrowsTy n
     -- compose is used to modify the eventual result of the recursion
        compose { n = Z } g f = g f
        compose { n = S k } g f = compose g . f

而且，如果你将compose合并到Arrows，你可以得到另一个版本：

Arrows' : (Type -> Type) -> (n : Nat) -> Type -> arrowTy n
Arrows' finalize Z x = finalize x
Arrows' finalize (S k) x = Arrows' (finalize . (\r => x -> r)) k
Arrows : (n : Nat) -> Type -> arrowTy n
Arrows = Arrows' id

是否可以在 Idris 中对种类进行抽象？

Is it possible to abstract over kinds in Idris?

idris