# Type validating Follow

Hi,

How I can validate substructure of types in the MPS. For example I have some primitive types such as integer, string etc. and I have some structured types such as sequence. In the case of primitive types it's clearly how to compare, but in the case of structured types clearly nothing:-(

**Someone can describe algo of the "InferenceRule" validating rule (":==:" statement) and how works "typeof" statements??? Anybody, please! **:-)

Regards,

Oleg

Please sign in to leave a comment.

Hi Oleg

It's not very clear what do you mean by "validating substructure" but I'll try to answer.

"typeof" statement returns evaluated so far type of a node. During typechecking it can be either a type variable, a concrete type with some type variables inside or a fully evaluated type.

equation :==: means that types on the left side and on the right side of an eqyation should match, (i.e. have the same set of properties with same values, same set of references with same targets and their respective children should also match).

Type evaluation and type checking via equations is performed using unification algorythm: if a variable should match some concrete type it becomes such a type.

for instance, if during typechecking type engine has the following equation (v being a type variable): v :==: Object, then v is definitely an Object; if List<v> :==: List<node<>>, then v is defenitely a node<>; etc.

Regards,

Cyril.

Hi, Cyril

Validating substructure means, that I have some constructed type and value, for example SequenceType and SequenceValue. SequenceType consists from several named types and SequenceValue must contains named values, that references to the corresponding named types and assign to them some values. In this case I must check some aspects of the value, such as presence and order of named values.

In what cases type considers as "concrete"?

rule IntegerValue {

applicable for concept = IntegerValue as value

overrides false

do {

typeof(value) :==: <INTEGER>

}

}

about typeof... in the case when typeof returns type of the variable, so in this case equation statement must always returns error, because IntegerValue (typeof(value)) isn't equals to the type IntegerType (<INTEGER>), but it isn't happens... why?

Regards,

Oleg

Hi Oleg,

you wrote:

rule IntegerValue {applicable for concept = IntegerValue as valueoverrides falsedo {typeof(value) :==: <INTEGER>}}about typeof... in the case when typeof returns type of the variable, so in this case equation statement must always returns error, because IntegerValue (typeof(value)) isn't equals to the type IntegerType (<INTEGER>), but it isn't happens... why?it hapens just as I have written:

Type evaluation and type checking via equations is performed using unification algorythm: if a variable should match some concrete type it becomes such a type.for instance, if during typechecking type engine has the following equation (v being a type variable): v :==: Object, then v is definitely an Object; if List<v> :==: List<node<>>, then v is defenitely a node<>; etc.Here in you example, if typeof(value) is a variable v, then v becomes equal to INTEGER when the equation v :==: INTEGER is solved

.Just consider a type variable as an "unknown" same as in simple linear equations known from school! There, if you have x == 3 and y == x + 2, you know that x is 3 and you may substitute 3 anywhere where x is written, therefore y becomes 3 + 2 that is 5 and the system is solved.

With type equations it is just the same. If you have, say, List<x> == List<String> and y == Set<x>, then type engine knows that x is String and therefore y is Set<String> and the system is solved.

Regards,

Cyril

Thanks, Cyril.

It's very intelligible answer ;-)

But what about "concrete" types? I saw "when concrete" statement, could you say how it works? In what cases type becomes as "concrete"?

Regards,

Oleg