Re: [stack] Re: Motivations to embrace undecidable type systems

On Apr 4, 2009, at 9:41 PM, hallucious wrote:

> If decidable type inference means that the type of quotations and  
> compositions of functions can be inferred and expressed, then I  
> think that type inference is decidable in this system. You are not  
> forced to simplify. (I should have pointed that out.)

It's easy to infer the constraints, but type inference (I believe)  
also entails checking that those constraints are satisfied and not in  
contradiction to one another. For example, you may have the following  
composition:

     A b -> A b      b Int
            C String d d   -> E

And you could assign it the following type:

     A b -> E where A < C and b = String and b < d and d = Int

This alone is not useful because the type inferred is not valid.

- John