3 ms·

You can make a breaking change without changing the type signature ("do_something now uppercases and reverses the input string before using it"), and you can ch

by djur 3y ago

You can make a breaking change without changing the type signature ("do_something now uppercases and reverses the input string before using it"), and you can change the type signature without making a breaking change ("do_something now accepts None and treats it equivalently to an empty string"). The author is conflating these two scenarios.

actionfromafar 3y ago
Someone is also sitting on the sidelines, snickering about how primitive the types and function signatures must be for that to happpen.
- anonymoushn 3y ago
  Do you know of a language that encodes whether a function has the capability to make a reversed uppercased copy of a string in the type of the function?
  - RedNifre 3y ago
    Maybe Idris or Blodwen. Idris can at least define a printf function where the string must contain the right template, i.e. printf("number %i text %s", 5, "hey") compiles, but printf("number %s text %s", 5, "hey") does not, so I'm not sure it's impossible to encode string reversal in the type signature.
    - deredede 3y ago
      You really don't need dependent types to do the printf thing, any language with GADTs or equivalent typing functionality can do it, see for instance OCaml's Printf module. Although you do need a little bit of magic from the compiler to get that exact syntax, which you can get rid of with dependent types.
  - codebje 3y ago
    Dafny and Whiley are two examples with explicit verification support. Idris and other dependently typed languages should all be rich enough to express the required predicate but might not necessarily be able to accept a reasonable implementation as proof. Isabelle, Lean, Coq, and other theorem provers definitely can express the capability but aren't going to churn out much in the way of executable programs; they're more useful to guide an implementation in a more practical functional language but then the proof is separated from the implementation, and you could also use tools like TLA+. https://dafny.org/ https://dafny.org/ https://whiley.org/ https://whiley.org/ https://www.idris-lang.org/ https://www.idris-lang.org/ https://isabelle.in.tum.de/ https://isabelle.in.tum.de/ https://leanprover.github.io/ https://leanprover.github.io/ https://coq.inria.fr/ https://coq.inria.fr/ http://lamport.azurewebsites.net/tla/tla.html http://lamport.azurewebsites.net/tla/tla.html

by djur 3y ago

actionfromafar 3y ago

Someone is also sitting on the sidelines, snickering about how primitive the types and function signatures must be for that to happpen.

anonymoushn 3y ago
Do you know of a language that encodes whether a function has the capability to make a reversed uppercased copy of a string in the type of the function?
- RedNifre 3y ago
  Maybe Idris or Blodwen. Idris can at least define a printf function where the string must contain the right template, i.e. printf("number %i text %s", 5, "hey") compiles, but printf("number %s text %s", 5, "hey") does not, so I'm not sure it's impossible to encode string reversal in the type signature.
  - deredede 3y ago
    You really don't need dependent types to do the printf thing, any language with GADTs or equivalent typing functionality can do it, see for instance OCaml's Printf module. Although you do need a little bit of magic from the compiler to get that exact syntax, which you can get rid of with dependent types.
- codebje 3y ago
  Dafny and Whiley are two examples with explicit verification support. Idris and other dependently typed languages should all be rich enough to express the required predicate but might not necessarily be able to accept a reasonable implementation as proof. Isabelle, Lean, Coq, and other theorem provers definitely can express the capability but aren't going to churn out much in the way of executable programs; they're more useful to guide an implementation in a more practical functional language but then the proof is separated from the implementation, and you could also use tools like TLA+. https://dafny.org/ https://dafny.org/ https://whiley.org/ https://whiley.org/ https://www.idris-lang.org/ https://www.idris-lang.org/ https://isabelle.in.tum.de/ https://isabelle.in.tum.de/ https://leanprover.github.io/ https://leanprover.github.io/ https://coq.inria.fr/ https://coq.inria.fr/ http://lamport.azurewebsites.net/tla/tla.html http://lamport.azurewebsites.net/tla/tla.html