[clean-list] Undefined value and theorem proving

[Maarten de Mol]

Hello Dmitry,


> Hi, All!
> 
> In an example given in "Theorem Proving for Functional Programmers - 
> SPARKLE: A Functional Theorem Prover" restriction is put that
> 
> take :: Int ![a] -> [a]
> 
>   does not get an undefined value as its first argument.
> 
> So I wonder how it is possible to call take with undefined value? And in 
> general, what operations in Clean can result with undefined expression?

The magic black box functions 'undef' and 'abort' from the module StdMisc
return the undefined value. For example, 'take undef [5]' will reduce
to 'undef', while 'take undef []' will reduce to '[]'.

There are other possibilities to produce the undefined value in Clean:
  * Calling a function with a pattern that does not match.
  * Using a case distinction in which no alternative matches.

Basically, anything that terminates your program with an error message
can be regarded as producing the undefined value.

Greetings,

Maarten de Mol

> 
> -- 
> Best regards, Dmitry Malenko.
> +----------------------------------------------------+
>   Registered Linux user #258004
>   ALT Linux Team                http://www.altlinux.ru
> +----------------------------------------------------+
> Do you guys know what you're doing, or are you just hacking?
> 
> 
> 
> _______________________________________________
> clean-list mailing list
> clean-list@cs.kun.nl
> http://www.cs.kun.nl/mailman/listinfo/clean-list
>