What do you gents think or shen, doc mark tarver and importance of types?

[gavino]

http://www.lambdassociates.org/Shen/newappeal.htm

[Nicolas Neuss]

gavino <gavc...@gmail.com> writes:

> http://www.lambdassociates.org/Shen/newappeal.htm

Nice stuff. I wish I had time to learn and use it.

Nicolas

[jvt]

I like static type systems and destructuring. Go look at a piece of
dynamically typed code: a tremendous amount of code is dedicated to 1)
checking the type of input arguments, 2) dispatching on the type of
input arguments (mitigated somewhat by things like CLOS), and 3)
destructuring the data held inside union or structural types so that
the data can be acted upon. It is all line noise which can be removed
by a good, expressive type system. Throw in the fact that the type
system saves you at compile time rather than failing (sometimes
bizarrely) at run time and get yourself a good type inference engine
on top of it all, and you write less, better code. A sufficiently
expressive type system hardly constrains your programming style too.
And the compiler can use type information to generate better machine
code.

Given this state of affairs, I'm surprised that there is any argument
about static types at all. I'm also surprised there isn't a practical
Lisp with a good static type system, and I'm somewhat unsure about
Shen's ability to turn type checking off. That said, I wonder about
the wisdom of having a turing complete type system. There may be
something to be said for having a type system which is "just
expressive enough."

In my mind the biggest benefit of dynamic types is that they
facilitate interactive development to a much greater extent than a
static system. I'll admit, this is a pretty compelling argument.
That and the fact that people design big projects in runtime-typed
languages all the the time, which proves only that a good type system
is an incremental change rather than a revolutionary one, and so the
whole discussion doesn't bear too much acrimony.

[gavino]

I read Paul Graham as saying dynamic typing problems easy to handle and he details this in on lisp book.

[Kaz Kylheku]

On 2011-11-03, jvt <vincen...@gmail.com> wrote:
> I like static type systems and destructuring. Go look at a piece of
> dynamically typed code: a tremendous amount of code is dedicated to 1)
> checking the type of input arguments,

A lot of dynamic code is completely generic, unconcerned with
the types of its arguments.

Bet you that code which does a lot of checking would be greatly
condensed with the use of a decent pattern-matching library.

Also, how much type checking there is depends on how close you are to some
untrusted boundary.

Are you an API function for wide use? Or an internal helper?

A lot of the type checking is not really necessary; it just helps
to identify a misuse earlier in the pipeline.

What is more helpful:

foo-macro: list of widgets expected, not ABC.

endp: a proper list must not end with ABC.

Once the inputs are validated at the boundary, the guts of a module
can dispense with the checks. If something sneaks through, it will
result in a low-level type error message.

A lot of type checking in dynamic systems is actually input validation. No
program can avoid input validation in any language. But in a dynamic system,
the expressivity is rich, allowing types to be inputs.

Types can contribute to the representation of external data arriving into the
program!

In Lisp we can read some data from a database, network, file or GUI,
and it has type. Now you have type checks that don't easily go away
with a static type system.

Your observation that dynamic typing facilitates interactive
programming is just a consequence of this. When we are programming,
we are giving input to the system. That input is richly typed, but
it's coming into the system during that system's run time!

There is no dynamic data without dynamic type.

> 2) dispatching on the type of
> input arguments (mitigated somewhat by things like CLOS), and 3)
> destructuring the data held inside union or structural types so that
> the data can be acted upon. It is all line noise which can be removed
> by a good, expressive type system.

Static typing is great as long as I'm still the boss.

Type system: "Sorry, you cannot run this code because it has a confirmed type
error."

Me: "Thanks, the error is duly noted! Now can you step aside and let me run it?
I am busy working on some other aspect of this, and I won't step on that case
in the kind of testing I'm doing. If I do, the run-time check will be there, so
I'm okay."

Type system: "Sorry, you cannot run this code because I couldn't prove it
to be free of type errors."

Me: "Seriously, what? That's your problem, now, really, get out of my way!"

[Marco Antoniotti]

On Tuesday, November 8, 2011 7:04:40 AM UTC+1, Kaz Kylheku wrote:
> On 2011-11-03, jvt <vincen...@gmail.com> wrote:
> > I like static type systems and destructuring. Go look at a piece of
> > dynamically typed code: a tremendous amount of code is dedicated to 1)
> > checking the type of input arguments,
>
> A lot of dynamic code is completely generic, unconcerned with
> the types of its arguments.
>
> Bet you that code which does a lot of checking would be greatly
> condensed with the use of a decent pattern-matching library.
>

Like CL-UNIFICATION? (Sorry, I couldn't resist :) )

...

> > 2) dispatching on the type of
> > input arguments (mitigated somewhat by things like CLOS), and 3)
> > destructuring the data held inside union or structural types so that
> > the data can be acted upon. It is all line noise which can be removed
> > by a good, expressive type system.
>
> Static typing is great as long as I'm still the boss.
>
> Type system: "Sorry, you cannot run this code because it has a confirmed type
> error."
>
> Me: "Thanks, the error is duly noted! Now can you step aside and let me run it?
> I am busy working on some other aspect of this, and I won't step on that case
> in the kind of testing I'm doing. If I do, the run-time check will be there, so
> I'm okay."
>
> Type system: "Sorry, you cannot run this code because I couldn't prove it
> to be free of type errors."
>
> Me: "Seriously, what? That's your problem, now, really, get out of my way!"

I wholeheartedly agree. My argument *for* not-so-static type systems is that yes: with a static-bb-type-system you eventually get to a correct and good program in pretty much the same time you get to a correct and good program using a not-so-static type system. The difference is where and when you put your time into. In the first case you spend a lot (*a lot*) of time satisfying the TS. In the second case you "explore" more: maybe down wasteful alleys, but it is worth the while of many programmers. Of course this argument cannot be "proven", but my gut feeling is that it is valid. If it weren't we would not have SLDJs.

Cheers
--
MA

[Mark Tarver]

Re the OP I'm not going to venture any opinion about myself ;); but
there's some interesting points in the thread.

> I'm somewhat unsure about Shen's ability to turn type checking off.

Yes; people who are devoted to static typing don't like this.
But ....

...what often happens when a programmer tries working in a statically
typed language is this: he finds that he can type check (in principle)
about 95% of all his code. What remains is a recalcitrant 5% that is
very difficult to check (e.g something involving 'eval' or FFI for
instance). After struggling and getting bogged down, he then throws
his hand in and then does *all* the work in an untyped Blub whereby
all type security is lost. After that he migrates to a comp.lang.blub
and tells everybody that statically typed languages like ML/Haskell
etc. are a PITA.

Getting fundamentalist about type checking works only if the
programmer is not free to explore other languages. Fundamentalism
polarises independent minds where everything good that the
fundamentalist is trying to sell is soundly rejected. Many old
arguments about static vs. untyped languages have a religious quality.

It is more sensible to allow the programmer an environment in which he
can type check 95% of his code and smuggle in the 5%, than to insist
on 100% fidelity and lose not only the 5% but the 95% that could have
been checked and alienate the programmer from ever checking his code.
So Shen allows you to do that. In other words .....

> static typing is great as long as I'm still the boss.

Yes; quite, exactly my point. But the resources of Shen are greater
than ML/Haskell (see http://www.lambdassociates.org/studies/study02.htm
for an example). Here is an example of the kind Kaz is talking about
where normally you might bomb out from static type checking in some
languages. Suppose he writes a Shen program that downloads a file as
a list of units (where a unit is just some unspecified object) and he
wants to return the numbers in the list. He writes

(define find-numbers-in-file
{string --> (list number)}
Filename -> (find-ns (read-file Filename)))

(define find-ns
{(list A) --> (list number)}
[] -> []
[X | Y] -> [X | (find-ns Y)] where (number? X)
[_ | Y] -> (find-ns Y))

where (say) read-file : string --> (list unit). The dialogue goes
like this.

Shen type system: "Sorry, you cannot run this code because it has a
confirmed type error in rule 2 of find-ns."

Kaz: "Thanks, the error is duly noted! Now can you step aside and let
me run it? The run-time check will be there because I'm testing for
numberhood in the guard, so I'm okay. Look you can assume this

(datatype numbers

\* assume that if N has been verified to be a number, then it is a
number *\

_____________________________________
(number? N) : verified >> N : number;)

Runs it again.

Shen type system: "On this assumption your code is type secure."

Regarding the Shen project; work on the kernel is now running in San
Francisco (porting to Javascript), Moscow (to Scheme) and here (in
Leeds UK where the maths library is being built). If you want to
correspond on it then register with qilang. I exist and correspond
largely on that group. You'll be very welcome.

Mark