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

John Nowak <[email protected]> wrote:
>  William Tanksley, Jr wrote:
>  > John Nowak <[email protected]> wrote:
>  > 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.

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.

>  > 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.

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 result of the macro is always a stretch of
code, which also always has a type, although I expect it to not be
possible to manually sign that type in general (although there's a
proper subset of macros for which the type is manually signable).

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...

>  > 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.

Yes, but there's plenty of research on similar concepts.

>  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.

Yup. The crucial lesson is that typechecking can't specify
correctness, ever. Correctness is uncomputable, and neither types
alone nor tests alone nor contracts alone are sufficient to specify
it.

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

Well, if you CAN, go for it. I enjoy having the freedom to put off a
painful part of a project sometimes.

>  - John

-Wm