John Nowak | 1 May 2008 04:14
Gravatar

Re: [stack] fundamental type system problems + possible solutions


On Apr 30, 2008, at 10:52 AM, William Tanksley, Jr wrote:

>> Fifth is a strict language in which evaluation is always left to
>> right, so I don't think this would be an issue.
>
> Are you saying that it's impossible to write an optimizing code
> generator for Fifth? :-)
> Seriously, though, I don't see why you should worry about 'effects
> inference' if you can't reorder anything. The only reason I know of to
> disallow effects is if evaluation order is flexible.

Ah, I misunderstood. I thought you were thinking that Fifth was lazy
and somehow needed the effect system to avoid stomping all over itself
when IO was involved. No, of course the effect system is useful for
optimization purposes. It's also useful for things like ensuring the
function passed to a parallel map function has no effects.

> Perhaps some more thought could be put into integrating the macro
> system and the type system. It seems to me that there are a few ways
> it could be done.
>
> Every parameter of the macro has a type; if inferring the type is too
> hard (and it probably is) you can require type signatures as part of
> the macro definition.

The problem is not typing the arguments to the macro; it's dealing
with the situation where the expansion of the macro is not inferable
and there's no way to provide annotations to quotations within the
expansion because the expansion is obviously not in the source code.
There are also issues with macros becoming much more tedious due to
the need to shuffle data in and out of some AST sum type in the macro
procedure itself. Ideally, you'd want implicit coersion to some 'any'
type as necessary to avoid the noise.

> Obviously, a typechecked macro system would exclude some obvious
> macros... But can we get things done with a subset of all possible
> macros? I think so...

Maybe. It's not just that though; if the facility becomes too much of
a pain to use for useful things, it might as well not be there at all.

Concatenative languages have a huge benefit in terms of macros because
there are no hygiene issues to worry about. Ignoring types, macros are
beyond trivial. Ideally, it would be nice to keep this property.

A soft type system makes this easy. Not being able to prove that the
macro evaluation itself will not have a type error is of little
concern to me provided that the expansion can be checked in the vast
majority of cases. A dynamic failure during a compile time expansion
isn't a big deal.

Right now, I'm leaning towards a soft intersection type system that
will be robust with respect to transformations and infer most any
reasonable program. Even if the type system never gets in your way,
there are benefits to soft types. For example, being able to run a
program to discover what's wrong with it when the type errors are
undecipherable is a very nice feature, especially for programmers new
to the language. I'll probably write up something about my approach
soon once I've filled in the details.

- John

__._,_.___
Yahoo! Finance

It's Now Personal

Guides, news,

advice & more.

Need traffic?

Drive customers

With search ads

on Yahoo!

Yahoo! Groups

w/ John McEnroe

Join the All-Bran

Day 10 Club.

.

__,_._,___
William Tanksley, Jr | 1 May 2008 17:30
Picon

Re: [stack] fundamental type system problems + possible solutions

John Nowak <john <at> johnnowak.com> wrote:
> William Tanksley, Jr wrote:
> > Perhaps some more thought could be put into integrating the macro
> > system and the type system. It seems to me that there are a few ways
> > it could be done.

> > Every parameter of the macro has a type; if inferring the type is too
> > hard (and it probably is) you can require type signatures as part of
> > the macro definition.

> The problem is not typing the arguments to the macro; it's dealing
> with the situation where the expansion of the macro is not inferable
> and there's no way to provide annotations to quotations within the
> expansion because the expansion is obviously not in the source code.

I can read this okay up until the phrase "obviously not in the source
code." Then I get completely lost. I'm going to reduce the argument to
a logical form as I understand it...

"It's impossible to X when condition Y holds."
X = "provide annotations to quotations within the expansion"
Y = "the expansion is obviously not in the source code"

I don't see how this could be _possibly_ true. Why should it ever be
impossible to annotate a quotation generated by a macro? Why is
"obviousness" part of the criteria for impossibility? How can code
generated by a macro not be part of the source code (unless you mean
not part of the original source code pre-generation, but again, I
don't see how it makes a difference whether the code was typed out by
hand or generated by a macro).

> There are also issues with macros becoming much more tedious due to
> the need to shuffle data in and out of some AST sum type in the macro
> procedure itself.

I think I see your point here... I don't know what AST means (abstract
syntax tree can't be right, can it?), but I can imagine a macro being
able to dynamically generate code AND also dynamically generate the
code's type signature. Yes, that would be both powerful and very
annoying.

> > Obviously, a typechecked macro system would exclude some obvious
> > macros... But can we get things done with a subset of all possible
> > macros? I think so...

> Maybe. It's not just that though; if the facility becomes too much of
> a pain to use for useful things, it might as well not be there at all.

That's what I mean -- break "macros" down into different classes and
subclasses, and only implement the classes that can currently be
reasonably accomplished, possibly using distinct syntax (or better,
distinct defining words) for each type.

The big problem with doing things this way is that someday you'll find
a sensible way to accomplish something new, and you'll have to add on
a new subclass of macros to express that. Your language will want to
change, but legacy will hold it back.

> Concatenative languages have a huge benefit in terms of macros because
> there are no hygiene issues to worry about. Ignoring types, macros are
> beyond trivial. Ideally, it would be nice to keep this property.

Agreed. This is a hard problem with types in general.

> A soft type system makes this easy.

Check out "hybrid typing",
http://www.cs.ucsc.edu/~cormac/papers/popl06-hybrid.pdf; I don't know
if it's any good, but it claims to be :-).

> Not being able to prove that the
> macro evaluation itself will not have a type error is of little
> concern to me provided that the expansion can be checked in the vast
> majority of cases. A dynamic failure during a compile time expansion
> isn't a big deal.

But a dynamic failure "during a compile time expansion" is actually a
static failure during the definition of the word using the macro, and
you've got all the same problems you wanted to solve as far as
printing out a readable error message that the person trying to use
the macro will be able to figure out.

> Right now, I'm leaning towards a soft intersection type system that
> will be robust with respect to transformations and infer most any
> reasonable program. Even if the type system never gets in your way,
> there are benefits to soft types. For example, being able to run a
> program to discover what's wrong with it when the type errors are
> undecipherable is a very nice feature, especially for programmers new
> to the language. I'll probably write up something about my approach
> soon once I've filled in the details.

I'm interested and curious. I think I get your point... Perhaps such a
type system could interact with the contract and test case
specifications to see what possibilities are ruled out or explicitly
required (respectively); and a type error could imply that you need to
correct one of your specifications or add a new specification, and
(even better) the error could hint what that specification would look
like.

> - John

-Wm

__._,_.___
Yahoo! Finance

It's Now Personal

Guides, news,

advice & more.

Ads on Yahoo!

Learn more now.

Reach customers

searching for you.

Cat Zone

on Yahoo! Groups

Join a Group

all about cats.

.

__,_._,___
John Nowak | 2 May 2008 03:35
Gravatar

Re: [stack] fundamental type system problems + possible solutions


On May 1, 2008, at 11:30 AM, William Tanksley, Jr wrote:

>> The problem is not typing the arguments to the macro; it's dealing
>> with the situation where the expansion of the macro is not inferable
>> and there's no way to provide annotations to quotations within the
>> expansion because the expansion is obviously not in the source code.
>
> I can read this okay up until the phrase "obviously not in the source
> code." ... (unless you mean
> not part of the original source code pre-generation, but again, I
> don't see how it makes a difference whether the code was typed out by
> hand or generated by a macro).

That is what I mean. Say you give a macro a quotation. That quotation
type checks. Now say the macro tears the quotation apart, and one of
the individual parts of the quotation doesn't check (which is very
possible). How would you annotate the fragment of the quotation that
failed to check?

> But a dynamic failure "during a compile time expansion" is actually a
> static failure during the definition of the word using the macro, and
> you've got all the same problems you wanted to solve as far as
> printing out a readable error message that the person trying to use
> the macro will be able to figure out.

Good point. Debugging macros is already little fun to begin with
though. My point was just that you won't be getting an error at runtime.

In any case, I have another approach for a type system I want to try
that more heavily depends on the algebraic properties of the language.
Initial results are encouraging, but I'll need another couple of
months to implement it as it's rather complex and I'm guessing my way
through it.

- John

__._,_.___
Yahoo! Finance

It's Now Personal

Guides, news,

advice & more.

Do-It-Yourselfers

Find Y! Groups

on Lawn & garden,

homes and autos.

Dog Zone

on Yahoo! Groups

Join a Group

all about dogs.

.

__,_._,___
William Tanksley, Jr | 4 May 2008 17:48
Picon

Re: [stack] fundamental type system problems + possible solutions

Before I start: http://citeseer.ist.psu.edu/dornan98typesecure.html
seems to possibly have something to do with this (maybe?). It's about
using dynamic types in a static system (which is nice for a soft type
system), and also about a static typechecked metaprogramming system.

John Nowak <john <at> johnnowak.com> wrote:
> That is what I mean. Say you give a macro a quotation. That quotation
> type checks. Now say the macro tears the quotation apart, and one of
> the individual parts of the quotation doesn't check (which is very
> possible). How would you annotate the fragment of the quotation that
> failed to check?

You're right -- I'm so used to reasoning about my experimental 01
language I'd forgotten that in the real world quotations can be torn
apart. I don't have a good answer to that. I was thinking of providing
tools that would cut quotations on boundaries of known types, but that
won't work if you're cutting the quotations on the results of string
searches (which is what a lambda-substitution macro has to do).

It would make sense to make quotations impossible to cut, but possible
to disassemble -- when you cut a quotation on a symbol, you get back
the quotation before the symbol, the quotation after the symbol, and a
program which when concatenated after those two correctly concatenates
them together. Simplest case:

[yadda x yadda] cut(x) ==
[yadda] [yadda] [concat]

All of the words that cut, concat, or insert quotations would, of
course, recompute and alter the quotations type signature.

I haven't figured out a heuristic to guess where a type error message
should direct the programmer's attention, though. Perhaps that's
something that should go in the annotations that metaprogrammers could
use... "If check fail in here, blame my macro code", versus "if checks
fail in here, trace it back to the user's annotations".

No, I don't see that one working. Oh well.

> In any case, I have another approach for a type system I want to try
> that more heavily depends on the algebraic properties of the language.
> Initial results are encouraging, but I'll need another couple of
> months to implement it as it's rather complex and I'm guessing my way
> through it.

Whew! Good luck.

> - John

-Wm

__._,_.___
Yahoo! Finance

It's Now Personal

Guides, news,

advice & more.

Need traffic?

Drive customers

With search ads

on Yahoo!

Find Balance

on Yahoo! Groups

manage nutrition,

activity & well-being.

.

__,_._,___
Manfred Von Thun | 13 May 2008 07:45
Picon
Picon
Favicon

[stack] QuoteAndEval

Still on the topic of quote and eval, it occurred to me that the Unix
command
languages (sh, csh, ksh, bash,..) have their own eval operator. It is the
backquote mechanism, which will evaluate what is enclosed inside the
backquotes `...` (I don¹t know what my mailer will do to it, it is the key
just under escape key at the top left). Example:

echo ³Today¹s date and the current time is `date`, have a nice day!²

Here the echo means print the following message which contains a short
backquoted command. The command returns a string that will be spliced
into the message. More complex commands can be backquoted:

echo ³In your home directory you have `ls ­la ~ | wc ­l ` files²

Here the ls command produces an output which is piped (with |)
to the wordcount facility wc to count just the lines.

The beauty of the various Unix utilities is that you can pipe the output
of one to become the input to the next. The backquote substitution
can make good use of it.

Is there a lesson to be learned for concatenative languages?
We have discussed Unix pipes briefly before, and their semantics
is clear: a pipe X | Y | Z computes the composition of the functions
X, Y and Z, just as any other concatenative language. But the
backquote is something else deserving a thorough examination.

- Manfred

[Non-text portions of this message have been removed]

__._,_.___
Yahoo! Finance

It's Now Personal

Guides, news,

advice & more.

Need traffic?

Drive customers

With search ads

on Yahoo!

Y! Groups blog

the best source

for the latest

scoop on Groups.

.

__,_._,___
rahul | 13 May 2008 19:52
Picon

Re: [stack] QuoteAndEval

....
> Is there a lesson to be learned for concatenative languages?
> We have discussed Unix pipes briefly before, and their semantics
> is clear: a pipe  X | Y | Z computes the composition of the functions
> X, Y and Z, just as any other concatenative language. But the
> backquote is something else deserving a thorough examination.

You may find this interesting

http://rosettacode.org/wiki/Category:UnixPipes

(Using unix pipes and files rather than the shell language).

>   - Manfred

Rahul

------------------------------------

Yahoo! Groups Links

<*> To visit your group on the web, go to:
    http://groups.yahoo.com/group/concatenative/

<*> Your email settings:
    Individual Email | Traditional

<*> To change settings online go to:
    http://groups.yahoo.com/group/concatenative/join
    (Yahoo! ID required)

<*> To change settings via email:
    mailto:concatenative-digest <at> yahoogroups.com 
    mailto:concatenative-fullfeatured <at> yahoogroups.com

<*> To unsubscribe from this group, send an email to:
    concatenative-unsubscribe <at> yahoogroups.com

<*> Your use of Yahoo! Groups is subject to:
    http://docs.yahoo.com/info/terms/

William Tanksley, Jr | 13 May 2008 22:19
Picon

Re: [stack] QuoteAndEval

Manfred Von Thun <m.vonthun <at> latrobe.edu.au> wrote:
> Still on the topic of quote and eval, it occurred to me that the Unix
> command
> languages (sh, csh, ksh, bash,..) have their own eval operator. It is the
> backquote mechanism, which will evaluate what is enclosed inside the
> backquotes `...` (I don¹t know what my mailer will do to it, it is the key
> just under escape key at the top left).

> Is there a lesson to be learned for concatenative languages?

I don't know what the lesson would be. Backquotes escape from a string
context to an executation/evaluation context. I suppose one could do
that in a concatenative language that had a string syntax.

More generally, I suppose one could "escape" from any context to an
evaluation, thus allowing you to compute a value at runtime which will
be compiled into the current quotation.

> - Manfred

-Wm

__._,_.___
Yahoo! Finance

It's Now Personal

Guides, news,

advice & more.

Ads on Yahoo!

Learn more now.

Reach customers

searching for you.

Y! Groups blog

the best source

for the latest

scoop on Groups.

.

__,_._,___
John Cowan | 13 May 2008 22:35

Re: [stack] QuoteAndEval

Manfred Von Thun scripsit:

> The beauty of the various Unix utilities is that you can pipe the output
> of one to become the input to the next. The backquote substitution
> can make good use of it.

Backquotes -- as is clearly shown by the alternative syntax $(...) --
essentially belong to the lexical level of the shell, just like $name
substitution. So they are very like Lisp macros: code inside backquotes
runs in a subshell to produce *source code* which is then evaluated by
the main shell in context, just as a Lisp macro runs in an subordinate
evaluator to generate Lisp code to be run by the main evaluator in
context.

--
What has four pairs of pants, lives John Cowan
in Philadelphia, and it never rains http://www.ccil.org/~cowan
but it pours? cowan <at> ccil.org
--Rufus T. Firefly

__._,_.___
Yahoo! Finance

It's Now Personal

Guides, news,

advice & more.

10 Day Club

on Yahoo! Groups

Share the benefits

of a high fiber diet.

Give Things.

Get Things.

It's free and it's

good for the planet.

.

__,_._,___
Christopher Diggins | 13 May 2008 22:43
Picon
Gravatar

Re: [stack] QuoteAndEval

So IIUC applying the idea to a concatenative language like Cat:

[is_weekend ["happy'] ["sad"] if] ` apply

Will generate different code depending on the day of week it is compiled.

Neat!

- Christopher

On Tue, May 13, 2008 at 4:35 PM, John Cowan <cowan <at> ccil.org> wrote:
>
>
>
>
> Manfred Von Thun scripsit:
>
>
> > The beauty of the various Unix utilities is that you can pipe the output
> > of one to become the input to the next. The backquote substitution
> > can make good use of it.
>
> Backquotes -- as is clearly shown by the alternative syntax $(...) --
> essentially belong to the lexical level of the shell, just like $name
> substitution. So they are very like Lisp macros: code inside backquotes
> runs in a subshell to produce *source code* which is then evaluated by
> the main shell in context, just as a Lisp macro runs in an subordinate
> evaluator to generate Lisp code to be run by the main evaluator in
> context.
>
> --
> What has four pairs of pants, lives John Cowan
> in Philadelphia, and it never rains http://www.ccil.org/~cowan
> but it pours? cowan <at> ccil.org
> --Rufus T. Firefly
>
>
>

__._,_.___
Yahoo! Finance

It's Now Personal

Guides, news,

advice & more.

All-Bran

10 Day Challenge

Join the club and

feel the benefits.

Yahoo! Groups

How-To Zone

Do-It-Yourselfers

Connect & share.

.

__,_._,___
Manfred Von Thun | 14 May 2008 07:49
Picon
Picon
Favicon

Re: [stack] QuoteAndEval



On 14/5/08 6:19 AM, "William Tanksley, Jr" <wtanksleyjr <at> gmail.com> wrote:
>
> Manfred Von Thun <m.vonthun <at> latrobe.edu.au <mailto:m.vonthun%40latrobe.edu.au>
> > wrote:
>
>> > Is there a lesson to be learned for concatenative languages?
>
> I don't know what the lesson would be. Backquotes escape from a string
> context to an executation/evaluation context. I suppose one could do
> that in a concatenative language that had a string syntax.
>
Maybe I should not have chosen those examples with the chatty strings inside
which
the backquote occurred. Here is an example that illustrates the Eval =
Unquote
principle: Eval(Quote(x)) = x:

echo `date` = date

For a concatenative language the lesson would be a facility to reach out
into the numerous Unix utilities which compute unary functions from
streams of bytes to streams of bytes. It would start with a string in the
concatenative language and end up with another string. All the Unix piping
would be done at the level of the concatenative language. The example
of counting the files in the home directory would look like one or the
other of these:

³la ~² ls ³-l² wc
³ls ­la ~² unix ³wc ­l² unix

This should leave a string of digits on top of the stack (or perhaps better,
an integer).

> More generally, I suppose one could "escape" from any context to an
> evaluation, thus allowing you to compute a value at runtime which will
> be compiled into the current quotation.
>
I definitely meant escaping to unix. Escaping to evaluate a quotation
is already in Joy: suppose there is a quotation on top of the stack. Then

stack swap infra first

or something similar will push the result of executing the quotation
onto the stack. Whether that result is to be spliced into another
quotation (what you called the current) is another matter again.

- Manfred

[Non-text portions of this message have been removed]

__._,_.___
Yahoo! Finance

It's Now Personal

Guides, news,

advice & more.

Curves on Yahoo!

Share & discuss

Curves, fitness

and weight loss.

Yahoo! Groups

w/ John McEnroe

Join the All-Bran

Day 10 Club.

.

__,_._,___

Gmane