6 ms·

I want to question the importance of soundness in type systems. Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compil

I want to question the importance of soundness in type systems. Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compiler switch to see all the case statements where a class of a type is missing. The intended benefit of this system is that it accepts all correct programs. Correct meaning, the program runs and returns the correct answer. Would such a language be viable? Or is it absolutely necessary to catch all possible type errors. In the past, tools like lint have been considered useful, although lint is not at all the kind of type system that I envision, namely a system that is in practice catching all the errors that ML catches -- it just doesn't (and cannot) guarantee it catches them. The restrictive nature of static type systems today is legendary, but I wonder sometimes whether people realize how restrictive they are. If you can't make your idea work with functors or typeclasses, chances are good there's no way to get it to compile and you have to write functions in longhand.

shadowfox 12y ago
There is always idea of Gradual Typing [1] which has been implemented with varying degrees of success. There are also a large set of static analysis theories/tools which can help here. It is also worth noting that if you dont want (global) type inference, you can get far in a language with permissive casting, type annotations and local inference. The results aren't a panacea though. > Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compiler switch to see all the case statements where a class of a type is missing. I am not quite sure what you mean by this. Care to elaborate? (In general, with inference systems, missing type information is hard(ish) to localize. So pointing out where exactly a type error occurred is non-trivial) [1] https://en.wikipedia.org/wiki/Gradual_typing https://en.wikipedia.org/wiki/Gradual_typing
- tailrecursion 12y ago
  I'm thinking of a system with valueset inference where valuesets are not necessarily disjoint. So the system may infer that a return value is the disjunction {INTEGER | REAL}. In order to get precision in checking, a lot of computation needs to be done so the compiler relaxes the precision when facing large disjunctions (networks) of constraints. Dynamic checks are inserted as necessary but a system that relaxes when things get hairy can't guarantee that it will find all errors at compile time. The idea is similar to Soft Typing of Cartwright and others, but they were thinking of an interactive system, some kind of programmer's aid. If I recall they ran into problems giving reasonable error messages.
  - tomp 12y ago
    The problem with this idea, at least compared with current implementations of Haskell and OCaml, is that it requires runtime type information. Right now, Haskell and OCaml both perform erasure, and the only kind of runtime type information used is for the GC, but if you have two ADTs with identical structure (number of branches, payloads) but different names (i.e. they are different types), they will be encoded in the same way. So, in order to tell them apart, you would need some additional type information, which would require changes to compilers and would probably performance characteristics.
imanaccount247 12y ago
>I want to question the importance of soundness in type systems Why? The most common and popular opinion is already that it is not important. >Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compiler switch to see all the case statements where a class of a type is missing. The intended benefit of this system is that it accepts all correct programs. That doesn't make sense. That's like saying suppose we had a system of math that gave the right answer 99% of the time. How would doing the wrong thing 1% of the time give you the benefit of accepting all correct programs? >The restrictive nature of static type systems today is legendary Mythological. Legends are supposed to have some historical root. >If you can't make your idea work with functors or typeclasses, chances are good there's no way to get it to compile and you have to write functions in longhand. What does that even mean? That's like saying "if you can't make your idea work with classes or inheritance, chances are good that there's no way to get it to compile and you have to write functions in longhand".
- millstone 12y ago
  Suppose we insisted in math that all proofs be computer-checkable. There would be no erroneous proofs, but there would also be many correct proofs that could not be accepted or even formulated. Mathematics would suffer overall. Compiler enforced static typing rejects many correct programs, which is a disadvantage.
  - thoughtpolice 12y ago
    > Compiler enforced static typing rejects many correct programs, which is a disadvantage. Only if you care about these programs. It is entirely possible many of these 'correct programs' are not useful at all, or arguably useful, or are outside the domain criteria, and rejecting them is fine. This is often a leading motivator behind the design of things like domain specific languages, or designs like MISRA C - many things by design cannot be done, but often those aren't the things we care about, use, or wish to discuss anyway. On the flip side, there are things type systems enable that I do not think can be actually accomplished in an untyped language - but really, this isn't very interesting aside from being a minor technical factoid, IMO. It's very far removed from the more interesting question of whether or not it's useful to consider these things at all. And it's completely legitimate to say "No, these things aren't worth considering".
lmm 12y ago
> Would such a language be viable? Or is it absolutely necessary to catch all possible type errors. In the past, tools like lint have been considered useful, although lint is not at all the kind of type system that I envision, namely a system that is in practice catching all the errors that ML catches -- it just doesn't (and cannot) guarantee it catches them. It's entirely possible - I believe Dylan implements something on these lines. IMO it's harder to reason about than a consistent type system with "escape hatches" like unsafePerformIO, and about equivalent in usability. > The restrictive nature of static type systems today is legendary, but I wonder sometimes whether people realize how restrictive they are. If you can't make your idea work with functors or typeclasses, chances are good there's no way to get it to compile and you have to write functions in longhand. I have yet to find a piece of "good code" that I couldn't implement in a typesafe way. I've occasionally found code that worked but couldn't be made typesafe (e.g. the "big global Map<String, Object>" antipattern), but it's always been code that I would have wanted to rewrite for readability and sanity anyway.
tel 12y ago
This happens absolutely all the time. For instance, Haskell does it in almost exactly these terms. If you have a type like data Drums = Ba | Dum | Tish and you have a function that consumes drums play :: Drums -> String play Ba = "Ba!" play Dum = "Dum!" you've left out the Tish. Possibly because you don't have a cymbal. You know this, but the compiler doesn't. This is considered to be an incomplete pattern match and would raise some eyebrows. But often it just means there's an invariant which you know and the type system does not. In Haskell -Wall will stop you dead here, but you can relax it to say "ehhhh, I know what I'm doing". More generally, you can also write play :: Drums -> String play Ba = "Ba!" play Dum = "Dum!" play Tish = error "Impossible! I have no cymbal" This 'error' is a misleadingly named function. It's more like 'assert' and indicates that this is a completely impossible program state (much like running into an unbalanced tree deep inside a library function which knows that tree balance is maintained). It's outside of the reach of the programmer to fix. It's not an exception, it's an assurance to the compiler that even though there's something missing in the type safety things will be OK.

shadowfox 12y ago

There is always idea of Gradual Typing [1] which has been implemented with varying degrees of success. There are also a large set of static analysis theories/tools which can help here. It is also worth noting that if you dont want (global) type inference, you can get far in a language with permissive casting, type annotations and local inference. The results aren't a panacea though. > Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compiler switch to see all the case statements where a class of a type is missing. I am not quite sure what you mean by this. Care to elaborate? (In general, with inference systems, missing type information is hard(ish) to localize. So pointing out where exactly a type error occurred is non-trivial) [1] https://en.wikipedia.org/wiki/Gradual_typing https://en.wikipedia.org/wiki/Gradual_typing

tailrecursion 12y ago
I'm thinking of a system with valueset inference where valuesets are not necessarily disjoint. So the system may infer that a return value is the disjunction {INTEGER | REAL}. In order to get precision in checking, a lot of computation needs to be done so the compiler relaxes the precision when facing large disjunctions (networks) of constraints. Dynamic checks are inserted as necessary but a system that relaxes when things get hairy can't guarantee that it will find all errors at compile time. The idea is similar to Soft Typing of Cartwright and others, but they were thinking of an interactive system, some kind of programmer's aid. If I recall they ran into problems giving reasonable error messages.
- tomp 12y ago
  The problem with this idea, at least compared with current implementations of Haskell and OCaml, is that it requires runtime type information. Right now, Haskell and OCaml both perform erasure, and the only kind of runtime type information used is for the GC, but if you have two ADTs with identical structure (number of branches, payloads) but different names (i.e. they are different types), they will be encoded in the same way. So, in order to tell them apart, you would need some additional type information, which would require changes to compilers and would probably performance characteristics.

imanaccount247 12y ago

>I want to question the importance of soundness in type systems Why? The most common and popular opinion is already that it is not important. >Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compiler switch to see all the case statements where a class of a type is missing. The intended benefit of this system is that it accepts all correct programs. That doesn't make sense. That's like saying suppose we had a system of math that gave the right answer 99% of the time. How would doing the wrong thing 1% of the time give you the benefit of accepting all correct programs? >The restrictive nature of static type systems today is legendary Mythological. Legends are supposed to have some historical root. >If you can't make your idea work with functors or typeclasses, chances are good there's no way to get it to compile and you have to write functions in longhand. What does that even mean? That's like saying "if you can't make your idea work with classes or inheritance, chances are good that there's no way to get it to compile and you have to write functions in longhand".

millstone 12y ago
Suppose we insisted in math that all proofs be computer-checkable. There would be no erroneous proofs, but there would also be many correct proofs that could not be accepted or even formulated. Mathematics would suffer overall. Compiler enforced static typing rejects many correct programs, which is a disadvantage.
- thoughtpolice 12y ago
  > Compiler enforced static typing rejects many correct programs, which is a disadvantage. Only if you care about these programs. It is entirely possible many of these 'correct programs' are not useful at all, or arguably useful, or are outside the domain criteria, and rejecting them is fine. This is often a leading motivator behind the design of things like domain specific languages, or designs like MISRA C - many things by design cannot be done, but often those aren't the things we care about, use, or wish to discuss anyway. On the flip side, there are things type systems enable that I do not think can be actually accomplished in an untyped language - but really, this isn't very interesting aside from being a minor technical factoid, IMO. It's very far removed from the more interesting question of whether or not it's useful to consider these things at all. And it's completely legitimate to say "No, these things aren't worth considering".

lmm 12y ago

> Would such a language be viable? Or is it absolutely necessary to catch all possible type errors. In the past, tools like lint have been considered useful, although lint is not at all the kind of type system that I envision, namely a system that is in practice catching all the errors that ML catches -- it just doesn't (and cannot) guarantee it catches them. It's entirely possible - I believe Dylan implements something on these lines. IMO it's harder to reason about than a consistent type system with "escape hatches" like unsafePerformIO, and about equivalent in usability. > The restrictive nature of static type systems today is legendary, but I wonder sometimes whether people realize how restrictive they are. If you can't make your idea work with functors or typeclasses, chances are good there's no way to get it to compile and you have to write functions in longhand. I have yet to find a piece of "good code" that I couldn't implement in a typesafe way. I've occasionally found code that worked but couldn't be made typesafe (e.g. the "big global Map<String, Object>" antipattern), but it's always been code that I would have wanted to rewrite for readability and sanity anyway.

tel 12y ago

This happens absolutely all the time. For instance, Haskell does it in almost exactly these terms. If you have a type like data Drums = Ba | Dum | Tish and you have a function that consumes drums play :: Drums -> String play Ba = "Ba!" play Dum = "Dum!" you've left out the Tish. Possibly because you don't have a cymbal. You know this, but the compiler doesn't. This is considered to be an incomplete pattern match and would raise some eyebrows. But often it just means there's an invariant which you know and the type system does not. In Haskell -Wall will stop you dead here, but you can relax it to say "ehhhh, I know what I'm doing". More generally, you can also write play :: Drums -> String play Ba = "Ba!" play Dum = "Dum!" play Tish = error "Impossible! I have no cymbal" This 'error' is a misleadingly named function. It's more like 'assert' and indicates that this is a completely impossible program state (much like running into an unbalanced tree deep inside a library function which knows that tree balance is maintained). It's outside of the reach of the programmer to fix. It's not an exception, it's an assurance to the compiler that even though there's something missing in the type safety things will be OK.