dependent types

Sub-cards (0)Archived
Comments (2)
Reply

Are very dependent types a good idea?

Profile picture

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

Profile picture

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?

Reply

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)
Π₁ = Π