7 ms·

It would be nice to have some examples of what these terms mean, for type system dilletantes like me. I must say, I was a little lost :) Re: TypeScript: > Typ

It would be nice to have some examples of what these terms mean, for type system dilletantes like me. I must say, I was a little lost :) Re: TypeScript: > TypeScript challenges the status quo, claiming that lowering the cognitive overhead of using types is more important than type soundness. They argue that JavaScript programmers, their main audience, would find it easier to use TypeScript if they deviated from traditional norms. Im not sure about the official mission statement, but as far as I understand, the purpose of their typesystem is to allow static description of the way existing JavaScript is typed, de facto, in the wild. This explains why e.g. literal strings are a type so you can do: interface Eventor { on('foo', FooHandler); on('bar', BarHandler); } Not because it’s nice to have a type that "foo" satisfies and not "bar", but because there is actual code out there that does this, today. Same for structural typing (TypeScript would be absolute horror to interface with existing code without it). And, I assume, covariant arrays. TypeScript was not created in a void, as a fresh, new typesystem. It was created to formalise the way existing JavaScript was informally typed. It would have been nice to see a little reference to or acknowledgement of this. Or an example of how this could have been achieved better; preserving type soundness.

Tarean 9y ago
There are basically two important results for type systems, soundndess and completeness. Soundness means that every program that typechecks is valid. Completeness means that every valid program can be typed. So basically typescripts type system doesn't match the language semantics so type checked programs may crash at runtime.
- s_kilk 9y ago
  I'm curious, given Godels incompleteness theory, isn't it impossible to have both soundness and completeness in the same language?
  - karatinversion 9y ago
    Gödel's incompleteness is for proof systems for languages which contain enough arithmetic to express its own syntax. Lots of things don't go this far - first order predicate logic is sound and complete, for example (see Gödel's completeness theorem(!)).
    - pas 9y ago
      Could you please expand on the soundness and completeness of first order logic? Isn't that false generally? Because you need a deductive/axiom system, so that you can ask the question of completeness/soundness. And ZFC is too strong, hence cannot prove its soundness and correctness at the same time. But you can formalize weaker systems in first order logic, that are provably complete and sound.
      - gpm 9y ago
        (It's been a year and a half since I took a course on this, so I apologize for any mistakes) You do need to define a deductive/axiom system before you can ask the question. We can use a few different standard deductive systems. We require that the axioms are sound. Then the system is complete. (I think one should also always be able to prove false if the axioms aren't sound... but I don't recall proving that) ZFC isn't too strong. That sounds like a contradiction, but it isn't, because we don't have a rich enough vocabularly in first order logic to state the problematic statements that make it either inconsistent or incomplete in stronger logic systems. Every true statement you can state about ZFC in first order logic is provable.
        indexerror 9y ago
        > It's been a year and a half since I took a course on this Can you please recommend a MOOC/resource for learning more about this?
        gpm 9y ago
        My only real exposure to it is the course I took, csc438 at UofT taught by Steven Cook. There are pretty complete notes for the course as well as assignments here [0], but not videos or planned lessons. You certainly could learn about it by reading them, but I don't know if it would be the most efficient way. [0] http://www.cs.toronto.edu/~sacook/csc438h/ http://www.cs.toronto.edu/~sacook/csc438h/
  - snnw 9y ago
    Godel's theorem only applies to proof systems that can encode basic arithmetic, which most type systems cannot.
    - vanderZwan 9y ago
      Would a type system that can verify whether array access is always in-bound implicitly encode arithmetic somehow? My gut feeling says yes, since I don't know how one would prove bounds without arithmetic, but I don't have the mathematical knowledge to back this up.
      - lmm 9y ago
        It would need a certain amount of arithmetic, but Presburger arithmetic (addition and constant multiplication, essentially) is complete and consistent and might be enough for all the array use we care about?
  - baq 9y ago
    you can design a complete and sound type system in which any program can be checked in polynomial time. https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...
  - vilhelm_s 9y ago
    Yes, although I would appeal to Rice's theorem rather than Gödel.
- davidgay 9y ago
  Note that most common type systems "crash" type-checked programs at runtime: null-pointer check failures, array-bound check failures, and (even, Java) co-variant array write check failures. So the line is fairly fuzzy.
  - _asummers 9y ago
    Or just silently fail! Knowing the history of the Collections API and generics in Java, I know WHY this is like this, but Map.get taking an Object has resulted in way more bugs in previous code bases than I'd like to think about. If you have a Map<S, T> Java will silently take an object that has NOTHING to do with S and return null because that key is obviously not in the map. You can of course wrap that call behind functions that DO check the proper input type, but until you've been burnt by it you might not think to do that.
    - brabel 9y ago
      > If you have a Map<S, T> Java will silently take an object that has NOTHING to do with S and return null because that key is obviously not in the map Map map = new HashMap(); map.put("one", 1); class Whatever {} Map<Whatever, Integer> whateverToIntMap = (Map<Whatever, Integer>) map; Integer i = whateverToIntMap.get("one"); System.out.println("i = " + i); Prints: i = 1 That's a consequence of generics type-erasure for backwards compatibility with non-generic code, so there _is_ a reason for `get` accepting any Object.
      - _asummers 9y ago
        Like I said, I know the history and why it exists. I learned Java before 1.5 came out. That API existed long before generics did (I think 1.0 or earlier). If they had designed the language with generics in mind, they would have probably done it differently; hindsight is 20/20. Doesn't make it not a suboptimal API. I don't think there's a good way to fix it this late in the game without breaking old code, but such are the warts of backwards compatibility.
  - deleted 9y ago
- tel 9y ago
  While this is true, it's critical to note that "valid" here doesn't mean "valid as in it follows the intention of the programmer who wrote it" but instead "valid as in it either terminates in a well-defined error condition or completes to an identically-typed result" (preservation and progress). The engineering constraint is to ensure that the design and logic of the types themselves enable preservation-and-progress-validity to enforce meaningful semantic constraints. A sound and complete type system can still say things that aren't practically meaningful.
- jackfoxy 9y ago
  > Soundness means that every program that typechecks is valid. Completeness means that every valid program can be typed. I like this definition. Can someone link to an authoritative article that elaborates on this statement?
  - eslaught 9y ago
    This is a pretty standard definition (though sometimes the words get swapped). E.g. you see a very similar sentence in Wikipedia: > Informally, a soundness theorem for a deductive system expresses that all provable sentences are true. Completeness states that all true sentences are provable. https://en.wikipedia.org/wiki/Soundness#Relation_to_completeness https://en.wikipedia.org/wiki/Soundness#Relation_to_complete... You could probably follow the references there to more authoritative sources.
    - jackfoxy 9y ago
      I was looking for something specific to type systems, but this is a good start.
    - Izkata 9y ago
      Ehh, no. The definition on Wikipedia - at least the part you quoted, the rest is too jargony for me - is circular (and makes me think it's incorrect/missing something). The GP's sentence would require a third link, which missing means it isn't circular. Programs that can be typed will not necessarily be typecheck-able successfully. (I hope what I'm trying to get at makes sense and I'm not causing more confusion... what I have in mind is things like Java's ClassCastException - everything's typed, the typecheck passes, but it wasn't actually successful. Going by the Wikipedia quote, it would mean it wasn't actually possible for this exception to be thrown.)
      - a-saleh 9y ago
        I think this might be, because the definition seems to stem from mathematical notion of logic. And logicians usually want to have their logics sound, because if you can prove false statements, what is the point of your logic, right? So to distinguish between sound/unsound typesystem, I would look at it as if it were logic, where types are my theorems, and typechecking is attempt to find a proof. Of course, type-system for a language has to have some compromises, Java explicitly tells you, that even typechcecked program still will have runtime exceptions (like ClassCastException). In haskell you can still fall into an infinite loop, even though all the types flow through the system as expected :-)
masklinn 9y ago
> Not because it’s nice to have a type that "foo" satisfies and not "bar", but because there is actual code out there that does this, today. Same for structural typing (TypeScript would be absolute horror to interface with existing code without it). That's in the line of Erlang's Dialyzer (one of the earliest "gradual typing" tools I know of), which also had to contend with actually being useful and being able to type actual usage patterns of existing years-old codebases..
- _asummers 9y ago
  Link to some papers around Dialyzer[0] Anecdotally, as an Elixir developer, I find Dialyzer to be pretty OK. Sometimes it misses things I think it should catch, but you quickly learn ways of structuring your code to help it more (not abusing macros, for one). We made a decision in the infancy of the code base to mandate typespecs for every function (both public and private) in the code base, and it has paid off in strides if for nothing else than documentation when you open a module you haven't touched in months. It catching bugs at CI time is a huge bonus. The error messages are... not great. I have it on hold right now, but I've got a branch for improving all the error messages in Elixir. Many library authors are unfortunately not very diligent in speccing their programs. My first contribution to a dependency we use is often fixing their type specs to allow our code to type check. Some don't even bother putting in typespecs and Dialyzer gets upset because there's code paths it can't quite figure out, or even worse when one is wrong really deep in the middle. Seeing 80 errors in bright red because of a widely used utility function saying it returns a String.t() instead of an integer can be frustrating. Re: CI, due to Dialyzer's persistent lookup table (PLTs) for all your app dependencies taking FOREVER to build from scratch, we had to do some trickery to get it cached as an artifact for future builds. But once that got working, CI got very snappy. It's really determined as a function of the triplet (erlang_version, elixir_version, the hashes of all your dependencies), so you can do things like create a docker image with a tag that is a function of that triplet. [0] http://www.it.uu.se/research/group/hipe/dialyzer/ http://www.it.uu.se/research/group/hipe/dialyzer/
- bjz_ 9y ago
  I kind of found Dialyzer disappointing from starting a project from scratch. It would miss many obvious mistakes that I expected would be caught. Very much was not a fan of this key design decision of success typing! That said, the theoretical research behind it I can respect.
leshow 9y ago
I think another reason they added refinement types in the form of literal string types and literal number types was because there are no data constructors in TS & Flow either. This is a bit of speculation on my part. For example, in lots of strongly typed languages when you make a sum type there's a constructor. haskell, data Foo = Baz | Bar or rust, enum Foo { Baz, Bar } Baz and Bar are data constructors, they allow you to pattern match on them and make new values. In ts an equivalent sum type has to use a string/number refinement. type Foo = { kind: "baz" } | { kind: "bar" } This fits closer to js semantics and still allows sum types to be written. Unfortunately the pattern matching isn't anywhere near as good, but I applaud them for adding this to the language.

Tarean 9y ago

There are basically two important results for type systems, soundndess and completeness. Soundness means that every program that typechecks is valid. Completeness means that every valid program can be typed. So basically typescripts type system doesn't match the language semantics so type checked programs may crash at runtime.

s_kilk 9y ago
I'm curious, given Godels incompleteness theory, isn't it impossible to have both soundness and completeness in the same language?
- karatinversion 9y ago
  Gödel's incompleteness is for proof systems for languages which contain enough arithmetic to express its own syntax. Lots of things don't go this far - first order predicate logic is sound and complete, for example (see Gödel's completeness theorem(!)).
  - pas 9y ago
    Could you please expand on the soundness and completeness of first order logic? Isn't that false generally? Because you need a deductive/axiom system, so that you can ask the question of completeness/soundness. And ZFC is too strong, hence cannot prove its soundness and correctness at the same time. But you can formalize weaker systems in first order logic, that are provably complete and sound.
    - gpm 9y ago
      (It's been a year and a half since I took a course on this, so I apologize for any mistakes) You do need to define a deductive/axiom system before you can ask the question. We can use a few different standard deductive systems. We require that the axioms are sound. Then the system is complete. (I think one should also always be able to prove false if the axioms aren't sound... but I don't recall proving that) ZFC isn't too strong. That sounds like a contradiction, but it isn't, because we don't have a rich enough vocabularly in first order logic to state the problematic statements that make it either inconsistent or incomplete in stronger logic systems. Every true statement you can state about ZFC in first order logic is provable.
      - indexerror 9y ago
        > It's been a year and a half since I took a course on this Can you please recommend a MOOC/resource for learning more about this?
        gpm 9y ago
        My only real exposure to it is the course I took, csc438 at UofT taught by Steven Cook. There are pretty complete notes for the course as well as assignments here [0], but not videos or planned lessons. You certainly could learn about it by reading them, but I don't know if it would be the most efficient way. [0] http://www.cs.toronto.edu/~sacook/csc438h/ http://www.cs.toronto.edu/~sacook/csc438h/
- snnw 9y ago
  Godel's theorem only applies to proof systems that can encode basic arithmetic, which most type systems cannot.
  - vanderZwan 9y ago
    Would a type system that can verify whether array access is always in-bound implicitly encode arithmetic somehow? My gut feeling says yes, since I don't know how one would prove bounds without arithmetic, but I don't have the mathematical knowledge to back this up.
    - lmm 9y ago
      It would need a certain amount of arithmetic, but Presburger arithmetic (addition and constant multiplication, essentially) is complete and consistent and might be enough for all the array use we care about?
- baq 9y ago
  you can design a complete and sound type system in which any program can be checked in polynomial time. https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...
- vilhelm_s 9y ago
  Yes, although I would appeal to Rice's theorem rather than Gödel.
davidgay 9y ago
Note that most common type systems "crash" type-checked programs at runtime: null-pointer check failures, array-bound check failures, and (even, Java) co-variant array write check failures. So the line is fairly fuzzy.
- _asummers 9y ago
  Or just silently fail! Knowing the history of the Collections API and generics in Java, I know WHY this is like this, but Map.get taking an Object has resulted in way more bugs in previous code bases than I'd like to think about. If you have a Map<S, T> Java will silently take an object that has NOTHING to do with S and return null because that key is obviously not in the map. You can of course wrap that call behind functions that DO check the proper input type, but until you've been burnt by it you might not think to do that.
  - brabel 9y ago
    > If you have a Map<S, T> Java will silently take an object that has NOTHING to do with S and return null because that key is obviously not in the map Map map = new HashMap(); map.put("one", 1); class Whatever {} Map<Whatever, Integer> whateverToIntMap = (Map<Whatever, Integer>) map; Integer i = whateverToIntMap.get("one"); System.out.println("i = " + i); Prints: i = 1 That's a consequence of generics type-erasure for backwards compatibility with non-generic code, so there _is_ a reason for `get` accepting any Object.
    - _asummers 9y ago
      Like I said, I know the history and why it exists. I learned Java before 1.5 came out. That API existed long before generics did (I think 1.0 or earlier). If they had designed the language with generics in mind, they would have probably done it differently; hindsight is 20/20. Doesn't make it not a suboptimal API. I don't think there's a good way to fix it this late in the game without breaking old code, but such are the warts of backwards compatibility.
- deleted 9y ago
tel 9y ago
While this is true, it's critical to note that "valid" here doesn't mean "valid as in it follows the intention of the programmer who wrote it" but instead "valid as in it either terminates in a well-defined error condition or completes to an identically-typed result" (preservation and progress). The engineering constraint is to ensure that the design and logic of the types themselves enable preservation-and-progress-validity to enforce meaningful semantic constraints. A sound and complete type system can still say things that aren't practically meaningful.
jackfoxy 9y ago
> Soundness means that every program that typechecks is valid. Completeness means that every valid program can be typed. I like this definition. Can someone link to an authoritative article that elaborates on this statement?
- eslaught 9y ago
  This is a pretty standard definition (though sometimes the words get swapped). E.g. you see a very similar sentence in Wikipedia: > Informally, a soundness theorem for a deductive system expresses that all provable sentences are true. Completeness states that all true sentences are provable. https://en.wikipedia.org/wiki/Soundness#Relation_to_completeness https://en.wikipedia.org/wiki/Soundness#Relation_to_complete... You could probably follow the references there to more authoritative sources.
  - jackfoxy 9y ago
    I was looking for something specific to type systems, but this is a good start.
  - Izkata 9y ago
    Ehh, no. The definition on Wikipedia - at least the part you quoted, the rest is too jargony for me - is circular (and makes me think it's incorrect/missing something). The GP's sentence would require a third link, which missing means it isn't circular. Programs that can be typed will not necessarily be typecheck-able successfully. (I hope what I'm trying to get at makes sense and I'm not causing more confusion... what I have in mind is things like Java's ClassCastException - everything's typed, the typecheck passes, but it wasn't actually successful. Going by the Wikipedia quote, it would mean it wasn't actually possible for this exception to be thrown.)
    - a-saleh 9y ago
      I think this might be, because the definition seems to stem from mathematical notion of logic. And logicians usually want to have their logics sound, because if you can prove false statements, what is the point of your logic, right? So to distinguish between sound/unsound typesystem, I would look at it as if it were logic, where types are my theorems, and typechecking is attempt to find a proof. Of course, type-system for a language has to have some compromises, Java explicitly tells you, that even typechcecked program still will have runtime exceptions (like ClassCastException). In haskell you can still fall into an infinite loop, even though all the types flow through the system as expected :-)

masklinn 9y ago

> Not because it’s nice to have a type that "foo" satisfies and not "bar", but because there is actual code out there that does this, today. Same for structural typing (TypeScript would be absolute horror to interface with existing code without it). That's in the line of Erlang's Dialyzer (one of the earliest "gradual typing" tools I know of), which also had to contend with actually being useful and being able to type actual usage patterns of existing years-old codebases..

_asummers 9y ago
Link to some papers around Dialyzer[0] Anecdotally, as an Elixir developer, I find Dialyzer to be pretty OK. Sometimes it misses things I think it should catch, but you quickly learn ways of structuring your code to help it more (not abusing macros, for one). We made a decision in the infancy of the code base to mandate typespecs for every function (both public and private) in the code base, and it has paid off in strides if for nothing else than documentation when you open a module you haven't touched in months. It catching bugs at CI time is a huge bonus. The error messages are... not great. I have it on hold right now, but I've got a branch for improving all the error messages in Elixir. Many library authors are unfortunately not very diligent in speccing their programs. My first contribution to a dependency we use is often fixing their type specs to allow our code to type check. Some don't even bother putting in typespecs and Dialyzer gets upset because there's code paths it can't quite figure out, or even worse when one is wrong really deep in the middle. Seeing 80 errors in bright red because of a widely used utility function saying it returns a String.t() instead of an integer can be frustrating. Re: CI, due to Dialyzer's persistent lookup table (PLTs) for all your app dependencies taking FOREVER to build from scratch, we had to do some trickery to get it cached as an artifact for future builds. But once that got working, CI got very snappy. It's really determined as a function of the triplet (erlang_version, elixir_version, the hashes of all your dependencies), so you can do things like create a docker image with a tag that is a function of that triplet. [0] http://www.it.uu.se/research/group/hipe/dialyzer/ http://www.it.uu.se/research/group/hipe/dialyzer/
bjz_ 9y ago
I kind of found Dialyzer disappointing from starting a project from scratch. It would miss many obvious mistakes that I expected would be caught. Very much was not a fan of this key design decision of success typing! That said, the theoretical research behind it I can respect.

leshow 9y ago

I think another reason they added refinement types in the form of literal string types and literal number types was because there are no data constructors in TS & Flow either. This is a bit of speculation on my part. For example, in lots of strongly typed languages when you make a sum type there's a constructor. haskell, data Foo = Baz | Bar or rust, enum Foo { Baz, Bar } Baz and Bar are data constructors, they allow you to pattern match on them and make new values. In ts an equivalent sum type has to use a string/number refinement. type Foo = { kind: "baz" } | { kind: "bar" } This fits closer to js semantics and still allows sum types to be written. Unfortunately the pattern matching isn't anywhere near as good, but I applaud them for adding this to the language.