Is it possible to abstract over kinds in Idris?

Question

I'm going through Type Driven Development with Idris, learning about how to define functions with variable numbers of arguments. I got a little ambitious and wanted to write a mapN function that would map a function of (n : Nat) arguments onto n values of some Applicative type.

Investigating this problem led me to think that it was probably not possible without at least also providing the types of the arguments to the function. This led me to try to write a function that would take a Nat and a variable number of Type arguments and return a function type as if you'd strung arrows between the types. As in:

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

Here was my best attempt, which doesn't work:

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

Unfortunately neither of the type signatures make sense, because sometimes I want the function to return a Type and sometimes it returns Type -> Type and sometimes it returns Type -> Type -> Type and so forth. I thought this would be roughly as straightforward as writing any other function with a variable number of arguments, but it seems that because those arguments are types, it might be impossible.

Looking around for an answer, I came across Kind Polymorphism enabled by -XPolyKinds in Haskell which seems to allow what's needed here. Am I correct in thinking that this is what Idris is missing for this to be possible? Or is there some other way to do this in Idris?

Answer 1

Well, Arrows has a dependent type, as you've noted:

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

Note that the appearance of Type here changes nothing. Specifically, note that Type : Type, (Type -> Type) : Type, and so on. It could be Int. It could be n ** Vect n (Fin n). In other words, there is no distinction between types and kinds.

So:

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

can be used to define Arrows's type.

And then you can define 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

And, if you merge compose into Arrows, you can get another version:

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