On 26/08/08 12:28, Jonathan Cooper wrote: > Andrew Miller wrote: >> Hi all, >> >> 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 document does not yet aim to be a formal specification, but >> instead, aims to outline all the ideas that we could use as a basis >> for writing up the relevant parts of the formal specification. >> >> Please feel free to discuss this and / or suggest improvements. I >> have enabled commenting on the document in Plone for people with an >> account, and this mailing list would also be a suitable place for >> discussion of the document to take place. >> >> 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). > > Hi Andrew (& all), > > Overall I think this looks like a good approach, providing both > expressive power and elegance. The key difficulty will be in getting > the details right, both of semantics and XML encoding. This requires > concrete examples of how the concepts are envisaged to be used. > > It would be good to have references to related work > (e.g. http://www.w3.org/TR/mathml-types/) and some comparison of the > pros and cons of each approach for CellML. To quote the MathML note, > "it is a well-known fact that developing a mathematical typing system > is a difficult task," so it would be beneficial to reuse existing work > if possible. I'd also like to know about existing /implementations/ > using type systems with MathML - if we choose a sufficiently similar > system then this could help ease the implementation burden for > software authors. > > One area I'd particular like examples for is the use of identifier > types. It would be good to be able to define 'a set of fluxes,' for > example, in a straightforward fashion, but I'm not sure what would be > the best way to do so. It's an interesting semantic question! In a > sense you want to be able to distinguish between 'a set of real > numbers with units of flux' (where you don't allow multiple members > with the same number value), and 'a set of variables of type > real_flux' (where variable identity, not value identity, is > considered). You then need to consider if the mathematical expression > "<apply><eq/><ci>x</ci><ci>y</ci></apply>" makes x & y identical > variables, or whether only connections achieve this. Perhaps a > multiset better captures this use case anyway, and the question is > moot? > > > Some other thoughts on various aspects of the proposal follow. > > > I was initially uneasy about lumping type and units information > together, since these are distinct concepts. I can see benefits, for > example the ability to link up type & units with a single connection. > We will certainly need a way to extract just the type or just the > units, however, and make sure that, say, an abstract 'squaring' > component can be defined (it would define a function from type T to > T^2, where T^2 has the same /type/ as T, but the units, if any, are > raised to the power 2). > > > I don't think it fits with the intended use of MathML to add items in > the CellML namespace directly to MathML elements (for example your use > of <cellml:function_type />). This requires validators to alter the > MathML schema they use. An alternative approach would be to make use > of the facilities MathML already provides, such as csymbol and the > type attribute (using the latter on cn elements would allow use of > cellml:units to be deprecated). > > > One approach to defining functions of multiple arguments is given in > http://www.w3.org/TR/mathml-types/. > > > Do we need to define an explicit 'struct' equivalent? Could we not > use cartesian products (which are already in MathML)? This provides > us with arbitrary tuple types - the only difference from a C struct is > that you can't name members.
Another I forgot earlier: have you thought about semantics for "int/int"? Should this always yield an int (as in C), or always a real or rational, or an int if possible and rational otherwise, or should the user be able to define which semantics is wanted? Jonathan _______________________________________________ cellml-discussion mailing list cellml-discussion@cellml.org http://www.cellml.org/mailman/listinfo/cellml-discussion
