Re: 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