Type Theory and Functional Programming

[Brian T Rice]

On 15 Mar 2003, Joerg F. Wittenberger wrote:

> Hi Brian,
>
> > While this is a reasonable suggestion, functional programming as you
> > describe it is not useful enough for Tunes. The current website doesn't
> > make this explicit enough,
>
> It would be _really_ useful, if the website could make the _reasons_
> explicit, why functional programming is not useful enough.

The simple fact that we need to express Active objects with side-effects
or lots of dynamic annotations within the language should be reason
enough. No monad or co-monad or dyad or whatever is ever going to be a
final answer to this.

> There is a nice article - I can't find the reference right now - which
> basically shows that the only difference between functional and
> non-functional programming is the fact that the former can proof their
> results, while the latter can't.  I do have the feeling that our
> mathematics is just the way it is, because over the thousends of
> years, we never found a better theory.  Hence I'm very sceptical, when
> there is a note like "not enough" towards math.  (I'm not saying you
> are wrong, I just say: please proof you statement.)

Well, if you define "functional programming" as "any language whose
programs you can prove" then your statement is trivially true, but that's
an entirely false concept. There are plenty of languages which are /not/
functional that have provable qualities, and even express side-effects. I
speak mainly about Maude, but there are other similar rewrite languages
which have this property.

-- 
Brian T. Rice
LOGOS Research and Development
mailto:water@tunes.org
http://tunes.org/~water/