5 ms·

Not all untyped languages are the same. E.g. Clojure now encourages specifying assumptions with spec annotations, some of them are stronger than those that can

by pron 7y ago

Not all untyped languages are the same. E.g. Clojure now encourages specifying assumptions with spec annotations, some of them are stronger than those that can be expressed by Haskell's type system: i.e. they can succinctly express more about the "entire code" than Haskell's types. Types are not the only way to write formal assertions and assumptions about code. The difference between the two is in the level of sound inference that can be made (stronger with types) and the strength and expressivity of the assertions (stronger with contracts). Of course, one could say we should have both, and some languages -- like Java with JML, C with ACSL, and SPARK, as well as some research languages like Whiley and Dafny -- do. But this could add complexity, and the interesting question is, if you could just have one, what are the relative merits of either? My guess is that types would be better for enforcing code organization and for tooling (more efficient AOT code generation, safe automatic refactoring, code completion), because automatic transformations require automatic and sound inference, while contracts are better for correctness because they can more easily express stronger properties of interest, and require less effort to verify them (types require formal deductive proofs, while contracts can use those or a range of other techniques that vary in their cost and their soundness). In short, types are not the only form of formal specification, but the different forms do have different practical characteristics. What matters is not just what we want to know about the rest of the code, but how we want to use that information and how certain we need to be. Unfortunately, theoretical results tell us that we cannot have a perfect system that is always correct, cheap to use, and can allow us to express rich properties.

capableweb 7y ago
Also, the following part isn't necessarily because of dynamic typing vs static > what types all the variables are, what expectations are attached to them, what mutation, if any, each method call performs But more about what the language offers. Clojure for example, goes beyond types with it's abstractions (like seq, that can be applied to strings, lists, maps and so on) and normally stays away from mutation, but when needed, makes it really explicit and easy to find those mutations.
- pron 7y ago
  Java's JML contract system [1] allows you to explicitly state which mutations a method performs as part of its contract. [1]: https://www.openjml.org/ https://www.openjml.org/
- yakshaving_jgt 7y ago
  > Clojure for example, goes beyond types with it's abstractions (like seq, that can be applied to strings, lists, maps and so on) Goes beyond types? Statically-typed languages can have polymorphism.
  - roenxi 7y ago
    Spec is at heart a data modelling system. So for example, (s/def ::integer integer?) is very explicitly not a definition of an "integer" type. It is preparation to model some data x and check that the data will evaluate to true if someone uses the predicate (integer? x). However, this is obviously enough to implement a type system. But you can also do some very loose things with spec that aren't done in a type system (I speak with a cheerful ignorance of type systems). Eg, I can spec a function so that one argument is smaller than the second. This allows my testing system to automatically generate the correct data to test my function. So spec can used to implement a type system but also to implement things that aren't type systems.
    - candeira 7y ago
      > But you can also do some very loose things with spec that aren't done in a type system (I speak with a cheerful ignorance of type systems). Eg, I can spec a function so that one argument is smaller than the second. This allows my testing system to automatically generate the correct data to test my function. Check out dependent type systems. These allow you to define, mindbreakingly enough, types that __depend on the values you assign at runtime__, and functions whose type depends on the values passed as arguments. Don't ask me how it's done; it's all dark magic to me. All I know is that people who use dependent type systems claim they are very good at certain uses involving incoming streams of unknown data, like parsing binary protocols. https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type
deleted 7y ago
[deleted]
Silhouette 7y ago
My guess is that types would be better for enforcing code organization and for tooling ... while contracts are better for correctness I see what you're getting at, but there is one other crucial difference: the types we're talking about here are usually checked at compile time, whereas the contracts we're talking about here are usually checked at run time. Although the latter may be more expressive if other things are equal, other things are very much not equal in this respect. How much that matters depends on the nature of the software and how it is to be deployed and used. If you're writing a program for your own use, it might not matter much at all. If you're writing a program that is going to control a satellite and software maintenance after launch is extremely expensive if not impossible, it might matter a great deal.
- pron 7y ago
  > whereas the contracts we're talking about here are usually checked at run time No, they can be checked in many different ways, hence their power. They can be checked "statically", i.e. at compile-time, or dynamically. One approach is sound but requires more effort, while the other is cheap yet unsound -- and there is a spectrum in between the two extremes. > If you're writing a program that is going to control a satellite and software maintenance after launch is extremely expensive if not impossible, it might matter a great deal. Such programs often use formal methods that precisely use such contracts. Rich type systems (like Idris's) are virtually never used in practice in those cases. If you've heard of SPARK, it's a language that provides static verification of properties specified as contracts, not as part of the type system, and it is used in some safety-critical realtime applications.
  - Silhouette 7y ago
    No, they can be checked in many different ways, hence their power. Sure, but the more dynamic ones that drift away from what a (good) static type system offers are exactly the ones that aren't amenable to automated proofs and so tend to be checked at run time. Such programs often use formal methods that precisely use such contracts. Rich type systems (like Idris's) are virtually never used in practice in those cases. As someone who has worked on relatively high-reliability systems, I can say with 100% confidence: it depends. This too is an area with a whole spectrum of possibilities, and some of those involve a degree of formal proof of algorithm properties but not a mechanically verified translation of those algorithms into implementation code. In such cases, a powerful static type system certainly can be a useful safeguard against introducing defects during the translation.
chrisdone 7y ago
Techniques like Ghost of Departed Proofs are the most exciting thing to me as a casual correctness enthusiast. It acts as a means of combining static types with contracts. Types are sound mostly because they are a stupid mini language, so easily enforced, like you said. Contracts are practical and convenient because you tend to write them in the language or a subset thereof that you’re checking. That’s hard to ignore. GODP has you write a runtime check in regular code, and return as a result a proof value. Put that code in a module boundary. Then you have upstream functions expect a proof argument along with the value the proof is about. They’re tied together with a unique type variable (rank n or existential are the mechanisms of delivery for Haskell, but may differ in other languages). head :: NonEmpty n -> Named n (List a) -> a In this way you started from a dynamic, runtime piece of code, and ended up using a static type system to just ensure everything is passed around correctly which is trivial. A single proof in this technique is nominal in the type (e.g. not null or positive or sorted ascending/descending), but combining them is done at the value level so there’s flexibility. The bang for buck potential is large. I’m more interested in stuff like this than the dependent types direction that people are pushing for in GHC. If I wanted dependent types I have Agda, Coq, Isabelle, Idris, etc. to play with.
- dwohnitmok 7y ago
  Actually techniques like the Ghost of Departed Proofs are precisely the reason I'm excited about dependent types (although with the caveat that you need some way of talking about erasure). Contract systems in general have the problem that it is difficult to express higher-order properties about how functions should interact with each other or repeated invocations of themselves. For example, it's rather convoluted to express associativity with a contract system. Contract systems are very well-suited for imperative contexts (see e.g. Hoare Logic), where you have procedures rather than functions and you usually don't think about e.g. whether a procedure is associative or not. They work for functions, but are not as great a fit. Dependent types allow for further expressivity, and, crucially, as long as you separate theorems from code (that is as long as you don't take Curry-Howard too seriously), there's no reason you're forced to prove a theorem with the type system if you find it too difficult. Imagine: concat : List a -> List a -> List a concat = ... concatSumsLength : (xs : List a) -> (ys : List a) -> size (concat xs ys) = size xs + size ys concatSumsLength = proofByPropertyTest concatPropertyTest concatPropertyTest = (1000 different lists concatenated together and then checking that their sizes add up) There's no reason that concatSumsLength needs to be satisfied by a true implementation, unless you require that its value be usable at runtime. However, as Idris 2 shows, there's no need for that to be true (or even Coq with Prop vs Type). You can just annotate it as erased at runtime. If you have a way of ensuring that certain values are never used at runtime, then there is no reason that your proof obligations must be met through satisfying the type checker.

by pron 7y ago

capableweb 7y ago

Also, the following part isn't necessarily because of dynamic typing vs static > what types all the variables are, what expectations are attached to them, what mutation, if any, each method call performs But more about what the language offers. Clojure for example, goes beyond types with it's abstractions (like seq, that can be applied to strings, lists, maps and so on) and normally stays away from mutation, but when needed, makes it really explicit and easy to find those mutations.

pron 7y ago
Java's JML contract system [1] allows you to explicitly state which mutations a method performs as part of its contract. [1]: https://www.openjml.org/ https://www.openjml.org/
yakshaving_jgt 7y ago
> Clojure for example, goes beyond types with it's abstractions (like seq, that can be applied to strings, lists, maps and so on) Goes beyond types? Statically-typed languages can have polymorphism.
- roenxi 7y ago
  Spec is at heart a data modelling system. So for example, (s/def ::integer integer?) is very explicitly not a definition of an "integer" type. It is preparation to model some data x and check that the data will evaluate to true if someone uses the predicate (integer? x). However, this is obviously enough to implement a type system. But you can also do some very loose things with spec that aren't done in a type system (I speak with a cheerful ignorance of type systems). Eg, I can spec a function so that one argument is smaller than the second. This allows my testing system to automatically generate the correct data to test my function. So spec can used to implement a type system but also to implement things that aren't type systems.
  - candeira 7y ago
    > But you can also do some very loose things with spec that aren't done in a type system (I speak with a cheerful ignorance of type systems). Eg, I can spec a function so that one argument is smaller than the second. This allows my testing system to automatically generate the correct data to test my function. Check out dependent type systems. These allow you to define, mindbreakingly enough, types that __depend on the values you assign at runtime__, and functions whose type depends on the values passed as arguments. Don't ask me how it's done; it's all dark magic to me. All I know is that people who use dependent type systems claim they are very good at certain uses involving incoming streams of unknown data, like parsing binary protocols. https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type

deleted 7y ago

[deleted]

Silhouette 7y ago

My guess is that types would be better for enforcing code organization and for tooling ... while contracts are better for correctness I see what you're getting at, but there is one other crucial difference: the types we're talking about here are usually checked at compile time, whereas the contracts we're talking about here are usually checked at run time. Although the latter may be more expressive if other things are equal, other things are very much not equal in this respect. How much that matters depends on the nature of the software and how it is to be deployed and used. If you're writing a program for your own use, it might not matter much at all. If you're writing a program that is going to control a satellite and software maintenance after launch is extremely expensive if not impossible, it might matter a great deal.

pron 7y ago
> whereas the contracts we're talking about here are usually checked at run time No, they can be checked in many different ways, hence their power. They can be checked "statically", i.e. at compile-time, or dynamically. One approach is sound but requires more effort, while the other is cheap yet unsound -- and there is a spectrum in between the two extremes. > If you're writing a program that is going to control a satellite and software maintenance after launch is extremely expensive if not impossible, it might matter a great deal. Such programs often use formal methods that precisely use such contracts. Rich type systems (like Idris's) are virtually never used in practice in those cases. If you've heard of SPARK, it's a language that provides static verification of properties specified as contracts, not as part of the type system, and it is used in some safety-critical realtime applications.
- Silhouette 7y ago
  No, they can be checked in many different ways, hence their power. Sure, but the more dynamic ones that drift away from what a (good) static type system offers are exactly the ones that aren't amenable to automated proofs and so tend to be checked at run time. Such programs often use formal methods that precisely use such contracts. Rich type systems (like Idris's) are virtually never used in practice in those cases. As someone who has worked on relatively high-reliability systems, I can say with 100% confidence: it depends. This too is an area with a whole spectrum of possibilities, and some of those involve a degree of formal proof of algorithm properties but not a mechanically verified translation of those algorithms into implementation code. In such cases, a powerful static type system certainly can be a useful safeguard against introducing defects during the translation.

chrisdone 7y ago

Techniques like Ghost of Departed Proofs are the most exciting thing to me as a casual correctness enthusiast. It acts as a means of combining static types with contracts. Types are sound mostly because they are a stupid mini language, so easily enforced, like you said. Contracts are practical and convenient because you tend to write them in the language or a subset thereof that you’re checking. That’s hard to ignore. GODP has you write a runtime check in regular code, and return as a result a proof value. Put that code in a module boundary. Then you have upstream functions expect a proof argument along with the value the proof is about. They’re tied together with a unique type variable (rank n or existential are the mechanisms of delivery for Haskell, but may differ in other languages). head :: NonEmpty n -> Named n (List a) -> a In this way you started from a dynamic, runtime piece of code, and ended up using a static type system to just ensure everything is passed around correctly which is trivial. A single proof in this technique is nominal in the type (e.g. not null or positive or sorted ascending/descending), but combining them is done at the value level so there’s flexibility. The bang for buck potential is large. I’m more interested in stuff like this than the dependent types direction that people are pushing for in GHC. If I wanted dependent types I have Agda, Coq, Isabelle, Idris, etc. to play with.

dwohnitmok 7y ago
Actually techniques like the Ghost of Departed Proofs are precisely the reason I'm excited about dependent types (although with the caveat that you need some way of talking about erasure). Contract systems in general have the problem that it is difficult to express higher-order properties about how functions should interact with each other or repeated invocations of themselves. For example, it's rather convoluted to express associativity with a contract system. Contract systems are very well-suited for imperative contexts (see e.g. Hoare Logic), where you have procedures rather than functions and you usually don't think about e.g. whether a procedure is associative or not. They work for functions, but are not as great a fit. Dependent types allow for further expressivity, and, crucially, as long as you separate theorems from code (that is as long as you don't take Curry-Howard too seriously), there's no reason you're forced to prove a theorem with the type system if you find it too difficult. Imagine: concat : List a -> List a -> List a concat = ... concatSumsLength : (xs : List a) -> (ys : List a) -> size (concat xs ys) = size xs + size ys concatSumsLength = proofByPropertyTest concatPropertyTest concatPropertyTest = (1000 different lists concatenated together and then checking that their sizes add up) There's no reason that concatSumsLength needs to be satisfied by a true implementation, unless you require that its value be usable at runtime. However, as Idris 2 shows, there's no need for that to be true (or even Coq with Prop vs Type). You can just annotate it as erased at runtime. If you have a way of ensuring that certain values are never used at runtime, then there is no reason that your proof obligations must be met through satisfying the type checker.