5 ms·

> increased expressive power at the cost of delayed verification. I don't see where the increased expressive power comes from. Dynamic checks are equally doabl

> increased expressive power at the cost of delayed verification. I don't see where the increased expressive power comes from. Dynamic checks are equally doable in a typed and an untyped setting. But let's say it gives you more expressive power. It does so at the cost of no verification. Validation is a very poor substitute. > Because the real answer is probably "it's too hard to do". It's common usage of GADTs and DataKinds nowadays. Granted, strictly speaking not Haskell, but GHC Haskell. > By the way, you probably want linear types in order to encode state machines in the type system in a natural way You only need linear types if you need to enforce that (some) values will have a single logical future.

pron 10y ago
> Dynamic checks are equally doable in a typed and an untyped setting. Yes, but specs are not "dynamic checks" but rather "static metadata". How they are checked depends on the tooling. It's true that a typed language could support specs, but those would either be an additional orthogonal mechanism (like Java and JML/C# and Spec#, or somewhat differently, Isabelle/HOL) or encoded in dependent types, which require the tooling to be built into the compiler, which would support either manual/interactive proofs (as in Agda/Coq respectively) or automatic inference (as in Liquid Haskell). > It's common usage of GADTs and DataKinds nowadays. Granted, strictly speaking not Haskell, but GHC Haskell. That's not the same level of expressivity, and certainly not the same level of effort.
- catnaroek 10y ago
  > Yes, but specs are not "dynamic checks" but rather "static metadata". It's the checking that matters, not the declaration of intentions. If the checking is dynamic, I'm calling the whole thing dynamic. And, because there exist hard limits on what can be inferred about programs, certain specification styles don't support static verification without additional programmer-supplied information. > That's not the same level of expressivity, and certainly not the same level of effort. Using GADTs parameterized by DataKinds to encode problem domain logic is by now a de facto standard practice in the Haskell community. It wouldn't have done so if it required an unreasonable amount of effort.
  - pron 10y ago
    > If the checking is dynamic, I'm calling the whole thing dynamic. Who says the checking is dynamic? This release contains several orthogonal capabilities: specs, which are a completely static language feature, and a few dynamic checking tools. Tomorrow they can release some static checking tools. Java's JML and C#'s Spec# are similar. They are static specs, but there are various tools for checking them, some static (using SMT solvers or model checkers), some dynamic (dynamic contracts), and some mixed (e.g. concolic tests). > Using GADTs parameterized by DataKinds to encode problem domain logic is by now a de facto standard practice in the Haskell community. It wouldn't have done so if it required an unreasonable amount of effort. First, I didn't say unreasonable, but I think it is still more effort. Second, without dependent types (which require proof, either manual -- which is a lot of effort -- or automatic -- which is rather limited), you can't nearly express the same propositions. The advantages and disadvantages of types do not stem from them expressing static propositions -- there are many ways of doing that -- but from them expressing propositions in a certain way that influences how the program is organized and how propositions propagate throughout the program. Whether propositions about code are best expressed as types or as data-level propositions is an interesting debate, but a rather subtle one; it is certainly not binary. IMO, it is likely that some propositions are best expressed as types while others are best expressed differently.
    - catnaroek 10y ago
      > Tomorrow they can release some static checking tools. Java's JML and C#'s Spec# are similar. If, in order to check a program, you need to supply additional annotations, you aren't checking the original program - you are checking the extended annotated program. So let's not conflate these two languages: (0) The whole of Java, and, (1) The collection of Java programs, equipped with JML annotations, that can be statically verified by some given tool. If the annotations express facts inexpressible in Java's type system, and tool performs a sound analysis, then you can prove more safety theorems about the second language. (And if the analysis is unsound, why bother with it?) That both languages happen to have mostly the same surface syntax and dynamics is best regarded as a happy accident. > First, I didn't say unreasonable, but I think it is still more effort. How so? All you have to do is think what properties you want to hold for your system. But this is something you have to do whether you encode these properties in types or not. > Second, without dependent types (which require proof, either manual -- which is a lot of effort -- or automatic -- which is rather limited), you can't nearly express the same propositions. I never said otherwise. I only said “using GADTs and DataKinds to express problem domain constraints is a de facto standard practice”. > The advantages and disadvantages of types do not stem from them expressing static propositions -- there are many ways of doing that Merely expressing static propositions is boring. What really matters is proving them. > but from them expressing propositions in a certain way In a compositional way: the types of expressions can be synthesized from those of their subexpressions, and the types of defined symbols can be recovered from their definitions' right-hand sides. > that influences how the program is organized and how propositions propagate throughout the program. In a modular way: when checking a module Foo, you won't observe a failure of an invariant internal to another module Bar. > Whether propositions about code are best expressed as types or as data-level propositions is an interesting debate, but a rather subtle one; it is certainly not binary. I can see legitimate use cases for expressing propositions as types (most of the time), as well as legitimate use cases for not bothering to represent propositions in a mechanically verifiable manner (when the proof is obvious, only needed in a very small part of the code, and explicit annotations would only add noise). But I can't see a use case for expressing yet not proving nontrivial propositions that you expect to hold. If it isn't trivial, you need a proof. > IMO, it is likely that some propositions are best expressed as types while others are best expressed differently. Whatever makes the proof go through the easiest.

pron 10y ago

> Dynamic checks are equally doable in a typed and an untyped setting. Yes, but specs are not "dynamic checks" but rather "static metadata". How they are checked depends on the tooling. It's true that a typed language could support specs, but those would either be an additional orthogonal mechanism (like Java and JML/C# and Spec#, or somewhat differently, Isabelle/HOL) or encoded in dependent types, which require the tooling to be built into the compiler, which would support either manual/interactive proofs (as in Agda/Coq respectively) or automatic inference (as in Liquid Haskell). > It's common usage of GADTs and DataKinds nowadays. Granted, strictly speaking not Haskell, but GHC Haskell. That's not the same level of expressivity, and certainly not the same level of effort.

catnaroek 10y ago
> Yes, but specs are not "dynamic checks" but rather "static metadata". It's the checking that matters, not the declaration of intentions. If the checking is dynamic, I'm calling the whole thing dynamic. And, because there exist hard limits on what can be inferred about programs, certain specification styles don't support static verification without additional programmer-supplied information. > That's not the same level of expressivity, and certainly not the same level of effort. Using GADTs parameterized by DataKinds to encode problem domain logic is by now a de facto standard practice in the Haskell community. It wouldn't have done so if it required an unreasonable amount of effort.
- pron 10y ago
  > If the checking is dynamic, I'm calling the whole thing dynamic. Who says the checking is dynamic? This release contains several orthogonal capabilities: specs, which are a completely static language feature, and a few dynamic checking tools. Tomorrow they can release some static checking tools. Java's JML and C#'s Spec# are similar. They are static specs, but there are various tools for checking them, some static (using SMT solvers or model checkers), some dynamic (dynamic contracts), and some mixed (e.g. concolic tests). > Using GADTs parameterized by DataKinds to encode problem domain logic is by now a de facto standard practice in the Haskell community. It wouldn't have done so if it required an unreasonable amount of effort. First, I didn't say unreasonable, but I think it is still more effort. Second, without dependent types (which require proof, either manual -- which is a lot of effort -- or automatic -- which is rather limited), you can't nearly express the same propositions. The advantages and disadvantages of types do not stem from them expressing static propositions -- there are many ways of doing that -- but from them expressing propositions in a certain way that influences how the program is organized and how propositions propagate throughout the program. Whether propositions about code are best expressed as types or as data-level propositions is an interesting debate, but a rather subtle one; it is certainly not binary. IMO, it is likely that some propositions are best expressed as types while others are best expressed differently.
  - catnaroek 10y ago
    > Tomorrow they can release some static checking tools. Java's JML and C#'s Spec# are similar. If, in order to check a program, you need to supply additional annotations, you aren't checking the original program - you are checking the extended annotated program. So let's not conflate these two languages: (0) The whole of Java, and, (1) The collection of Java programs, equipped with JML annotations, that can be statically verified by some given tool. If the annotations express facts inexpressible in Java's type system, and tool performs a sound analysis, then you can prove more safety theorems about the second language. (And if the analysis is unsound, why bother with it?) That both languages happen to have mostly the same surface syntax and dynamics is best regarded as a happy accident. > First, I didn't say unreasonable, but I think it is still more effort. How so? All you have to do is think what properties you want to hold for your system. But this is something you have to do whether you encode these properties in types or not. > Second, without dependent types (which require proof, either manual -- which is a lot of effort -- or automatic -- which is rather limited), you can't nearly express the same propositions. I never said otherwise. I only said “using GADTs and DataKinds to express problem domain constraints is a de facto standard practice”. > The advantages and disadvantages of types do not stem from them expressing static propositions -- there are many ways of doing that Merely expressing static propositions is boring. What really matters is proving them. > but from them expressing propositions in a certain way In a compositional way: the types of expressions can be synthesized from those of their subexpressions, and the types of defined symbols can be recovered from their definitions' right-hand sides. > that influences how the program is organized and how propositions propagate throughout the program. In a modular way: when checking a module Foo, you won't observe a failure of an invariant internal to another module Bar. > Whether propositions about code are best expressed as types or as data-level propositions is an interesting debate, but a rather subtle one; it is certainly not binary. I can see legitimate use cases for expressing propositions as types (most of the time), as well as legitimate use cases for not bothering to represent propositions in a mechanically verifiable manner (when the proof is obvious, only needed in a very small part of the code, and explicit annotations would only add noise). But I can't see a use case for expressing yet not proving nontrivial propositions that you expect to hold. If it isn't trivial, you need a proof. > IMO, it is likely that some propositions are best expressed as types while others are best expressed differently. Whatever makes the proof go through the easiest.