[lrc]

I have been interested in doing this for a long time, and have thought about doing it in Haskell. It would be a lot of work, and some of the type decisions that would be needed would probably complicate the UX of the software (the automatic differentiation of functions of various shapes would make typing the D operator interesting; I think it would force all real-valued functions of a real variable to look like they were working in a vector space of dimension 1, or the inconsistency would be maddening). SICM's software also does a lot of "lowering" of types, so 0 (zero) is kind of a universal additive identity, but in a strongly typed system you'd need zeros of many different kinds and it might be that once all this was finished there was too much "wrapping" left visible and the scientific investigations in the SICM spirit would lose some of their charm. I guess that's a long-winded way of saying that there are lots of type puns in mathematical notation that are useful affordances even if they are slightly abusive.

[Myrmornis]

Thanks that was very interesting to hear your thoughts. If you do ever decide to work on this again, I'd be interested to know and probably in helping. Others in these threads have expressed interest too. But yes, it does sound like rather a lot of work for a slightly esoteric cause. My contact details are in my profile.