Minimal Core Language | Formal Specification

[sirinath]

I believe for long term viability of Nitra some form of formal specification is needed. Once initial cut of Nitra iss out perhaps remove its dependency on Nemerle. Also perhaps Nitra can become a language of its own.

Some initial thoughts what should be there are:

• HList / HMap based structures
  • Parameter lists are HLists, which are tuples
  • Objects are HMaps of Symbol and type to value or expression
• Pattern matching
• Formal specification of concurrency
• Proofs
• GADT
  • HOAS
• Staging and macros
• Macro based type inference (http://typedclojure.org/)
• Embedded logic and relational programming (http://flix.github.io/, http://www.rascal-mpl.org/)
• Tag types (type based capabilities, effects, annotation types, constraint types, phantom types, Substructural type)
• Nominative and structural typing

This is a brain dump of the ideas:

Creating a symbol

def a // Type Any, Effects {Initializable}, Contains AnyRange, Scope current, etc.

def a = 1.0 // type float
a := a : int // converts value and binding of a to int and mutate

def a = 1.0
def b -< a // a is now unusable, b borrows value of a
b >- a // b is unusable, b gives back value to a 

def a @{Read}
a = 1 // = is only for initialize of 1st assignment
// a := 1 // error

def b @{Read, Write} = 1
b := b + 1

def a: [int @{len(> 10)}] // a is a list of int with a dimension greater than 10
def b: [@{len(> 10)}] // b is a HList with a dimension greater than 10
def c: [<: Number @{len(> 10)}] // c is a HList which contains subtype Number with a dimension greater than 10

def a = 1 -> 2
def b = a[1] // Given 1 return 2
def c = a // c = 1

def d = 1 -> 2 | 3 -> 4 // give 1 or 2 returns 2 or 4

def m: [A -> B] // HMap type A to B
def m: [A => B] // HList function from A to B

def a: Int | Float = 1.0 // int or float
def b: Mamel & Quadruped = dog // should satisfy both types

def a: @{value(1 | 2)} = 1 // a can hold 1 or 2

def a = (1 | 2) -> 'A' // a maps 1 and 2 to 'A'
def b = a[1]

type c = @{values(1 | 2)} // value as types
type c = 1 | 2 // same as above

// types can also be sets of values of values with ordering or partial ordering or unordered. How this is done needs to be thought thought.

type d = 'A'

def e = c -> a
def f = e[1] // same as b

def a = 1
def b = a: @{values((1|2|3) -> 'A' | (4|5|6) -> 'B')} // b is 1; pattern matching
def b = a: (1|2|3) -> 'A' | (4|5|6) -> 'B') // same as above

type c = @{values((1|2|3) -> 'A' | (4|5|6) -> 'B')}
type c = (1|2|3) -> 'A' | (4|5|6) -> 'B') // same as above
def d = a: c // same as b
def e = 1: c // same as b

type A {
  def a: int @{private(<: B)} // private in any subtype of B otherwise accessible in any type which is not a subtype of B
}
// Define type A

type B <: A { // B extends A
  def b: int
}
// B is a subclass of A with additional definition

type C: B // C is an alias for B

type D: B { ... } // D is nominatively considered as B though it has additional functionality. Essentially this is a subtype but D can be substituted where B is expected.

type S :> A {
  def s1: int,
  def init1: () => () @{new(_), init(s1)} = { s1 = 1 }, // When creating a new object run this function which initialises s1
  def s2: int,
  def init2: () => () @{new(_), init(s2, after = init1)} = { s2 = 2 }, // When creating a new object run this function which initialises s2 after init1 is run
  def s3: int,
  def init3: () => () @{new(_), init(s3)} = { s3 = 3 }, // can run in parallel to init1
}

type X<P> <: P // type X is subtype of  P

type Y<Q> = Q { ... } // Y is structure with elements of Q and { ... }
type Y1 = A { ... } // sames as above if Y<A>

type Z = { ... } // Z is a structural type

def s: {def f: int } // defining a structural type

def f: int => int = (a) => { ... } // function name followed by type and body

def f1 = (a) => { a.b } // find b in passed structure
def f2 = (a) => { a._: int } // find unknow symbol of type int in a

def b = 1

f1(_: int) // pass local scope as a record to the function, find all symbols of int type
f([_: int][0]) // pass local scope as a record to the function, find 1st symbols of int type
f([_: int]*.b) // pass local scope as a record to the function, find symbols b of int type

type A = { def f1 = 1 ... }
def b = .f1 // find binding f1

def a = new<A>

def c = a.b // same as a.f1 or in other pseudo language [a].map(_.f1)
def d = a.*[.f1(), .f2(), f3()] // get a list evoking all expression f1, f2 & f3 in a tuple / HList - [a].map((_.f1(), ...))
def e = [o1, o2, o3]*.f1() // for all object o1, o2m o3 evoke f1 getting a tuple - zip([o1]. ...).map(_.f1())
def f = [o1, o2, o3]*.*[.f1(), .f2(), f3()] // For all object in the 1st list evoke expression in the 2nd list getting a nested tuple zip(...).map(((_.f1(), ...), (_.f1(), ...), ...)

def f(a = _ : int) = a // find implicitly a int value
def f() = _: int // find implicitly a int value in scope

type t = int : 1 // dependent type 1
def a: int : 1 = 10 //
def b = a :: type // b is Any:1 
type x = a : ? // x is int
def c = a // c is 10
def d = _: ? : 1 // d is 10
type e = _ :: ? // e is Any:1

@{lazy} - lazy
@{strict} - strict

default is undefined so compiler can use strictness inference.

This is just a 1st impression dump of ideas. Perhaps we can how to refine this. Perhaps someone can take on the formalism part.