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

On Apr 29, 2008, at 1:16 PM, William Tanksley, Jr wrote:

> John Nowak <[email protected]> wrote:
>> It seems there's a fundamental problem with typing concatenative
>> languages: Most type systems are not compositional which destroys the
>> simple algebra of concatenative programs.
>
> The literature includes some uses of the word "compositional" for type
> systems, but is there a specific meaning you have in mind here? I
> think you're talking about a type system which completely preserves
> the associative property of concatenative languages (the associative
> property guarantees both arbitrary factoring and arbitrary order of
> evaluation).

Correct. The expression '[a b] [c] compose' should always give the  
same type as '[a] [b c] compose'. Additionally, '[foo] i' should give  
the same type as 'foo'.

> That's a goal I share... Although it's also a goal I want to be able
> to work around. There are times when a type system should be able to
> force a specific order of evaluation, primarily when the system
> deduces the presence of side effects.

Fifth is a strict language in which evaluation is always left to  
right, so I don't think this would be an issue.

> Let me add one more thing before I go on: this problem is specific to
> type inference, not to type checking in general. If you always
> annotate inputs, outputs, and executions, there's no problem.

This is true. The problem comes in when dealing with macros. For  
example, a macro that translates lambda expressions to stack-based  
code needs to splice values into (possibly nested) quotations.  
Unfortunately, this translation might result in very confusing type  
errors, and there would be no way to give types to the generated  
quotations since the code is the result of a macro.

Ignoring macros for a moment, I have no issue with requiring  
annotations. I'm particularly partial to Daan Leijen's HML system (http://research.microsoft.com/users/daan/pubs.html 
). It gives more precise types than System F and offers full inference  
for impredicative instantiation. Type annotations are only required  
when a function parameter has a polymorphic type.

Maybe the solution is to just forget about macros, build in lambda  
expressions (which will give better error reporting), build in pattern  
matching, and just get on with it. Bah.

> Compare Spark Ada -- which, by the way, might be a useful role model
> for a very powerful type system that doesn't actually hurt code that
> it can't check (it's entirely optional, contained entirely within
> comments of perfectly standard Ada code).

Aye, Spark is great. It's unfortunate that it isn't free.

> Ability, dedication, and above all else _testing_. Darcs isn't buggy
> because its maintainer is unskilled; it's buggy (to the extent that it
> IS) because he can't consider all the possible cases, and there aren't
> enough people hammering on it (both in coders and in users) to find
> them reliably. (I know Darcs is getting a LOT better, by the way; it
> was my favorite, although I use Mercurial now.)

I love Darcs myself, and I continue to use it despite the issues. To  
be clear, in no way meant to say the people behind Darcs are  
unskilled. Rather, my point is that there are problems in the big- 
picture design of the program itself. Despite Haskell's rather fancy  
types, and the team's use of GADTs to enforce correctness, I still  
wouldn't trust it for anything involving more than a few people.  
Luckily, it does seem to be getting better. Darcs 2 is quite zippy,  
relatively speaking.

To be honest, I'm just experiencing some cognitive dissonance. My  
brain is trying frantically to rationalize avoiding the type system  
for awhile.

> Support for testing is important; it would be nice to have support for
> it baked into the compiler, and to have support not only for specific
> test cases, but also for universal claims (as in Design By Contract,
> Haskell's QuickCheck, and formal static annotation-augmented analysis
> like SPARK).

Fifth will offer contracts. This was a bit of a trick to get to  
working efficiently given that I wanted to be able to ensure removing  
contracts would have no effect on the program. In particular, it  
proved necessary for the programmer to state how many items on the  
stack a contract will need to access so that a portion of the stack  
can be (shallow) copied and restored before each assertion. The type  
system would ensure no more than the number of elements specified are  
accessible to the assertion. This would all be much easier in Joy  
where the stack is persistent, but this is out of the question for  
efficiency reasons.

Thanks for the input.

- John