Language Notes

(Anya's comments in bold)

• What parameters are for on a concept
• Environment
• Fix the module system
• Choose what the internal representation for polymorphic types
• Fix the template system
• Concepts
• Repeat statement
• A syntax that works with dependent types, overloading, templates and concepts
• No signature
• Yet another core language

What parameters are for on a concept

Ok, so we are able to give a name to a model and have several model of the same concept with same arguments. For example:

concept Monoid<type T> {
 function T _+_(obs T a, obs T b);
}

model foo = Monoid<int> {
 function T _+_(obs T a, obs T b) = a+b;
}

model bar = Monoid<int> {
 function T _+_(obs T a, obs T b) = a*b;
}

The thing is that, if we continue this process. What is the point having parameters? I can write:

concept Monoid {
 type T;
 function T _+_(obs T a, obs T b);
}

model foo = Monoid {
 type T = int;
 function T _+_(obs T a, obs T b) = a+b;
}

model bar = Monoid {
 type T = int;
 function T _+_(obs T a, obs T b) = a*b;
}

procedure Foo(obs T a)
 forall type T
 requires m = Monoid
 m::T == T
{}

I know it looks kind of crazy. But the only difficulty we get here is to find automatically the model when there is only one available. Now, what about concept template? Well it will look exactly like the first one and ease the syntax.

concept Monoid forall type T {
 function T _+_(obs T a, obs T b);
}

model foo = Monoid(int) {
 function T _+_(obs T a, obs T b) = a+b;
}

model bar = Monoid(int) {
 function T _+_(obs T a, obs T b) = a*b;
}

procedure Foo(obs T a)
 forall type T
 requires m = Monoid(T)
{}

I just think that having special kind of parameters to concepts just make the language worse, and I would prefer to reuse the template system. Also have the same syntax that the rest to avoid confusion for people. In general, I want to have "forall" everywhere. Maybe the second notation is a bit hard to handle, but it makes sense to use the third one.

-- Valentin

Environment

I have thought about how a nice uniform environment would look like. A bit more developed than my last email.

Let's have \Gamma, our environment. \Gamma: I -> C

I is a set of qualified identifiers. And C, I call it a "class" of modules, types or objects.

I have c \in C, c: List(A) -> A c is partial.

A is a set of concrete types or objects. It is like an "address", a constant and unique definition. We might want to also have compile-time computable constants, like on integers.

For a class, it will be something like class Foo(int), or a module, we could also use the same notation, module Foo(int). The nice thing for having the type "int" as parameter for a module is like for a class, we can have several instantiation when we come to templates. But note we do not have templates yet. For the moment we can have specializations in some ways. For example, I can write.

class Foo(int) { ... }
class Foo(float) { ... }

we have c: int \mapsto ... and float \mapsto ...

But it is not polymorphic yet, it is kind of part of the name.

What about the List(A) of functions and procedures? It is basically the list of types. Then we have overloading for free.

We can also extend it to all objects of our languages, even variables.

var baz(int) = somecall();
var baz(float) = someothercall();

Note that the type of baz(int) does not have to be int.

Now let's add polymorphism:

What I do when I do a "forall" is basically give several mapsto in my map (from C).

class Foo(T) forall T { ... }

It basically means: \forall T, I have Foo: T \mapsto ...

We need to think of course about the order of resolution when we have several polymorphic objects or types that are ambiguous.

Now, concepts:

class Foo(T) forall T where b = Bar(T) { ... }

It basically means: \forall T where there is a model m of concept Bar(T), I have Foo: T \mapsto ...[b->m]

My "Bar" here was a concept, it behaves like a predicate.

I can define a concept, like that:

concept Bar(T) forall type T {
 ...
}

If this is a auto concept, I can add:

m = model Bar(T) forall type T {}

Otherwise, I can do a simple model like that:

m = model Bar(int) {}

I had my environment like that. \Gamma

Foo \mapsto Foo_def Bar \mapsto Bar_def

Foo

\forall T where there is a model m of concept Bar(T), I have T

\mapsto ...[b->m]

Bar

int \mapsto {}

A model really looks like a class. But a concept is something that did not exist before. I am actually thinking we could have no model, just classes. But classes have the power of namespaces.

concept Picard(T) forall T {
 type Kirk;
 void Spock(obs Kirk);
}

void Spock(obs float f) {...}
class Data models Picard(int) {
 type Kirk=float;
}

Then we can make quick classes that models our concept. But if we want to make a model for several types, for example:

concept Convertible(T, U) forall T {
 U(obs T);
}

float(obs int i) {...}
class IntToFloat models Convertible(int, float) {
}

Axioms are only on concepts. All we need in a model should be certainly available in a class. The interesting thing is that we model several concepts with only one class.

concept A(T) forall T { void foo(); void bar(); }
concept B(T) forall T { void foo(); void baz(); }
class C models A(int), B(float) {
 static void foo() {...} // this one is for both A(int) and B(float)
 static void bar() {...}
 static void baz() {...}
}

In concept C++, we would try:

concept A<typename T> { void foo(); void bar(); }
concept B<typename T> { void foo(); void baz(); }
concept_map A<int> {
 void foo() {...}
 void bar() {...}
}
concept_map B<float> {
 void foo() {...} // we redifine?
 void baz() {...}
}

And then conclude we should extract foo:

concept A<typename T> { void bar(); }
concept B<typename T> { void baz(); }
concept AandB<typename T, typename U>: A<T>, B<T> { void foo(); }
concept_map AandB<int,float> {
 void foo() {...}
 void bar() {...}
 void baz() {...}
}

Hope it makes sense for you.

-- Valentin

Fix the module system

It is impossible with the current implementation to include automatically several modules in the same time without having to list all the module each time. This is due to the fact that importing a module does not make the import of what the imported module needs. There are two ways to fix it.

• Having an external configuration system. Which I am completely against since it is yet another system to maintain.

• Having a clean system of module where we can re-export what we import. Usually we need two kind of import keywords.

Importing a module does recursively import its dependencies, though those dependecies aren't imported into the local namespace, i.e., you can't refer to them by short names without importing the module in the current module. But imported names aren't re-exported as short; this is certainly useful sometimes (making 'bundle' modules) -- Anya

Choose what the internal representation for polymorphic types

We have patterns and forall annotations. First of all, the forall should be part of the type and not of the definition. I would tend to take forall, since it is better to extend with concepts. Whereas patterns are hard to extend with requirements.

Attaching to the definition is bad, and inconvenient. Patterns are very convenient to work with in overload resolution. Putting concept requirements in the pattern variables could solve the problem:

function Ring.T foo(Ring.T a);

This would make semantic analysis of foo's definition trivial.

-- Anya

Fix the template system

Having a half system of template does not really help us. Not very hard to have partial specialization. And would be really benefic. Moreover

class A(T) forall T or class A(?T) are OK. But class A(type T) is not really sound. What does it mean if T is already declared? Obviously it should become a specialization. This is adding context in parsing. Also parameters should be the same as functions. And the name of the parameter is anonymous. We get then dependant types nearly for free. Also, we need a way to say "whatever object of a given type". I propose ":int" for example for a "whatever" object of type int.

class A(T) forall T {}

A(:int) or even A(0). Which should be the same.

class A(int i) {}

A(0) and A(1) are different types because i is not anonymous. A is a dependant type. But the class in the implementation should be the same. We will just have to check when assigning at run time that we keep the same i.

A last reason why I want to say class A(T) forall T, instead of class A(?T) is because of multiple models with concepts.

class A(T, model m) forall T where m is Somethingable(T) {}

Which give me the opportunity to give a model as parameter.

Specialisation is nice and useful, but has low priority

-- Anya

Concepts

Repeat statement

For repeat statement to work we need concepts to work. This will enable us to pass lambda abstractions with local context. Pretty simple to do realize when the concept works.

There will be also a lot of work a posteriori on inlining code.

BTW, there is an inliner available for both functions and procedures -- Anya

A syntax that works with dependent types, overloading, templates and concepts

I try to see how to re-factor the Magnolia syntax so that we have only one rule for any variable, procedure, functions and class.

First the keyword "var" means we can reassign. But only with the same type. And "define" is a constant. Most of the time, we want to "define" classes, functions and procedures. But after all it is just a name.

   "var" -> ConstMode {cons("Var")}
   "define" -> ConstMode {cons("Const")}

Here is my rule:

   ConstMode Declarator (":" Type)?  ("=" Expr)? ";" -> Decl
   Identifier? Params? ForAllClause? -> Declarator
   "(" ParamList ")" -> Params
   {Param ","}* -> ParamList
   ParamMode? Type AbsDeclarator
                               -> Param

   "forall" {ForAllParam}+     -> ForAllClause
   "type" Declarator           -> ForAllParam
   Param                       -> ForAllParam

   Type Params ForallClause?   -> Type
   "class"                     -> Type
   "procedure"                 -> Type
   "model" Identifier "(" {Expr ","}* ")" -> Type
   "concept"                   -> Type
   Identifier                  -> Type

   "{" Stat* "}"               -> Expr
   Decl                        -> Stat

We should forbid the case we have neither an expression or a type. Blocks become expressions. Blocks declaring variables can be considered as structures. If we want member functions... anyway we can define whatever we want as a member. I would say that as members "var" becomes an object field, and "define" becomes a class field. But I am maybe wrong on the last point.

Here are some example.

var i = 3;
var i : int = 3;
var i : int;
var i(int) = 3; // Works like a variable, since we do not care about
the first parameter. We access to it by i(:int).

define foo(T i) forall type T, C(T) m : T = {
 return i;
};
//note that C is a concept, and we here say that there should be a
model m for C(T).

//The same with passing the model as parameter:
define foo(T i, C(T) m) forall type T : T = {
 return i;
};

define foo(obs T i) forall type T, C(T) m : procedure = {
 return i;
};

//Remark you can always just declare:
define foo(obs T i) forall type T, C(T) m : procedure;

//Or:
define foo : procedure(obs T) forall type T, C(T);
//Note that with the second declaration, we cannot overload foo.

define Pair(T, U) forall type T, type U : class = {
 var T fst;
 var U snd;
};

//Declaration:
define Pair(T, U) forall all type T, type U : class;
//Or to forbid overloaded definitions:
define Pair: class(T, U) forall all type T, type U;

//And now the dependent type:
define Array(int size, T) forall type T : class;

//A function that takes a dependent type as parameter:
define foo(Array(N, T) a) forall int N, type T: T = {
 //Here we have access to N, since we unpacked Array.
};

//To pass a type template as parameter:
define foo(A) forall type A(T) forall type T: procedure;
//If we have a second lever of forall, it is because

//A concept definition:
define A(T) forall type T : concept {
 //signature definition.
};

//A model definition:
define m : model A(int) {
};

//A default model definition
define : model A(int) {
};

//A typedef:
define foo = int;

-- Valentin

No signature

If we want to simplify everything, we can say that struct and concepts are signatures, whereas concept maps, objects, functions and procedures are models. We can even put modules into the game. A module defines a signature and a model. The model would correspond to the global variables defined within the module. There is only one module model for each module.

But we can got even one step further. We can generate the minimum signature for a model. Then we could define everything as models. With eventually an incomplete definition.

define HasPlus = model(T) forall type T {
  define plus(T, T): T;
}

define m = HasPlus(:int) {
  define plus(int a, int b): int = a*b;
}

-- Valentin

Note that a struct isn't just a set of operations to manipulate objects -- you can treat it like that when you're programming (an abstract data structure), but a concrete data structure also has things like size, layout, alignment requirements, ...

-- Anya

Yet another core language

forall T
// The reason we pass the T on the right hand side of the satisfaction
// relation, is for having a static parameter.
define Monoid(|=T) {
  define op(out |= T, obs |= T, obs |= T);

  axiom Assoc(a |= T, b |= T, c |= T) {
    op(a, op(b, c)) == op(op(a, b), c);
  }
}

forall T
define Semigroup(|=T) {
  // We name our signature morphism and say it has to obey the
  // satisfaction relation. It means, we import the axioms.
  // The signature morphism is injective (i.e. op -> op), so
  // we do nto define it.
  define op(out o |= T, obs a |= T, obs b |= T);

  define phi |= Monoid(|=T) {
    //It should find automatically the op defined one level up.
  }
  // |=T is an anonymous expression of type T.


  define identity_elt(out |= T);

  axiom Identity(a |= T) {
    op(a, identity_elt) == identity_elt;
    op(identity_elt, a) == identity_elt;
  }
}

/*
 //We could have defined it as an implicit Monoid with th
 //following definition (implicit morphism).
 forall T
 define Semigroup(|=T) |= Monoid(|=T) {
   define identity_elt(out |= T);

   axiom Identity(a |= T) {
     op(a, identity_elt) == identity_elt;
     op(identity_elt, a) == identity_elt;
   }
 }
*/

define m |= Semigroup(|=Int) {
  // This is default satisfaction with a non
  // injective signature morphism.
  define op(out r |= Int, obs a |= Int, obs b |= Int) {
    r = a + b;
  }
  define identity_elt(out o |= Int) {
    o = 0;
  }
}

// Here is an example where we can choose the model
forall T
define foo(a |= T, b |= T, out c |= T, model |= Monoid(|=T)) {
  c = model.op(a, b);
}

// Here, it will pick the only model available.
forall T, model |= Semigroup(|=T)
define foo(a |= T, b |= T, out c |= T) {
  call foo(a, b, c, model.phi);
}

forall n |= Int
define main(out return |= Int, params |= array(|=string, n)) {
  var i |= Int { }
  i = new 42; // new does a copy of the constant 42. Since 42
              // represents a constant implementation that satisfy
              // Int.
  var j |= Int { }
  j = new 51;
  call foo(i, j, return);
}

-- Valentin