On Tue, 28 Sep 1999, Paul Hudak wrote:
> I'm not sure what you mean by "sane" vs "consistent".

Sanity means, in this context that boolean functions comply with
boolean logic when passed boolean values.
Boolean logic does not specify a behavior for functions with non-boolean
domains (like _|_).  However, as you note, from a developer perspective,
all Haskell implementations should agree on a _consistent_ behavior for
Haskell functions.
(I am making a really simple and mundane point.  I am surprised that people
are disputing it.  George Bool did not have a concept of _|_ when he
documented Boolean logic!)

> > PS Charity claims to eliminate _|_.  I don't know enough about
> > category theory and programming language design to know the 
> > costs of doing so.
> 
> I have no idea what Charity is, but if this is indeed the case then, at
> least for Booleans, all expressions must be strongly normalizing, i.e.
> will always terminate with value True or False.  Usually languages such
> as these sacrifice expressivity (for example, no general recursion!),
> such as languages based on constructive type theory.  (Either that or
> they have solved the halting problem :-)

Yes.  Charity is categorical programming language.  From  
http://ftp.cpsc.ucalgary.ca/projects/charity/home.html:

 Charity is based on the theory of strong categorical datatypes. These are
 divided into two subclasses: the inductive datatypes
 (built up by constructors in the familiar way) and the coinductive
 datatypes (broken down by destructors). Programs over
 these datatypes are expressed by folds (catamorphisms) and by unfolds
 (anamorphisms), respectively. 

They claim that you don't really need general recursion.  As I said
before, I don't know enough to evaluate this claim.

-Alex-

___________________________________________________________________
S. Alexander Jacobson                   Shop.Com
1-212-697-0184 voice                    The Easiest Way To Shop








Reply via email to