Are very dependent types a good idea?

What’s the difference between dependent and very dependent types? I tried to skim the paper but it was too hard.

A normal function that takes inputs of type A to outputs of type B is denoted as:

A

B

f : A → B

And then you call it as y = f(x). Naturally, the value of y depends on the value of x.

y = f(x)

y

x

Dependent functions generalize this, so that the type of y depends on the value of x. Let’s say I define

g true = “Hello” g false = 0

The input has type bool, but the output may be either string or int. We would write the type of g as:

bool

string

int

g

g : (x : bool) → (if x then string else int)

And in general, a dependent function is denoted thus:

f : (x : A) → B(x)

So in a dependent function, the return type B is parameterised by the input value x.

A very dependent function can also refer to itself in the type of its output. We can thus denote it as:

f : (x : A) → B(f, x)

Note that B may also refer to f now. The paper uses a slightly different notation:

f

{ f | x : A → B(f, x) }

I have not yet understood the consequences of this, or the use cases it would enable. Hence the question: is it a good idea to allow this?

The kind of (→) is Type → Type → Type. What is the kind of Π?

(→)

Type → Type → Type

Π

{-# OPTIONS --type-in-type #-} Π : (t : Set) -> (t -> Set) -> Set Π t f = (x : t) -> f x Π₁ : Π Set (λ t -> (t -> Set) -> Set) Π₁ = Π

Are very dependent types a good idea?