`ΠΣ-calculus by T. Altenkirch et al. is typed turing-complete calculus of partial functions with an exceptionally rich type structure able to accommodate the type-level structure and computational expressiveness of Martin-Löf-style type-theories and their known extensions. It is intended to serve as a core ("sugar-free") language for various dependently typed languages such as Agda and Coq, which lambda calculus fails short to serve as base for. Being partial, ΠΣ allows for the type of all types Type:Type and treats terms and types on equal footing, it fails, however, to treat contexts as first-class citizens.`

By introducing the notion of suspended contexts (which coincide with modules in ML and objects in Scala) we can replace tuples by records (suspended contexts with no interdependencies), pair construction by more expressive dependent concatenation (coincides with type refinements in Scala) and unify (split p with (x, y) -> t) with (let c in t).

The main obstacle to this approach is the complexity of context typing. Product of types defines a type of tuples with no interdepency between members. Dependent products allow for left-to-right dependencies (type of a certain tuple member may depend on values of the members left to it). To provide types for contexts we need to allow circular and mutual dependencies.

Here we propose a way to handle these problem inspired by Dependent Object Types (DOT) calculus, which is being currently developed by members of the Martin Odersky (Scala) team in EPFL.

(In author's opinion, the DOT itself gains lots of unneccessary complexity due to urge to accomodate the legacy inheritance-based polymorphism)

Following [Al1], a partial context is a sequence of declarations x:T and and (possibly recursive) defitions x = t. Denitions and declarations may occur in any order, subject to the following constraints:

- Before a member can be defined, it must be declared;

- Every member can be declared and defined utmost once.

- Every declaration and denition has to type check with respect to the

previous declarations and definitions.

If every declared member is also defined, the partial context is a (total) context. We'll also define a partial order on partial context: "x refines y" iff x can be derived from y by performing the following actions:

- Defining already declared members;

- Narrowing (in sense of nominal subtyping) the types of declared members, if the member is already defined, the value must type check with respect to the new type.

Parentheses containing a comma-separated list of definitions, declarations and external contexts to include will denote a (partial) context. Shorthand x: T = v will denote a declaration x: T immedeately followed by a definition x = v.

Example 1:

(x: Nat, y: Nat = 5)

Example 2:

c = (x: Nat, y: Nat = 5)

d = (c, x = y + 1)

We'll introduce the notation c.(t) for "let c in t" for more similarity to object oriented languages:

c = (x: Nat = 1, y: Nat = 5)

a = c.x

b = c.(x + y)

Every partial context can be used also as type of all (total) context that refine c. We'll define nominal subtyping relation on context types:

a < b iff a can be obtained from b by performing the following actions:

- Declaring new variables;

- Defining already declared variables;

- Narrowing (in sense of nominal subtyping) the types of declared members, if the member is already defined, the value must type check with respect to the new type.

(i.e. refining + declaring new members.)

Boolean and Optional:

Boolean = {'true, 'false}

Optional = (

T: Type,

isVoid: Boolean,

value:

)

The type of natural numbers:

Nat: Type

Nat = (

isZero: Boolean,

pred: Optional(

)

The typeclass of Nat-like objects:

NatStructure = (

N: Type,

zero: N,

succ: N -> N

)

(The type Nat is isomorphic to the N of the free NatStructure. In Haskel and Agda compilers are able to derive the structural definition of Nat from the declarative definition as in NatStructure.)

Type of lists of specified type:

ListOf: Type -> Type

ListOf = (T: Type) => (

isEmpty: Boolean,

head: Optional(T, isVoid = isZero)

tail: Optional(

)

Existentials:

# Type of all lists:

List: Type = (T: Type, ListOf(T))

# Universal type:

Any: Type = (T: Type, v: T)

Type of vectors (ornamented lists):

VecOf: (T: Type, len: Nat) -> ListOf(T)

VecOf = (T: Type, len: Nat) =>

'true => (ListOf(T), isEmpty = 'true) |

'false => (ListOf(T), isEmpty = 'false,

tail = VecOf(T, len.pred))

}

By introducing the notion of suspended contexts (which coincide with modules in ML and objects in Scala) we can replace tuples by records (suspended contexts with no interdependencies), pair construction by more expressive dependent concatenation (coincides with type refinements in Scala) and unify (split p with (x, y) -> t) with (let c in t).

The main obstacle to this approach is the complexity of context typing. Product of types defines a type of tuples with no interdepency between members. Dependent products allow for left-to-right dependencies (type of a certain tuple member may depend on values of the members left to it). To provide types for contexts we need to allow circular and mutual dependencies.

Here we propose a way to handle these problem inspired by Dependent Object Types (DOT) calculus, which is being currently developed by members of the Martin Odersky (Scala) team in EPFL.

(In author's opinion, the DOT itself gains lots of unneccessary complexity due to urge to accomodate the legacy inheritance-based polymorphism)

Following [Al1], a partial context is a sequence of declarations x:T and and (possibly recursive) defitions x = t. Denitions and declarations may occur in any order, subject to the following constraints:

- Before a member can be defined, it must be declared;

- Every member can be declared and defined utmost once.

- Every declaration and denition has to type check with respect to the

previous declarations and definitions.

If every declared member is also defined, the partial context is a (total) context. We'll also define a partial order on partial context: "x refines y" iff x can be derived from y by performing the following actions:

- Defining already declared members;

- Narrowing (in sense of nominal subtyping) the types of declared members, if the member is already defined, the value must type check with respect to the new type.

Parentheses containing a comma-separated list of definitions, declarations and external contexts to include will denote a (partial) context. Shorthand x: T = v will denote a declaration x: T immedeately followed by a definition x = v.

Example 1:

(x: Nat, y: Nat = 5)

Example 2:

c = (x: Nat, y: Nat = 5)

d = (c, x = y + 1)

We'll introduce the notation c.(t) for "let c in t" for more similarity to object oriented languages:

c = (x: Nat = 1, y: Nat = 5)

a = c.x

b = c.(x + y)

Every partial context can be used also as type of all (total) context that refine c. We'll define nominal subtyping relation on context types:

a < b iff a can be obtained from b by performing the following actions:

- Declaring new variables;

- Defining already declared variables;

- Narrowing (in sense of nominal subtyping) the types of declared members, if the member is already defined, the value must type check with respect to the new type.

(i.e. refining + declaring new members.)

**By example**Boolean and Optional:

Boolean = {'true, 'false}

Optional = (

T: Type,

isVoid: Boolean,

value:

**case**isVoid**of**{'true => () | 'false => T})

The type of natural numbers:

Nat: Type

Nat = (

isZero: Boolean,

pred: Optional(

**Rec**[Nat], isVoid = isZero))

The typeclass of Nat-like objects:

NatStructure = (

N: Type,

zero: N,

succ: N -> N

)

(The type Nat is isomorphic to the N of the free NatStructure. In Haskel and Agda compilers are able to derive the structural definition of Nat from the declarative definition as in NatStructure.)

Type of lists of specified type:

ListOf: Type -> Type

ListOf = (T: Type) => (

isEmpty: Boolean,

head: Optional(T, isVoid = isZero)

tail: Optional(

**Rec**[ListOf(T)], isVoid = isZero))

Existentials:

# Type of all lists:

List: Type = (T: Type, ListOf(T))

# Universal type:

Any: Type = (T: Type, v: T)

Type of vectors (ornamented lists):

VecOf: (T: Type, len: Nat) -> ListOf(T)

VecOf = (T: Type, len: Nat) =>

**case**len.isZero**of**{'true => (ListOf(T), isEmpty = 'true) |

'false => (ListOf(T), isEmpty = 'false,

tail = VecOf(T, len.pred))

}