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: alan.garny at dpag.ox.ac.uk (Alan Garny)
  • Subject: [cellml-discussion] A typed lambda calculus system for CellML
  • Date: Wed, 6 Aug 2008 19:31:37 +0100
> > 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.

> > - "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;
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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.

Just for information, how would you define the above in CellML using your
approach?

> > - "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.?

> > - 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.

> > 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.

> > - Paragraph starting "The specification would define that two types are
> > equivalent if...": though I do understand what you are saying, it might
> help
> > some people to give a concrete example.
> >
> See the next sentence in that paragraph, which gives an example.

True, but I meant a concrete example rather than a sentence.

> > - I need to understand what is exactly meant by "Identifier types"
> before
> > being able to feed back on this section.
> >
> The idea is a type, the values of which serve no purpose other than to
> be unique. Having uniqueness available to modellers allows constructs
> which attribute meaning to equality, such as set membership, to be given
> the correct semantics. For example, if different parts of the model
> indicate that fluxes belong to the set of all fluxes acting on a
> species' concentration, the desired interpretation is that each flux
> belongs to the set once per part of the model which adds the flux, not
> once per unique numerical value of the flux (if another part of the
> model sums over the values of the set to get the rate, and there are two
> separate reactions which generate numerically identical fluxes, both of
> these fluxes should be added to get the rate). In this case, it is
> useful to 'tag' the values being added to the set with an identifier, so
> that they are compared for the purposes of the uniqueness of set members
> based on the identifier and not the value.

I clearly have problems with the way you describe/define things. I need
concrete examples (the one that you give is not concrete enough for me,
sorry).

> > - You might want to provide some concrete examples of the advantages you
> > list. I am, for example, not clear what you mean by the third advantage
> that
> > you listed.
> >
> Yes, this is something that still needs to be done... ideally we should
> build some examples of complete models, including those using time
> delays and summary statistics, coded up according to the draft versions
> of CellML 1.2.

Yes, that is what I am after when asking for concrete examples.

Alan



Archive powered by MHonArc 2.6.18.

Top of page