dok/spec/OOP

Paradigm

In Dok, OOP is used for:

• specifying type variants, like Algebraic Data Types in FP;
• specifying classes of objects satisfying some properties, like class in FP, or interface in OOP;
• grouping functions on the same subject, like in traditional OOP;

So in Dok, OOP has a FP semantic, but an OOP syntax.

In Dok, OOP is not used for specifying a run-time system of cooperating objects. Other paradigms will be used instead. In Dok, OOP systems are not live-systems, like in Smalltalk or Self. For the run-time system, Dok will use paradigm/runtime-oriented-programming. In Pharo and Smalltalk, OOP is very powerful because: everything is an object; metaprogramming using OOP. But it can create also obscure code because every part of an OOP application can be hidden in class, metaclass and similar customizations.

In Dok, OOP inheritance is not used for maximizing code reuse. Instead it is preferred feature/chunk-oriented-programming at level of “data”.

Data

data is a physical type. It can:

• have variants, like in an AST
• implement one or more classes

The type of data like /A/B conforms to:

• its specific type /A/B/
• the type of its parent /A
• the type of all classes it implements

data DAI [
  slot prefix::String

  variant ../Zero [ slot suffix::String ]

] -isa A(Int) [

  fun a(x::String)::Int -specialize {
    return x.to(Int)
  } -when ../Zero {
    return 0
  }

  fun af(x::String)::Float {
    return self.a(x).to(Float)
  }
] -isa ... [ ... ]

data cannot subtype from another data. In these cases feature/syntax-abstractions is used, for reusing code.

TODO an external library in Dok is shipped with source code and the user can add patches for chunking part of the code and reuse them, or they can indicate all the code with a formula. Write some example.

Reuse of code between between different data but common parts, is done using feature/chunk-oriented-programming.

Variant Types

They are like sum-types in FP. There is a base object, and then slightly different variants. A method defined for a parent object, is valid for all variant sub objects if not redefined.

Only leaf variant types can be directly istantiated.

Classes

Class is a list of methods with contracts. They support multiple inheritance and subtyping rules. They are similar to interfaces in Java and traditional OOP, and to class in Haskell and FP language with ad-hoc polymorphism.

Class has the same semantic of data in Dok, except that it does not support variants specified inside the class. In class functions are usually abstract, because a class represents an abstract concept, and not concrete data like data.

class A(T::Number) [
  fun a(x::String)::T -abstract {
    :require x.to(Int)
    :ensure ~result.to(Int) > 0
  }
]

class B(T::Number) -isa A [
  fun a(x::String)::T -specialize {
    :ensure ~result.to(Int) > 10
  }

  fun zero::T -abstract {
    :ensure ~result.to(Int) == 0
  }
]

TODO Locale vs Class

Locales and class are parametric theories.

In Isabelle there are locale and class. A class associate some properties to only a type, while a locale can describe more complex relationships between different types.

In practice the majority of structure in math and expecially in programming can be expressed using class.

In Dok I use only class.

Note that a class is different from a module.

TODO if the same data can be an instance of the same class in different ways, then I can define type aliases like data T2 isa T1, and all previous definitions remain valid, and I can override other definitions.

slot vs fun

In a FP language like Haskell there is not a clear difference between a “slot” and the result of a function, because all values are thunks that can be calculated on demand.

Also in Dok, the code involving values is declarative code that is referential transparent. So slots can be transformed during compilation passes to call to functions calculating their value.

Type params

Type params are used for defining a (generic/parametric) type template, that can be used for defining different types, using different parameter values.

In Dok type params can store both type and normal values, but they are not a form of dependent-types, because Dok follows feature/refinement-types approach. Params starting with upper case letter are associated to types. Params starting with lower case letters to values.

Type params can be seen as read-only slot of a value, that do not change after value creation. For example if we create a Map from String to Int, these two params never change after we created the object, while the content of the Map can change.

Type variants can not have additional type parameters. They can only reuse the type params of the parent type. This simplifies the semantic and readability of the language, because type params are all declarated up-font.

On the contrary distinct inner types can introduce new type params, because they are used like distinct service types, and the hosting type is not related to them.

class Bounded-container(Of::Any, max-size::Int) [

  fun size::Int -abstract {
    :ensure ~result <= max-size
  }

  fun !add(v::Of) -abstract {
    :require self.size < max-size
    :ensure self.sive == ~old.size + 1
  }
]

Object constructors

Both class and data can have constructors. They are actions setting all the slots of the data.

data Point [

  slot x::Double
  slot y::Double

  init {
    #-NOTE this is the default constructor. In this case it is not necessary, because slots are already initializated to their default values.

    set self.x 0
    set self.y 0
  }

  init !polar(r::Double, t::Real) {
    :# Init the point using polar coordinates.

    set self.x r * t.cos
    set self.y r * t.sin

    #-NOTE for being a valid creation procedure all not initialized fields must be set to an initial value, otherwise the compiler will signal an error
  }

  init !cartesian(x::Double, y::Double) {
    do self.default!()
  }
] -isa Eq [ :derive ]

var p1::Point(with x 10, with y 20)
# explicit setting of slots

var p2::Point
# call p2.default constructor

var p3::Point.cartesian(10, 20)

var p4::Point
do p4.!cartesian(10, 20)
assert p4 == p3

do p4.!default
assert p4.x == 0 && p4.y == 0

assert p1.default.x == 0
assert p1.x == 10

No Runtime Reflection + JIT

In Pharo and Smalltalk there is runtime reflection and metaprogramming + JIT. Then the code become fast, also without compile-time CL macros. But not so much fast.

Dok follows a compile-time approach:

• there is no run-time reflection
• metaprogramming is only at compile time

Usage examples

• dok/example/Algebraic-Data-Type
• dok/example/OOP

Generalized Abstract Data Type (GADT)

In Haskell a type can be extended with a phantom type, that can be used as constraint. Type constructors are seen as functions from type parameters to final type. The type param is an exact type, and it is used both as input type for the type constructor and output type for the constructed type.

data Expr a where
    I   :: Int  -> Expr Int
    B   :: Bool -> Expr Bool
    Add :: Expr Int -> Expr Int -> Expr Int
    Mul :: Expr Int -> Expr Int -> Expr Int
    Eq  :: Eq a => Expr a -> Expr a -> Expr Bool

eval :: Expr a -> a
eval (I n) = n
eval (B b) = b
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Eq  e1 e2) = eval e1 == eval e2

In Dok, the type system is simpler, but requirements can be added to it. It is based on feature/refinement-types.

data Expr {

  attr value::OneOf(Int, Bool)

  variant ../I [ slot x::Int ]
  variant ../B [ slot x::Bool ]
  variant ../Add [
    slot x::Expr
    slot y::Expr
    :require self.x.value.isa(Int)
    :require self.y.value.isa(Int)
  ]
  variant ../Mul [
    slot x::Expr
    slot y::Expr
    :require self.x.value.isa(Int)
    :require self.y.value.isa(Int)
  ]
  variant ../Eq [
    slot x::Expr
    slot y::Expr
    :require self.x.value.isa(self.y.value.type)
    :require self.x.value.isa(Eq)
    :require self.x.value.isa(Eq)
  ]

  visit self -when ../I {
    set self.value self.x
  } -when ../B {
    set self.value self.x
  } -when ../Add {
    set self.value self.x + self.y
  } -when ../Mul {
    set self.value self.x * self.y
  } -when ../Eq {
    set self.value self.x == self.y
  }
]

Type aliases

Sometime it is useful giving a better name to an already existing data.

data Age -like Int

In every place where an Int is expected, an Age can be used instead.

If new functions are added to Age, then these are definitions also for Int, despite they make more sense in the domain of Age.

This is not similar to inheritance because Age isa Int && Int isa Age. They are two synonymous.

New Types

In Haskell, newtype is usually used for creating a type similar to another one, but with different implementations of some class. For example:

newtype NT = NT Int

instance Show Int where
  show (NT x) = "int:" ++ show x

In Dok, this is supported using feature/syntax-abstractions

data NT -copy Int [
  fun show::String -specialize {
    return "int:${self.to(Int).show}"
  }
]

Tuple

In Dok tuples are objects with slots named like x0, x1, and so on.

var t1::Tuple [
  3
  "hello"
]

assert t1.x0 == 3 && t1.x1 == "hello"

var $my_named_tuple := Tuple[
  field s0 : Int = 3
  field s1 := "Hello"
  "World"
]

assert {
  $my_named_tuple:
    ~.isa(Tuple)
    ~.s0 == 3
    ~.s1 == "Hello"
    ~.x2 == "World"
    ~.x[0] == ~.s0
    ~.len == 3
}

data can be converted to tuple

data Division-result [
  slot quotient::Int
  slot remainder::Int
] -isa Tuple [ :derive ]

Copy of Objects

Already created objects can be used as initial prototype for a new value.

data Person [
  slot name::String
  slot surname::String

  fun complete_name::String {
    self.name + " " + self.surname
  }
]

var p1::Person(with name "Massimo", surname: "Zaniboni")
var p2::Person

set p2 p1.(with surname: "Zanziboni")

assert {
  p1.name == p2.name
  p1.surname == "Zaniboni"
  p2.surname == "Zanziboni"
}