Hi Andrew,
> I have been looking into how we could define a typed lambda calculus
> system in CellML, and have written up a document to collect ideas on this:
> http://www.cellml.org/Members/miller/outline-of-a-typed-lambda-calculus-
> system
This is a good starting point, well done!
> Of particular interest is ideas about how this could be applied, and of
> anything that we could potentially be missing (for example, whether this
> is sufficient to support stochastic simulations with the addition of a
> few operators, or if it needs more fundamental changes to allow for
> that. This is something I am still looking into and would welcome ideas
on).
Regarding stochastic models and based on your current document, I am
wondering whether it wouldn't be worth having/gathering (snippets of) models
that would ideally be described in a typed CellML format?
I don't know anything about stochastic modelling, but if we were to have
such (snippets of) models, it might help us determining what is required to
get "a typed lambda calculus system [(TLCS)] could work in CellML".
Anyway, back to your document (please keep in mind that I haven't really
thought about TLCS):
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.
- "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?
- "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).
- "However, it would be invalid to connect two built-in variables to each
other." I guess I will understand that statement once I know exactly what a
"built-in variable" 'looks like'.
- 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... Why would all components have a built-in variable called
"real_metre"? What used would such a variable have? On the other hand, I
could see the need for such a type to be available everywhere. I have the
feeling that this might be a matter of terminology?
- Variables as types: "Variables holding a type have type "type", where type
is a built-in variable which itself has type "type"." Could this be
rephrased?!
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"? Otherwise, to illustrate the product of
real_metre and real_second, couldn't you say that you end up with something
like real_metre_second, or am I missing something?
- "Creating the type of a function in terms of the return type and the
argument types." Could you please give a concrete example of what you mean
by this?
- "Reversing the operations of the previous two operators". I first need to
understand those two operators to know whether I understand/agree with that
statement.
Dealing with real numbers:
--------------------------
- "The equivalence rules would enforce dimensional consistency, but
automatically apply conversion factors." Did you really mean that or "the
equivalence rules would *NOT* enforce dimensional consistency, but
automatically apply conversion factors", or even something else?
- "An operator which relates a real type A to two real types A and B such
that..." I suppose you meant "An operator which relates a real type *X* to
two real types A and B such that..."?
- You may, for the last three operators, want to swap A and X, so that it is
consistent with the first operator (e.g. for the second operator, it should
read "An operator which relates a real type X to a real type A and...").
- 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.
- "Identifier types are the exception, and can be used to provide semantics
like 'tag types' in other languages when this is required." This is lost on
me. Note: I see that "identifier types" are 'defined' in the next section.
Identifier types:
-----------------
- It would help if you could give some examples of identifier types.
- "Secondly, we *NEED* new context-sensitive MathML constructors for..."?
- I need to understand what is exactly meant by "Identifier types" before
being able to feed back on this section.
Functions:
----------
- I am not clear why the variable "fn_seconds_to_metre" is of type "type".
You mention something about type "type" in the last paragraph of the
"Variables as types" section. Is that related?
- I agree that functions that take one or more parameters is the best
approach.
- 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.
Structured types:
-----------------
- "However, for these types, it most likely would be reasonable that all
members are of the type would be of the same type, and so we should specify
the element type for all members." This is not clear to me. Are you saying
that for each member of, say, a vector, we should specify its type? I.e. we
could have a vector V[3] with V[0] = 123 {integer}, V[1] = true {boolean}
and V[2] = 456.789 {float}.
- You might want to give a concrete example of structured type.
- "Another useful type to have would be a structured type *WITH* differently
typed elements..."?
- "Extracting the sizes / dimensions of vector / matrix / set / list types."
Could you please give a concrete example of this?
Miscellaneous:
--------------
- As a general rule, I would very much welcome concrete examples and a not
so abstract/formal style of writing (unlike for the specifications). If find
the current version of your document to be unnecessarily difficult to read.
If you want feedback (and I want you to get some!), you would, in my
opinion, greatly benefit from writing in a much simpler style. Remember that
we are not all native English speakers and haven't all put loads of thoughts
in TLCS... This being all said: well done indeed!
Alan
_______________________________________________
cellml-discussion mailing list
cellml-discussion@cellml.org
http://www.cellml.org/mailman/listinfo/cellml-discussion
