# dependent types

Sub-cards (0)

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:

``````f : A → B
``````

And then you call it as `y = f(x)`. Naturally, the value of `y` depends on the value of `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:

``````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 | 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 `Π`?

``````{-# OPTIONS --type-in-type #-}

Π : (t : Set) -> (t -> Set) -> Set
Π t f = (x : t) -> f x

Π₁ : Π Set (λ t -> (t -> Set) -> Set)
Π₁ = Π
``````