Re: [stack] possibilities for macros in a typed language

On Feb 22, 2008, at 9:41 AM, Christopher Diggins wrote:

>> Adding macros to Kitten seems fairly easy at first as the syntax is
>> easily representable as a list and there are no variables to get in
>> the way. Given that adding macros is fairly easy, it seems worth  
>> doing
>> if they'd be truly useful.
>>
>> But are they?
>
> Yes.

I suppose this was more rhetorical.

>> For an example, the m combinator 'dup i' cannot be assigned
>> a type
>
> Depends on your type system.

Of course. A system with rank-N polymorphism can handle 'dup i'  
properly. Unfortunately (perhaps?), we don't have such a system for a  
compositional/concatenative language yet.

> In Cat "dup apply" has the type "(A (A (B -> C) -> D) -> D)"

I'm not convinced this is useful. As a trivial example, it assigns  
'[swap] dup apply' the type 'A b -> A (C -> D) b'. Your system then  
rejects this type because (C -> D) is unknowable. Perhaps you have  
examples of where 'A (A (B -> C) -> D) -> D' can be composed to yield  
useful types?

Such a system also disallows the use of "unknowable" types for non- 
terminating functions like 'error'. My system gives 'error' the type  
'A -> B' which is quite useful as it allows one conditional branch to  
terminate a program without having to balance the error-causing branch  
with the successful branch for the sake of placating the type system.  
For example, 'true [dup] [error] if' is legal (and safe). If error did  
not have the type 'A -> B', something like 'true [dup] [error dup] if'  
would be needed instead. (Or alternatively, you could rewrite it as  
'true [] [error] if dup'.) Disallowing 'A -> B' also disallows unsafe  
coercion functions which may or may not be desirable.

I'm also not sure that 'A (A (B -> C) -> D) -> D' won't occasionally  
yield knowable types that are bogus, so some proof of its soundness  
would be desirable here.

>> for the same reason that '\x -> x x' cannot be assigned a type
>> in Haskell; it requires the construction of an infinite type. (Cat's
>> version of 'i' is called 'apply' I believe.)
>
> The problem with Haskell is the lack of inference for inner forall
> polymorphism.

Aye. Rank-N types are needed to handle this properly.

> That is true, but it would be a very minor hack to improve the MetaCat
> system to fix this. This is a very interesting idea!
> The lack of parameterized types in Cat is a huge thorn in its paw.
> Using macros we can side-step the issue by generating code.

Surely the correct solution is to offer parameterized types!

>> There are obviously downsides to macros as well. Firstly, you
>> sacrifice something in terms of concatenativity. For example, 'A B C
>> D' might not be decomposable into 'A B' and 'C D' if macros are
>> involved.
>
> Type-checking is usually done after macro expansion.

I was speaking here primarily from a pedagogical standpoint. With  
macros, you can no longer state that every space-delineated token is a  
function. The fact that you can do this without the presence of macros  
is a result of languages like Cat not needing any special forms. This  
is a very nice property that macros destroy, as macros are obviously a  
way of introducing special forms.

- John