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.