Typesystem: Parametrized types

Hi,

I'd like to create a Language for a functional programming language
featuring algebraic data types and Hindley-Millner type system.

Defining the Concepts and the appropriate scoping Constraints was
straightforward, but I'm stuck at defining the type system because I
don't know how to create parametrized types.

Here's an example showing the Language and showcasing my problem.
Let's say I have the following type definitions:

DefType "List"
    typeformals:
        DefTypeVar "T"
    constructors:
        DefConstructor "Nil"
        DefConstructor "Cons"
            formals:
                RefTypeVar -> T
                TypeDesc -> List
                    typeactuals:
                        RefTypeVar -> T

(hopefully the notation makes sense; "->" means the given Concept is a
reference concept with the appropriate field pointing to the
DefTypeVar or the DefType with the given name).

Now I want to determine the type of the expression

RefConstructor -> Cons
    actuals:
        A
        B

where A and B are some other expressions.

The type equations arising are (with t1, t2 and t3 being type
variables, and E being the node of the whole expression)

TypeOf(A) :==: t2
TypeOf(B) :==: t3
t2 :==: t1
t3 :==: List(t1)
TypeOf(E) :==: List(t1)

The problem, then, is how to represent the type "List(t1)", that is, a
type that points to the given DefType in the Solution, and also points
to some type variables that are freshly created by the typesystem rule.

6 comments
Comment actions Permalink

Hi Gergo,

1)to create a new type variable, say V, inside a rule you write "var V"

2)a type is simply a node, so a type with a var inside it, is just a node of an appropriate concept which has a reference to type declaration and a variable as its child in a certain role.

to write a statement which creates such a type in a type rule, you may use

- either simple smodel language:

node<TypeDesc> td = new node<TypeDesc>();

td.declaration.set( *here you write code which returns a type declaration* )

td.typeactuals.add(V);

(with "declaration" and "typeactuals" being appropriate links)

- or use quotations and antiquotations to simplify your task and make it more visual, in a such way:

you type "<List(%(V )%)>", where < > are quotation brackets, %( )% are node-antiquotation brackets, List( ... ) is (an editor for) your TypeDesc which has a reference to List.

see also http://www.jetbrains.net/confluence/display/MPS/Typesystem#Typesystem-quotations

Regards, Cyril

0
Comment actions Permalink

Thanks for your answer.

I can't really use quotes/unquotes because the DefType itself ('List' in the example) is in the Solution, not in the Language. But the crucial information that you gave me was the possibility of treating typevars as simple Nodes -- and that solved this problem for me.

However, it seems the typevars somehow "disappear"...

Moving on with the previous example, there needs to be a mapping from

Here's the code I wrote to calculate the type of a RefConstructor:

node<DefConstructor> defconstructor = expr.decl;
node<DefType> deftype = defconstructor.ancestor<concept = DefType>;
node<TyAlgebraic> ty = new node<TyAlgebraic>(<no prototypeNode>);
ty.supertype = deftype;
map<node<DefTypeVar>, node<>> mpTypeformalTypevar = new hashmap<node<DefTypeVar>, node<>>;
foreach typeformal in deftype.typeformals {
  var tTypeformal ;
  mpTypeformalTypevar[typeformal] = tTypeformal;
  ty.typeactuals.add(tTypeformal);
}
typeof(expr) :==: ty;

ensure defconstructor.formals.count == expr.actuals.count   reportError "len(formal) != len(actual)" -> expr ;
for (int i = 0; i < defconstructor.formals.count; ++i) {
  node<TypeExpr> formal = defconstructor.formals.skip(i).first;
  node<Expression> actual = expr.actuals.skip(i).first;
  typeof(actual) :==: TypecalcHelper.TyFromTypeExpr(formal, mpTypeformalTypevar);
}

TyFromTypeExpr is the part that traverses the signature of a constructor. Using the names from the example in my original post, it's the code that creates the type homomorphism generated from T->t1, thus returning t1 for T and List(t1) for List(T)


public static node<> TyFromTypeExpr(node<TypeExpr> typeexpr, map<node<DefTypeVar>, node<>> mpTypeformalTypevar)

{
  if (typeexpr.concept.isExactly(RefTypeVar))

  {

    return mpTypeformalTypevar[((node<RefTypeVar>) typeexpr).decl];

  }

 
  node<TypeDesc> td = (node<TypeDesc>) typeexpr;
  node<TyAlgebraic> typedesc = new node<TyAlgebraic>(<no prototypeNode>);
  typedesc.supertype = td.decl;
  foreach typeactual in td.typeactuals

  {
    typedesc.typeactuals.add(TyFromTypeExpr(typeactual, mpTypeformalTypevar));
  }
  return typedesc;
}

(as an aside, would it be possible to avoid having to write a standalone function for this, and use some MPS facility to pass down the map as some kind context?)

Now, the problem is, using the code above to infer the type of the expression

Cons True Nil

I get, as the type of the node "True", TyAlgebraic(supertype: Bool) which is correct, as the type of "Nil", TyAlgebraic(supertype:List, typeactuals:TyAlgebraic(supertype:Bool)) which is also correct, however, the typeactuals of the outermost expression, that of "Cons True Nil", has somehow vanished and its type is reported simply as TyAlgebraic(supertype:List).

0
Comment actions Permalink

I can't really use quotes/unquotes because the DefType itself ('List' in the example) is in the Solution, not in the Language.

1) Oh yes, sure. Sorry. But, if you want to, you may also create antiquotations for referents, not only for children: enter reference antiquotation, ^( )^ inside your quotation, in a cell where a reference to a type def is supposed to be.

2) Text of your code seems to be correct. It's better if you send us your project where you have a problem, so we'll be able to find out what is a source of your problem. Cyril.Konopko@jetbrains.com

Regards, Cyril

0
Comment actions Permalink

Hi,

Thanks for the offer. I've uploaded what I've so far written to http://gergo.erdi.hu/projects/mps/Funny.zip. Let me know if you have any insights.

Thanks,

     Gergo

0
Comment actions Permalink

Hi Gergo,

1) I've found the problem's source: the problem happened because a node (a type variable in your case) can't have many parents, in your case the same variable tried to be a child of List a type of outer Cons and List which is a type of inner Nil. So when it was set as a child for the second time it was detached from the former parent and reattached to the new one.

Fortunately, quotations and antiquotations mechanism of typesystem engine detects and resolves such situations, so I re-wrote your method TyFromTypeExpr as follows:


public static node<> TyFromTypeExpr(node<TypeExpr> typeexpr, map<node<DefTypeVar>, node<>> mpTypeformalTypevar) {
  if (typeexpr.concept.isExactly(RefTypeVar)) { return mpTypeformalTypevar[((node<RefTypeVar>) typeexpr).decl]; }
  node<TypeDesc> td = (node<TypeDesc>) typeexpr;

// change:
  nlist<> tActuals = new nlist<>;
  foreach typeactual in td.typeactuals {
    tActuals.add(TyFromTypeExpr(typeactual, mpTypeformalTypevar));
  }
  node<TyAlgebraic> typedesc = <supertype ^( td.decl )^ typeactuals *( tActuals )*
  >;

//~change


  return typedesc;
}

and types of your Cons ( True Nil )  became correct. Hence I recommend you to do it, too.

2) An inference rule highlights its applicable node red, if an equation inside it is broken. But in an inference method an equation doesn't know which node to highlight, so it's good to provide a node for an equation, which will be highlighted if an equation is broken. For instance, in your inference method TyInstantiateConstructorCall it is good to write, say, "node to check = expr" for a first equation and, say, "node to check = actual" for the second one (this can be written in an inspector for an equation).

3) A comparison rule AlgebraicStructuralEquality seems to be unnecessary, since equality stated and checked with equations is already structural.

Moreover, comparison rules are meant to state comparability (such as is required by EqualsExpression or CastExpression of jetbrains.mps.baseLanguage), not equality, while the only kind of equations in your project is simple equation.

4) The "scripts" aspect is meant for creating refactorings and migration scripts, not for creating typesystem utility classes. Such classes should be written just inside the typesystem model.

Regards,

Cyril.

0
Comment actions Permalink

Thanks for your help. Hopefully, I'll manage from here :-)

0

Please sign in to leave a comment.