Expressing the type of variadic functions in Idris

user_6053778 0
Viewed 77

In the book "Type-Driven developement with Idris" the author explains how to create variadic functions. He takes the example of a adder function that consumes a first parameter n: Nat and then n + 1 integer parameters to be added. In order to declare this function the book introduces the dependent type AdderType so that one can write:

adder: (numargs: Nat) -> (acc: Int) -> AdderType numargs

So far so good. But then the following definition of AdderType is proposed:

AdderType : (numargs: Nat) -> Type
AdderType Z = Int
AdderType (S k) = (next: Int) -> AdderType k

At this point I'm lost. Line AdderType Z = Int makes sense but the last one does not. I would have thought that the expression (next: Int) -> AdderType k had kind Int -> Type, but not kind Type. Does Idris consider that any dependent type is also a type? If yes, does that also apply to type constructor? (That is to say: does a value of kind Type -> Type also have kind Type ?)

Disclaimer: I'm a beginner in type theory so my usage of technical terms like "kind" and "dependent type" might be inappropriate. Please correct me if this is the case.

idris variadic
1 Answers

Eventually I understood my mistake so I'm answering my own question just in case someone else might be interested. I was confusing the kind of (next: Int) -> AdderType k (which is indeed a type) with the value of (next: Int) -> AdderType k (which is the type of all functions from type Int to type AdderType k). What is true is that all the defined types except AdderType Z are function types. But a function type is just a normal type anyway.

The way I could make sense of it was by imagining what would be the result if we could define each AdderType k individually. It would be the infinite list of following definitions:

AdderType Z = Int
AdderType (S Z) = Int -> Int
AdderType (S (S Z)) = Int -> Int -> Int
AdderType (S (S (S Z))) = Int -> Int -> Int -> Int
…

It then became very obvious that each AdderType k is indeed just a normal type. Furthermore each newly defined type could be used inside the right hand side of the following line:

AdderType Z = Int
AdderType (S Z) = Int -> AdderType Z
AdderType (S (S Z)) = Int -> AdderType (S Z)
AdderType (S (S (S Z))) = Int -> AdderType (S (S Z))
…

And at this point the infinite list of definitions (except the first) could be replaced by a single polymorphic definition.

AdderType Z = Int
AdderType (S k) = Int -> AdderType k
user_60537780
Related