Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Babel-17


view this post on Zulip Email Gateway (Aug 18 2022 at 13:36):

From: Jens Doll <jd@cococo.de>
The paper about Babel is written esthetically and inspiring, but lacks
deeper insight:

a) a functional language should not make use of ancient constructs like
"while" and "for", use iterators instead
b) the example on The GCD might be incomplete, pls. have a look

Thanks for the input,
Jens

view this post on Zulip Email Gateway (Aug 18 2022 at 13:36):

From: Steven Obua <obua@wjpserver.cs.uni-sb.de>
On Jun 17, 2009, at 7:29 AM, Jens Doll wrote:

The paper about Babel is written esthetically and inspiring, but lacks
deeper insight:

a) a functional language should not make use of ancient constructs
like
"while" and "for", use iterators instead

Actually for-do uses iterators. I don't see why the programmer should
be burdened with adhering to the iterator protocol, the language can
do that for you. I am just lazy, probably an ancient habit.

b) the example on The GCD might be incomplete, pls. have a look

It is complete. But it just defines a function gcd, so when you run
it, you will need to provide an expression that uses this function. Try:

fun gcd (a, b) =
while b != 0 do
b = a % b,
a = b
end;
a;

gcd (120, 35)

Steven


Last updated: May 03 2024 at 08:18 UTC