Re: Functions in programming

[Thorsten Altenkirch <txa@Cs.Nott.AC.UK>]

> There is one problem, of course: Haskell does not think this is
> legal as
> it thinks all datatypes should have at least one constructor.  (BTW do
> any functional languages allow NO constructors? They really should.)

Yes, Agda does.

> But now we have remembered that initial and final datatypes are
> supposed
> to coincide we have a blinding flash of inspiration:  because ()=1 is
> the final type it must also be the initial object.  So constant
> functions ARE the same as initial functions after all ....... so the
> student was not confused at all!
>
> Or was he?

I think it is a common misunderstanding that because you can write non-
terminating function that you should. Non-termination is a bug and it
is not what functional programming is about.

Btw, Agda is total, but you are allowed to ignore the termination
checker.

Thorsten

>
>
> -robin
>
>
> Robin Cockett, Calgary
>
>
>


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.