Functional - Re: shootout: implementing an interpreter for a simple procedural language Minim

Author

Re: shootout: implementing an interpreter for a simple procedural language Minim

Raffael Cavallaro

2007-07-30, 4:14 am

On 2007-07-30 00:39:24 -0400, Paul Rubin <http://phr.cx@NOSPAM.invalid> said:

> But really, CL and
> even Scheme are 1970's languages, and things have been happening since
> then.

Yes, but imho they've been moving in precisely the wrong direction.
Modern statically typed languages found their birth at a time when
interactive computing as we know it today was not the norm. The
argument has been made [1, 2, 3] that the future of computing is no
longer of the model:

known range of inputs -> algoritmic processing -> known range of outputs

but rather:

partially known range of inputs -> combination of human interactive and
algorithmic processing -> unpredictable range of outputs

If this is the future of computing, then the focus on static typing is
a massive effort in solving the wrong problem.

1. http://www.cse.uconn.edu/~dqg/papers/cacm02.rtf

2. http://www.cse.uconn.edu/~dqg/papers/cie05.pdf

3. http://www.cse.uconn.edu/~dqg/inter_book.html

Steve Schafer

2007-07-30, 7:08 pm

On Mon, 30 Jul 2007 16:35:28 +0200, Rainer Joswig <joswig@lisp.de>
wrote:

>Say I have a library routine in some crypto package.
>This routine needs primes as input. How can I statically
>check the application that the routine is not
>used with non-primes?

I'm going to use "even" instead of "prime," just because it's easier to
show in a few lines. I'm using Haskell as the implementation language.

First declare a data type for even values:

> data Even = Even Int

(That is, a value of type Even has a single data constructor, also
called Even, that takes a single value of type Int.)

Now declare a function that extracts the numeric value out of an Even
and returns it as an Int:

> evenValue :: Even -> Int
> evenValue (Even x) = 2 * (x `div` 2)

That's it. Now, whenever we want to devise a function that accepts only
even numbers, we declare it to take arguments of type Even. In that
function's body, we use evenValue whenever we want to treat an Even as
an integer (to use in an arithmetic expression, for example).

(Note that the above code silently coerces non-even values passed to the
constructor to a "nearest" even value. We can handle that situation in a
variety of other application-specific ways, perhaps by raising an error.
The bottom line is that we can easily declare functions that are
_guaranteed_ by the type system to receive only even values as input.)

Declaring a data type for primes is conceptually the same, although
computationally quite a bit more involved (obviously).

Steve Schafer
Fenestra Technologies Corp.
http://www.fenestra.com/

Rainer Joswig

2007-07-30, 7:08 pm

In article <3bjpa3pb72b2lgroo3fcgg0m68t16l0s0o@4ax.com>,
Steve Schafer <steve@fenestra.com> wrote:

> On Mon, 30 Jul 2007 16:35:28 +0200, Rainer Joswig <joswig@lisp.de>
> wrote:
>
>
> I'm going to use "even" instead of "prime," just because it's easier to
> show in a few lines. I'm using Haskell as the implementation language.
>
> First declare a data type for even values:
>
>
> (That is, a value of type Even has a single data constructor, also
> called Even, that takes a single value of type Int.)
>
> Now declare a function that extracts the numeric value out of an Even
> and returns it as an Int:
>
>
> That's it. Now, whenever we want to devise a function that accepts only
> even numbers, we declare it to take arguments of type Even. In that
> function's body, we use evenValue whenever we want to treat an Even as
> an integer (to use in an arithmetic expression, for example).
>
> (Note that the above code silently coerces non-even values passed to the
> constructor to a "nearest" even value. We can handle that situation in a
> variety of other application-specific ways, perhaps by raising an error.
> The bottom line is that we can easily declare functions that are
> _guaranteed_ by the type system to receive only even values as input.)
>
> Declaring a data type for primes is conceptually the same, although
> computationally quite a bit more involved (obviously).
>
> Steve Schafer
> Fenestra Technologies Corp.
> http://www.fenestra.com/

Very good reply.

If I use a constant integer somewhere and I declare it to be
a prime, I better want to have it statically checked.

That's something I wanted to show, that computing with types
is possible in some places, still it may not be practical due to
possible large (or even larger ;-) ) run times.
Sometimes the type system's implementation may also
place restrictions.

Thanks again for the reply.

--
http://lispm.dyndns.org

Paul Rubin

2007-07-30, 7:08 pm

Steve Schafer <steve@fenestra.com> writes:
>
> That's it. Now, whenever we want to devise a function that accepts only
> even numbers, we declare it to take arguments of type Even. In that
> function's body, we use evenValue whenever we want to treat an Even as
> an integer (to use in an arithmetic expression, for example). ...
> The bottom line is that we can easily declare functions that are
> _guaranteed_ by the type system to receive only even values as input.)

But unless I'm missing something, this is only a runtime guarantee,
not a static check. For example, if I implement the version of Even
that signals an error if I give it an odd constructor arg, then write

-- double any even number, giving another even number
doubleEven :: Even -> Even
doubleEven x = Even (evenValue x + evenValue x)

then I can write

frob :: Even
frob = doubleEven 7 -- invalid!!!!

and not get a compile time error message. There may be a way to do it
with GADT's.

Paul Rubin

2007-07-30, 7:08 pm

Rainer Joswig <joswig@lisp.de> writes:
> If I use a constant integer somewhere and I declare it to be
> a prime, I better want to have it statically checked.
> That's something I wanted to show, that computing with types
> is possible in some places, still it may not be practical due to
> possible large (or even larger ;-) ) run times.
> Sometimes the type system's implementation may also
> place restrictions.

Right, one of the big advances in PL theory in the 1980's or 1990's
(?) was realizing there is a type corresponding to every
constructable mathematical set. I think that's why so much PL
research these days is devoted to type systems.

I borrowed a copy of Pierce's 700 page book (and that's just volume 1)
"Types and Programming Languages", about type systems, a few months
ago, but I couldn't understand much of it at that time. I've done
some other reading since then so I might look at Pierce's book again.
That book is supposedly the inspiration for Pugs, the Haskell
implementation of Perl 6.

Steve Schafer

2007-07-30, 10:05 pm

On Tue, 31 Jul 2007 09:57:40 +1000, Andrew Reilly
<andrew-newspost@areilly.bpc-users.org> wrote:

>On Mon, 30 Jul 2007 08:50:55 -0500, Matthias Blume wrote:
>
>
>Why wouldn't that runtime test turn into a compile-time test with
>sufficiently vigorous constant propagation?

It would, but then you're talking about a compiler that can determine
whether or not the integer value represented by the string
"170141183460469231731687303715884105727" is prime or composite.

In a reasonable amount of time, of course.

Steve Schafer
Fenestra Technologies Corp.
http://www.fenestra.com/

Jon Harrop

2007-07-31, 8:07 am

Rainer Joswig wrote:
> If I use a constant integer somewhere and I declare it to be
> a prime, I better want to have it statically checked.

You can do the same thing in OCaml and then write a macro to check
constants.

> That's something I wanted to show, that computing with types
> is possible in some places, still it may not be practical due to
> possible large (or even larger ;-) ) run times.

Static type systems rarely introduce run-time performance degradations.

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...entists/?usenet

Jon Harrop

2007-07-31, 8:07 am

Paul Rubin wrote:
> But unless I'm missing something, this is only a runtime guarantee,
> not a static check.

It is a mix. Once an Even is constructed (using a run-time type) it is
statically typed and type errors in its use are found statically.

This example has many problems though. Mainly, nobody does this for even
numbers. Also, most programs do some computation using the static type.

A compiler would be a better example. The question then becomes "but a
static type system doesn't check the user input?" to which the answer
is "yes, but it does check the compilation process".

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...entists/?usenet

Sponsored Links