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

Question

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

调查这个问题让我认为，如果不至少向函数提供参数的类型，这可能是不可能的。这促使我尝试编写一个函数，它需要一个 Nat和一个可变数量 Type参数并返回一个函数类型，就像在类型之间串起箭头一样。如:

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

不幸的是，这两种类型签名都没有意义，因为有时我希望函数返回 Type有时它会返回 Type -> Type有时它会返回 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