# fundamental type system problems + possible solutions

## John Nowak — 2008-04-29 07:20:17

    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. Take these equivalencies for

    example:

        [$A] i       ==  $A       -- application

        [$A] [$B] o  ==  [$A $B]  -- composition

        $a [$B] pa   ==  [$a $B]  -- partial application

        [$A] m       ==  [$A] $A  -- self-application

    Unfortunately, all of these rules (except perhaps for partial

    application) fall apart once types are involved. This is of practical

    concern as it makes cut-and-paste refactoring impossible and will

    cause problems with many macro transformations.

    What is needed is a type system that is compositional. One system that

    meets this requirement is System E developed by Carlier and Wells [1].

    While this seems like an appealing solution at first, the types

    produced by System E are so complex that they're not really human-

    decipherable. Even if a solution to making error reports

    understandable could be found via some form of type error slicing [2],

    there would still be no way to make types useful as documentation.

    As I see it, there are three main benefits of static type systems:

    Automatic and correct documentation, increased safety, and increased

    efficiency. Of these three, I consider documentation to be the most

    important. After all, there are language implementations without

    static type systems that perform quite well such as SBCL and LuaJIT.

    As for safety, dynamic languages are used to build highly-reliable

    systems (see Erlang); ultimately, the design of a program and ability

    of the implementors contributes much more to software reliability than

    the presence of a type system (compare Haskell/Darcs to C/Perl/Git).

    The need for documentation, however, you can't escape. This is

    especially so in stack-based languages where stack effect comments are

    necessary to make sense out of things. While no type system will

    replace the need for such comments entirely, as it is often necessary

    to state not just the type of a value but its purpose, a type system

    can at least ensure the correct number of arguments will always be

    passed and that type constraints will be respected.

    I would rather have no type system than one which makes simple

    transformations, and hence macros and much refactoring, impossible.

    Static type systems seem doomed to being either non-compositional or

    not suited to producing human-readable documentation.  Therefore, as I

    see it, there are two possibilities going forward.

    One is to develop a soft type system that hopefully will be able to

    report most errors without rejecting any program. If a language is

    designed with a soft type system in mind, the quality of error

    reporting can be quite good. For example, dynamic checks can be

    inserted to ensure lists are used homogeneously and type declarations

    can be required for data types to avoid the need for equi-recursive

    types.

    The other approach would be some way of inferring the equivalences

    mentioned at the beginning of this email. I guess this would take the

    form of some kind of abstract interpretation. The goal here would not

    be to catch all type errors (although some would be catchable), but

    rather to provide a detailed description of what a function does

    beyond what an HM-based type system would be capable of yielding. It

    seems the primary issue here would be giving equivalencies for

    functions involving recursive data types. For example, if we define

    some 'each' function that simply places an element from a list on the

    stack and then calls some function repeatedly until the list is empty,

    how would we express this?

    Anyway, these are just my current thoughts. As for Fifth, I've decided

    to delay inclusion of the type system until I can find a solution that

    won't cause problems with macros or inhibit cut-and-paste refactoring.

    (I'll credit Slava Pestov for reminding me of how critical this is.)

    Any thoughts would be appreciated, especially regarding the second

    approach described above.

    - John

    [1] http://www.church-project.org/modular/compositional/system-E/

    [2] http://www.macs.hw.ac.uk/ultra/compositional-analysis/type-error-slicing/slicing.cgi

## William Tanksley, Jr — 2008-04-29 17:16:22

    John Nowak <john@...> 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).

    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.

    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.

    I need to read up on this; thank you for the references.

     >  As I see it, there are three main benefits of static type systems:

    >  Automatic and correct documentation, increased safety, and increased

    >  efficiency.

     I suppose the availability of statically known information to the

    programmer counts as "documentation", but sometimes it's more than

    that. Consider Ada's type attributes, as in TYPENAME'MAX or

    TYPENAME'SIZE. In theory, we could do much better.

    I would consider a static type system to be a huge "win" if it helped

    programmers. I'm not against static type systems for their own sake,

    but I'm strongly for them when they help.

    The effect system you proposed would have some interesting ways of helping.

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

    http://en.wikipedia.org/wiki/SPARK_programming_language is perhaps a

    good place to start. (I know there are more formal systems out there,

    but this one's especially interesting because it's purely optional.)

     >  Of these three, I consider documentation to be the most

    >  important. After all, there are language implementations without

    >  static type systems that perform quite well such as SBCL and LuaJIT.

     A good point; JITs tend to have a lot of useful information available

    to them. On the other hand, it's easy to design a language that is

    very hard to JIT.

     >  ultimately, the design of a program and ability

    >  of the implementors contributes much more to software reliability than

    >  the presence of a type system (compare Haskell/Darcs to C/Perl/Git).

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

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

     >  I would rather have no type system than one which makes simple

    >  transformations, and hence macros and much refactoring, impossible.

    >  Static type systems seem doomed to being either non-compositional or

    >  not suited to producing human-readable documentation.  Therefore, as I

    >  see it, there are two possibilities going forward.

     Requiring limited annotation could be useful, and has some nice

    effects in terms of safety as well -- it's easy to write a function

    for which the compiler infers a correct type that is not similar to

    the type you'd desired (thus deferring the error message until later,

    when it's probably less useful).

     >  The other approach would be some way of inferring the equivalences

    >  mentioned at the beginning of this email. I guess this would take the

    >  form of some kind of abstract interpretation. The goal here would not

    >  be to catch all type errors (although some would be catchable), but

    >  rather to provide a detailed description of what a function does

    >  beyond what an HM-based type system would be capable of yielding. It

    >  seems the primary issue here would be giving equivalencies for

    >  functions involving recursive data types. For example, if we define

    >  some 'each' function that simply places an element from a list on the

    >  stack and then calls some function repeatedly until the list is empty,

    >  how would we express this?

     The uncomputable sky is the limit -- we need a type theory in order to

    decide anything here.

     >  - John

     -Wm

## John Nowak — 2008-04-30 04:52:39

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

     > John Nowak <john@...> 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

## William Tanksley, Jr — 2008-04-30 14:52:54

    John Nowak <john@...> wrote:

     >  William Tanksley, Jr wrote:

    >  > John Nowak <john@...> 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

## John Nowak — 2008-05-01 02:14:57

    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

## William Tanksley, Jr — 2008-05-01 15:30:33

    John Nowak <john@...> 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

## John Nowak — 2008-05-02 01:35:43

    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

## William Tanksley, Jr — 2008-05-04 15:48:23

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