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
Basically, Green-0 will resemble EO. Perhaps this programming language will help solve the problem of adding TDD to EO.
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
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
IntM is an integer that is more than the specified value
IntB is an integer that is greater than
a and less than
Nat is a natural numbers.
LimText is a text whose length does not exceed the specified value
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.
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.
... 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
object BookL1k is Book 1000 as pr: mutual @name : Text @cost : IntL pr ...
Now you can change its value not only in the
... 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.
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.