是否有可能在伊德里斯中抽象出来？

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

遗憾的是,这两种类型的签名都没有意义,因为有时候我希望函数返回a Type,有时它会返回Type -> Type,有时会返回Type -> Type -> Type等等.我认为这与使用可变数量的参数编写任何其他函数大致相同,但似乎因为这些参数是类型,所以它可能是不可能的.

寻找答案,我遇到了由Haskell中的-XPolyKinds启用的Kind Polymorphism,它似乎允许这里需要的东西.我是否正确地认为这是伊德里斯为此而失踪的原因？或者在伊德里斯还有其他方法吗？

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