Dependent Classes

Introduction

A dependent class is a class whose structure depends on arbitrarily many objects; this dependency is expressed explicitly over class parameters, rather than by nesting. In a sense, dependent classes can be seen as an combination of virtual classes with multi-dispatch. This combination is an improvement from the perspective of both VCs and MD: It makes VCs more extensible by abandoning the strict hierarchical nesting structure, and it makes MD more expressive because more programs are statically type-safe. The notion of path-dependent types, as employed by most proposals for static type systems for virtual classes to keep track of the dependencies between a type and the ``family'' or ``enclosing'' object, is generalized as well, such that types can depend on an arbitrary number of objects described by paths.

People

Mira Mezini
Klaus Ostermann
Vaidas Gasiunas

Implementation of Dependent Classes

vcⁿ Calculus

The operational semantics and type system of dependent classes are defined by vcⁿ calculus.

Implementation of the Calculus

An interpreter for vcⁿ is can be downloaded here

The steps to start the compiler

• Install the Glasgow Haskell Compiler.
• Unpack the intepreter files
• Start the GHC interactive environment
• Load MVC.hs
• Call function exec with an input file name: exec "example.mvc". The exec function will find declaration of main() and start its constructor.

Use our examples to test the interpreter:

• nat.mvc - natural numbers.
• func.mvc - operations on functions.

Soundness Proof

The soundness of vcⁿ is established via a machine-checked type soundness proof in Isabelle/HOL. Follow the links below to download the proof files or the generated documents:

Theory files in a zip archive
Browse theory files online
Proof document
Proof outline

The proof was checked with Isabelle build of 17-Sep-2006.

Completeness of Path Equivalence

We have formulated a property the defines compleness of path equivalence relation: If for all values v that are allowed in certain context expressions v.p and v.p' evaluate to the same result, then the paths p and p' must be equivalent in that context. Below you will find an informal proof of this property for our calculus.