Is it possible to abstract from the species in Idris?

Question

I talk about how to define functions with a variable number of arguments. I am a bit ambitious and wanted to write a mapN function that maps the argument function (n : Nat) to n values ​​for some Applicative type.

Investigating this problem made me think that this is probably not possible, at least also by providing function argument types. This made me try to write a function that takes Nat and a variable number of Type arguments and returns the type of the function, as if you were drawing arrows between types. How in:

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

Here is my best attempt that doesn't work:

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

Unfortunately, none of the type signatures makes sense, because sometimes I want the function to return Type , and sometimes it returns Type -> Type , and sometimes it returns Type -> Type -> Type and so on. I thought it would be about as simple as writing any other function with a variable number of arguments, but it seems that since these arguments are types, this may not be possible.

Looking back at the answer, I met Kind Polymorphism , which was included by -PolyKinds in Haskell, which seems to allow what is needed here. Am I right in thinking that this is what Idris is missing to make this possible? Or is there another way to do this in Idris?

Answer 1

Well, Arrows is of a dependent type, as you already noted:

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

Note that the appearance of Type does not change anything here. In particular, note that Type : Type , (Type -> Type) : Type , etc. It may be Int . This may be n ** Vect n (Fin n) . In other words, there is no difference between types and species.

So:

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

can be used to determine the type of Arrows .

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 } gf = gf compose { n = S k } gf = compose g . f 

And, if you combine compose into Arrows , you can get a different 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