First login?
Lost password?
 
 
cellml-discussion AT lists.cellml.org 
CellML Discussion List

Text archives Help


[cellml-discussion] A typed lambda calculus system for CellML


Chronological Thread 
  • From: ak.miller at auckland.ac.nz (Andrew Miller)
  • Subject: [cellml-discussion] A typed lambda calculus system for CellML
  • Date: Thu, 07 Aug 2008 10:55:02 +1200
Alan Garny wrote:
>>> Variables as types:
>>> -------------------
>>> - Do we really want to allow generic types? I am concerned that this
>>>
>> could
>>
>>> lead to models that are not bullet-proof.
>>>
>>>
>> The core of CellML can be very generic, and then secondary
>> specifications can narrow down CellML to a subset of CellML which can be
>> implemented by a particular tool. Models would then be coded up in
>> accordance with a secondary specification.
>>
>> One secondary specification would likely only allow real numbers, and
>> other parts of the secondary specification might also allow the use of,
>> say, vectors of real numbers. But the core specification has to be more
>> general so that more secondary specifications can be defined.
>>
>
> Sorry, I am aware of all of that. I guess I didn't make myself clear. I was
> referring to "Components designed to be imported in another model may be
> coded using generic types (that is, using a type variable which could be
> connected to more than one different type) so that different final types can
> be connected up when the component is imported."
>
> My concern is related to "a type variable which could be connected to more
> than one different type". I would expect connections to involve the same
> type on both ends while I read your statement as meaning that this is not
> required.
>
The connection we are talking about has type "type" at both ends, and it
is the value of the variable (which is a type) which changes. However,
by connecting up variables of type 'type' holding different types, it
becomes possible to choose the type used at connection time. See below
for a discussion of how this is useful for building reusable components.

>
>>> - "In order to provide built-in types, there will need to be built-in
>>> variables." I think I understand the concept of "built-in types", but I
>>>
>> am
>>
>>> not sure what you mean by "built-in variables". Could you please provide
>>>
>> us
>>
>>> with some concrete examples of those?
>>>
>>>
>> Remember that the core statement of how the TLCS works is that "CellML
>> variables are defined inside components to hold types". In other words,
>> types are stored in variables. If we want to have built-in types, we
>> need to have variables to store them in, hence built-in variables. I
>> think that perhaps I need to emphasise the idea of variables holding
>> types more somehow.
>>
>> real_metre is an example of a built-in variable, which is given in the
>> same paragraph.
>>
>
> Ok, I now understand what you are saying. Still, I am not sure I agree with
> such an approach (but that might be because it's still not 100% clear to
> me!).
>
> Why not take a similar approach to that used in programming? In most
> programming languages, the declaration of a variable requires to specify its
> type, e.g. in C/C++:
>
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> int A;
> double V;
> bool T;
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>
> In our case, we would also need to know the units associated with those
> variables. So, again using a C/C++ syntax, we could have something like:
>
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> int_metre A;
> double_millivolt V;
> bool_dimensionless T;
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>
Note that I only intended that real numbers have dimensions. I'm not
sure that it makes sense to have dimensions on anything else.

That said, variables with type attributes on them are roughly the XML
equivalent of what you have proposed.

> int_metre, double_millivolt and bool_dimensionless would, in CellML, be
> defined in a similar way to how units are currently defined. In other words,
> definition of types would be an extension of the definition of units. From
> there, you could declare variables in a similar way to the one already used
> in CellML.
>
This would simultaneously be more complicated and less powerful than the
TLCS. We go to a great deal of effort to build such features as imports
and encapsulation and define how it works for components, and if we
store types in variables, we benefit from this immediately, allowing us
to make more reusable components. If we invent a completely different
system, then we have to devote a lot of specification space to defining
how, for example, types can be imported (along the lines of how units
work at the moment), we have to define a whole lot of extra elements,
and we have to invent a new structured system for defining types when we
could be just using MathML.
> Just for information, how would you define the above in CellML using your
> approach?
>
Something like...
<variable name="A" type="real_metre" /> <!-- Note that integers can't
have dimensions. -->
<variable name="V" type="real_millivolt" />
<variable name="T" type="boolean"/> <!-- boolean might need to be a
built in type -->
<variable name="real_millivolt" type="type" /> <!-- -This would probably
normally be connected up from a type library in real models -->
<m:math>
<m:apply><m:eq/>
<m:ci>real_millivolt</m:ci>
<m:apply><m:times/>
<m:cn units="dimensionless">0.001</m:cn>
<m:ci>real_volt</m:ci>
</m:apply>
</m:apply>
</m:math>
Whether or not we would actually use times for this I'm not sure.

>
>>> - "It would be valid to connect a built-in type using the name of one
>>> component to another variable". I must confess that this doesn't really
>>>
>> make
>>
>>> sense to me. I think it would help if you were to give some concrete
>>>
>> example
>>
>>> (the example you give in your document is still somewhat abstract).
>>>
>>>
>> I could add in something like:
>> Component A:
>> Variable name="T" type="type"
>> * Some more variables of type T *
>> Maths in terms of variables of type T
>>
>> Component B:
>> Empty
>>
>> Connection
>> Between Component A and Component B
>> Connect Component A.T to Component B.real_metre
>>
>> This would cause all the variables in Component A to be in terms of
>> real_metre. This is valid.
>>
>
> I find this unnecessarily confusing. What is wrong with having:
>
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> Component A:
> Variable name = "Var1" type="real_metre"
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>
> Rather than defining "T" as a variable of type "type", etc.?
>
That can be done too, if that is what the modeller wants. But in some
cases, it is useful to build generic components which can be used with
more than one type / unit. Examples:
* A component which does something which works on more than one size
of vector (where the vector size doesn't change dynamically with
simulation time, but may be different each time the component is imported).
* A component which can work with several different types of
concentration units, such as 'concentration' per unit area or
concentration in terms of volume, depending on whether it is being used
to model reactions on a membrane or in the lumen.
* Components which perform various types of scaling which don't depend
on type / units.
>
>>> - You mention "real_metre" as an example of a built-in variable. For
>>>
>> some
>>
>>> reason, I would have thought of "real_metre" as being an example of
>>>
>> built-in
>>
>>> type...
>>>
>> Because all types are stored in variables. So real_metre is a built-in
>> variable of type "type".
>>
>
> Ok, I am starting to understand better. I still think it's unnecessarily
> confusing though. A variable of type "type"!?
>
> I am sure I must be missing something, so I would very much appreciate if
> you could tell me what is wrong with the approach I suggested earlier. That
> will, hopefully, help me understand and appreciate your approach better.
>
I think simplicity is important, and using a TLCS gives us greater
simplicity in terms of elements needed in the specification, the number
of elements a modeller needs to learn about, and decreases the
difficulty of implementing the specification.

It also means we can use existing facilities for imports and
encapsulation, and allows for greater flexibility in what secondary
specifications can allow.

>
>>> MathML operators for dealing with types:
>>> ----------------------------------------
>>> - "Creating types which represent the product space of two (or more)
>>>
>> other
>>
>>> types. For example, given the types real_metre and real_second, creates
>>>
>> the
>>
>>> type for both a real_metre and real_second." Couldn't you refer to
>>>
>> "product"
>>
>>> rather than "product space"?
>>>
>> I mean product space in the sense that the set of acceptable values for
>> the type is the cartesian product of the sets of possible values of the
>> types the operator is applied to. So for example, a variable of the
>> product space type of real_metre x real_second could take the value (5m,
>> 10s).
>>
>
> Ok, though I am now wondering when such a product would be useful to have.
>
Any time you have two or more pieces of information that are so tightly
coupled they should be in one variable instead of two, or when you want
to put that information onto a list. Complex numbers, Cartesian
co-ordinates, and similar sorts of tightly coupled structured
information would be likely applications.

Best regards,
Andrew



Archive powered by MHonArc 2.6.18.

Top of page