7 ms·

> Certainly this is true, but if you're in an entirely unityped setting... do you have any guarantees? This is what clojure.spec is all about. The answer is no

> Certainly this is true, but if you're in an entirely unityped setting... do you have any guarantees? This is what clojure.spec is all about. The answer is not, of course, "no". They are "reinventing a run-time type checker" and prefer it that way because it allows increased expressive power at the cost of delayed verification. > Ah, yes, I understand what you mean now, but you can actually encode that if you really want to. (If we assume Haskell, there's very limited DT programming which will probably let you state which transitions are legal. I must admit I'm not very up-to-speed on it, but see the next paragraph.) So you don't actually know how to do it, but assume that you can. This a little strange. Are you sure that "people usually don't want to go that far"? Because the real answer is probably "it's too hard to do". By the way, you probably want linear types in order to encode state machines in the type system in a natural way, which Haskell does not have.

mac01021 10y ago
> So you don't actually know how to do it, but assume that you can. This a little strange. Not all that strange. I trust the members of the Algorithms Research community when they tell me it's possible to test a number for primality in polynomial time. I have no idea how to do it.
- _asummers 10y ago
  AKS is the name of that algorithm, by the way, after the initials of the authors. The paper is called "PRIMES in P". https://en.wikipedia.org/wiki/AKS_primality_test https://en.wikipedia.org/wiki/AKS_primality_test
tome 10y ago
> So you don't actually know how to do it, but assume that you can. This a little strange. Also a little strange to follow this ticking off with a false claim "you probably want linear types in order to encode state machines". State machines certainly do not require linear types.
- tree_of_item 10y ago
  My claim is not false: state machines do not "require" linear types, but that is not what I said. I said linear types are what you want if you want to encode these things in a natural way. Substructural (linear) types are ALL ABOUT encoding stateful propositions in the type system. Even if you had an expressive dependent type system, the best way to type check a stateful protocol would be to add substructural types to it! See http://users.eecs.northwestern.edu/~jesse/pubs/dissertation/tov-dissertation-screen.pdf http://users.eecs.northwestern.edu/~jesse/pubs/dissertation/... for a good discussion of encoding stateful propositions with substructural (linear) type systems.
  - catnaroek 10y ago
    This is wrong. Linear types are about values having a single-threaded logical history. It's true that linear types allow you to soundly implement certain operations as in-place modifications of their inputs, because these inputs are guaranteed not to be used anymore by other computations. But that's an implementation detail. If you don't need to control the number of logical futures of your values, you don't need linear types.
lomnakkus 10y ago
> They are "reinventing a run-time type checker" and prefer it that way because it allows increased expressive power at the cost of delayed verification. Well, to me "delayed verification" is worth nothing. There is an almost unbounded infinity of program states. I want proof before I run the program. (That's, like, the point, man! I'm not going to send up a space shuttle and just count on "oh, well, our error recovery is great and we saw no errors during testing anyway". To quote a great comedian: "Are you having a laugh?") > So you don't actually know how to do it, but assume that you can. Oh, come on, be a little more charitable. I don't know, but people in the DT community know and will tell you... at length how to do it. > By the way, you probably want linear types in order to encode state machines in the type system in a natural way, which Haskell does not have. Indeed it does not... but I must say I don't miss them that much for all practical purposes. If what you want to do is encoding state machines and prove things about said machines, then you probably want an even more specialized language. I'm OK with that. I'm not OK with saying: "Can't be done in language X, therefore all effort at static verification is futile." So there.
- pron 10y ago
  > I want proof before I run the program. Except that for most interesting propositions you can't have proof. You need to show that the crude propositions that your type system can prove are what makes all the difference. I'm not so sure that's the case.
  - lomnakkus 10y ago
    Well, what's "most interesting"? That me there's a lot interesting stuff that can automatically get proven by the compiler given a little effort on your part. It may not be the most interesting, but that doesn't make it worthless, does it?
catnaroek 10y ago
> 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
> reinventing a run-time type checker It's not a runtime type checker, but a spec (not a type[1]!) that tools can use to check in different ways. ------------ [1]: A spec is a proposition; a type is a judgment (that corresponds to a proposition). E.g., you can have a type: `data A = 1 | 2 | 3`, and `data B = 3 | 4 | 5`, but then testing `a < b` (assuming `a:A b:B`) may not be straightforward (depending on the language), while a spec of `A = {1, 2, 3}, B = {1, 2, 3}, a ∈ A, b ∈ B` does let you test `a < b`.
- lomnakkus 10y ago
  Types are propositions. See Curry-Howard.
  - pron 10y ago
    Types encode propositions (see Curry-Howard) but are logical judgments in the language's logic. The expression `a:A` does not have a boolean truth value (like a logical proposition), but is rather a judgment. In my example above, the value of the expression `a ∈ B` is true iff a = 3 and false otherwise, but the expression `a:B` is just not a well-formed expression. In other words, you could create a type that corresponds to a proposition, but type assignment is distinct from a proposition (e.g. the proposition `b1 < b2`, assuming `b1,b2:B`) in the language. More precisely, you could say that types encode propositions at the type level (even if the language allows the same data-level syntax in type definitions, as in Idris), while propositions at the data level are distinct, while specs are data level propositions.
    - catnaroek 10y ago
      `x:T` is a typing judgment. A typing judgment is not a type, even if one of its constituent parts (`T`) is a type. What you call “data-level propositions” is really just “data-level abstract syntax representation of propositions”. Propositions really are types. (Though, of course, there are types that are not propositions.) And your example is simply not valid Haskell.
      - 10y ago

mac01021 10y ago

> So you don't actually know how to do it, but assume that you can. This a little strange. Not all that strange. I trust the members of the Algorithms Research community when they tell me it's possible to test a number for primality in polynomial time. I have no idea how to do it.

_asummers 10y ago
AKS is the name of that algorithm, by the way, after the initials of the authors. The paper is called "PRIMES in P". https://en.wikipedia.org/wiki/AKS_primality_test https://en.wikipedia.org/wiki/AKS_primality_test

tome 10y ago

> So you don't actually know how to do it, but assume that you can. This a little strange. Also a little strange to follow this ticking off with a false claim "you probably want linear types in order to encode state machines". State machines certainly do not require linear types.

tree_of_item 10y ago
My claim is not false: state machines do not "require" linear types, but that is not what I said. I said linear types are what you want if you want to encode these things in a natural way. Substructural (linear) types are ALL ABOUT encoding stateful propositions in the type system. Even if you had an expressive dependent type system, the best way to type check a stateful protocol would be to add substructural types to it! See http://users.eecs.northwestern.edu/~jesse/pubs/dissertation/tov-dissertation-screen.pdf http://users.eecs.northwestern.edu/~jesse/pubs/dissertation/... for a good discussion of encoding stateful propositions with substructural (linear) type systems.
- catnaroek 10y ago
  This is wrong. Linear types are about values having a single-threaded logical history. It's true that linear types allow you to soundly implement certain operations as in-place modifications of their inputs, because these inputs are guaranteed not to be used anymore by other computations. But that's an implementation detail. If you don't need to control the number of logical futures of your values, you don't need linear types.

lomnakkus 10y ago

> They are "reinventing a run-time type checker" and prefer it that way because it allows increased expressive power at the cost of delayed verification. Well, to me "delayed verification" is worth nothing. There is an almost unbounded infinity of program states. I want proof before I run the program. (That's, like, the point, man! I'm not going to send up a space shuttle and just count on "oh, well, our error recovery is great and we saw no errors during testing anyway". To quote a great comedian: "Are you having a laugh?") > So you don't actually know how to do it, but assume that you can. Oh, come on, be a little more charitable. I don't know, but people in the DT community know and will tell you... at length how to do it. > By the way, you probably want linear types in order to encode state machines in the type system in a natural way, which Haskell does not have. Indeed it does not... but I must say I don't miss them that much for all practical purposes. If what you want to do is encoding state machines and prove things about said machines, then you probably want an even more specialized language. I'm OK with that. I'm not OK with saying: "Can't be done in language X, therefore all effort at static verification is futile." So there.

pron 10y ago
> I want proof before I run the program. Except that for most interesting propositions you can't have proof. You need to show that the crude propositions that your type system can prove are what makes all the difference. I'm not so sure that's the case.
- lomnakkus 10y ago
  Well, what's "most interesting"? That me there's a lot interesting stuff that can automatically get proven by the compiler given a little effort on your part. It may not be the most interesting, but that doesn't make it worthless, does it?

catnaroek 10y ago

> 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

> reinventing a run-time type checker It's not a runtime type checker, but a spec (not a type[1]!) that tools can use to check in different ways. ------------ [1]: A spec is a proposition; a type is a judgment (that corresponds to a proposition). E.g., you can have a type: `data A = 1 | 2 | 3`, and `data B = 3 | 4 | 5`, but then testing `a < b` (assuming `a:A b:B`) may not be straightforward (depending on the language), while a spec of `A = {1, 2, 3}, B = {1, 2, 3}, a ∈ A, b ∈ B` does let you test `a < b`.

lomnakkus 10y ago
Types are propositions. See Curry-Howard.
- pron 10y ago
  Types encode propositions (see Curry-Howard) but are logical judgments in the language's logic. The expression `a:A` does not have a boolean truth value (like a logical proposition), but is rather a judgment. In my example above, the value of the expression `a ∈ B` is true iff a = 3 and false otherwise, but the expression `a:B` is just not a well-formed expression. In other words, you could create a type that corresponds to a proposition, but type assignment is distinct from a proposition (e.g. the proposition `b1 < b2`, assuming `b1,b2:B`) in the language. More precisely, you could say that types encode propositions at the type level (even if the language allows the same data-level syntax in type definitions, as in Idris), while propositions at the data level are distinct, while specs are data level propositions.
  - catnaroek 10y ago
    `x:T` is a typing judgment. A typing judgment is not a type, even if one of its constituent parts (`T`) is a type. What you call “data-level propositions” is really just “data-level abstract syntax representation of propositions”. Propositions really are types. (Though, of course, there are types that are not propositions.) And your example is simply not valid Haskell.
    - 10y ago