Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Suspended contexts in ΠΣ-calculus: A handy tool for typeclasses, ornaments and restrictions

ΠΣ-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. De nitions 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 de nition has to type check with respect to the
previous declarations and de finitions.

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))
    }
Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 2 comments