Object Oriented Programming Languages with Dependent Types

There are several programming languages with dependet types: Agda, Coq, Idris, Twelf, F*, ATS, Lean, Matita. Most of them are functional only a few are imperative. Only one of them is logical programming languages. There is no object oriented languages with dependent types even for the most easy cases.

Next, we will look at the possibility of the existence of the object-oriented programming language with dependent types. We’ll call it “Green-0”.

Green-0 programming languages

Influenced by

Basically, Green-0 will resemble EO. Perhaps this programming language will help solve the problem of adding TDD to EO.

Built-in types

Green-0 will contain 4 built-in types: Int, Double, Text, Seq. And type Any might need to be the root of the type hierarchy. Then,

type Int is Any
type Double is Any
type Text is Any
type Seq is Any

Simple types

type IntL a: Int is Int where Less: value, a
type IntM a: Int is Int where More: value, a

type IntB a: Int, b: Int
    is IntL b with IntM a
    where Less: a, b

type Nat is IntEqM 0
type LimText a: Nat is Text where Not: More: Length: value, a

IntL is an integer that is less than the specified value a.
IntM is an integer that is more than the specified value a.
IntB is an integer that is greater than a and less than b.
Nat is a natural numbers.
LimText is a text whose length does not exceed the specified value a.

Example

Create type for a book with a limited cost:

type Book a:
    def name ret Text
    def cost ret IntL a
    def test a : Int, b : Int ret Bool where Less: a, b

A method can only return one object.

Yes, method test is not needed for this type, but it will help to demonstrate some ideas.

Create object for him:

object BookL1k is Book 1000 as pr:

    @name : Text
    @cost : IntL pr

    ||| Primary ctor.
    def ctor text: Text, price: Int ret
        @name <- text
        @cost <- price

    ||| Secondary ctor.
    def ctor text: Text ret
        ctor: text, pr

    def name ret @name
    def cost ret @cost
    def test a : Int, b : Int ret And: Less: a, @cost, More: b, @cost

||| Primary ctor. is comment.

Other options:

    ...
    def test a : Int, b : Int ret
        And:
            Less: a, @cost,
            More: b, @cost
    ...
    def test a : Int, b : Int ret
        ls <- Less: a, @cost
        mr <- More: b, @cost
        And: ls, mr

What is the problem with this option? It violates the rule that a method can only return an object. Let’s add a WithLet object and Let object that helps him:

    ...
    def ctor text: Text, price: Int ret
        WithLet:
            Let: @name, text
            Let: @cost, price
    ...
    def test a : Int, b : Int ret
        WithLet:
            Let: ls, Less: a, @cost,
            Let: mr, More: b, @cost,
            And: ls, mr

But it looks a bit unnatural.

It is important to note that all fields of object is final and private. If you want not final field you should use mutual:

object BookL1k is Book 1000 as pr:

    mutual @name : Text
    @cost : IntL pr
    ...

Now you can change its value not only in the ctor:

    ...
    def test a : Int, b : Int ret
        @name <- Lower: @name
        And:
            Less: a, @cost,
            More: b, @cost

Of course, it is advisable to avoid mutable variables.

Conclusion

This is a superficial review of the possibility of creating an object-oriented programming language with a kind of dependent types. Now the most possible use of this language is to solve the problem of adding TDD to EO. When I finally define the language design, I’ll try to create its implementation for the JVM.

comments powered by Disqus