undefined | Better HN

0 pointsyogthos8y ago0 comments

A lot of the same refactoring is possible in dynamic languages as in static ones. I recommend reading up on Term to see what's possible to do with JavaScript http://marijnhaverbeke.nl/blog/tern.html

I use Cursive https://cursive-ide.com/ for working with Clojure, and it can do safe refactoring for symbols by doing static analysis of the source. It can show all usages of a symbol, rename it, do automatic imports, and so on.

Another piece of tooling that's not available in any statically typed languages at the moment is REPL integration with the editor seen here http://vvvvalvalval.github.io/posts/what-makes-a-good-repl.h...

I find that the REPL driven workflow found in Lisps is simply unmatched. When you have tight integration between the editor and the application runtime, you can run any code you write within the context of the application immediately. This means that you never have to keep a lot of context in your head when you're working with the application. You always know what the code is doing because you can always run and inspect it.

Having the runtime available during development gives you feedback much faster than the compile/run cycle. I write a function, and I can run it immediately within the context of my application. I can see exactly what it's doing and why.

The main cost of static typing is that it restricts the ways you can express yourself. You're limited to the set of statements that can be verified by the type checker. This is necessarily a subset of all valid statements you could make in a dynamic language.

Finally, dynamic languages use different approaches to provide specification that have different trade offs from static typing. For example, Clojure has Spec that's used to provide runtime contracts. Just like static typing, Spec provides a specification for what the function should be doing, and it can be used to help guide the solution as seen here https://www.anthony-galea.com/blog/post/hello-parking-garage...

Spec also allows trivially specifying properties that are either difficult or impossible to encode using most type systems. Consider the sort function as an example. The constraints I care about are the following: I want to know that the elements are in their sorted order, and that the same elements that were passed in as arguments are returned as the result.

Typing it to demonstrate semantic correctness is impossible using most type systems. However, I can trivially do a runtime verification for it using Spec:

    (s/def ::sortable (s/coll-of number?))

    (s/def ::sorted #(or (empty? %) (apply <= %)))

    (s/fdef mysort
            :args (s/cat :s ::sortable)
            :ret  ::sorted
            :fn   (fn [{:keys [args ret]}]
                    (and (= (count ret)
                            (-> args :s count))
                         (empty?
                          (difference
                           (-> args :s set)
                           (set ret))))))

The above code ensures that the function is doing exactly what was intended and provides me with a useful specification. Just like types I can use Spec to derive the solution, but unlike types I don't have to fight with it when I'm still not sure what the shape of the solution is going to be.

0 comments

rbobrowicz8y ago

For someone only passingly familiar with Spec, what's the benefit of Spec over just using a property based testing framework like Haskell's QuickCheck (and I think Clojure's test.check)?

I can encode all those invariants as QuickCheck properties and have them automatically tested against random inputs on every test run. It's still all runtime verification, but with random inputs I actually have more confidence of hitting a corner case than with just asserting during regular program runs or hand written example tests.

Also, with enough heavy lifting you can actually encode all of that in the types in a dependantly typed language like Idris [1]. And while a machine checked proof of your sorting algorithm is nice, it might be hitting the diminishing returns point the article mentions over just using property tests.

[1] https://github.com/davidfstr/idris-insertion-sort

sheepmullet8y ago

Think of QuickCheck/test.check but with better integration into the language.

This makes it much more likely to be used but it's fundamentally the same set of ideas.

A really cool idea I'm playing with at the moment is using fuzzing/static analysis based generators to feed spec/test.check.

I think it will help get past the, imo, biggest issue with generators in that they can miss exceptional cases in the code.

E.g. If (x=="jack and Jill) {exceptional case} is unlikely to be triggered with standard generators but "easy" for static analysis tools to solve.

> Also, with enough heavy lifting you can actually encode all of that in the types in a dependantly typed language like Idris [1]

In theory. In practice it is multiple orders of magnitude harder to prove properties in Idris than it is to spec them using property based testing.

yogthosOP8y ago

To add to what sheepmullet said, I think the insertion sort example is exactly the problem with advanced type systems. It takes nearly 300 lines of code to provide the specification.

Somebody has to be able to read that specification and understand that it's correct in a semantic sense. Ultimately, the specification itself becomes a full blown program that the type checker executes. So, now you run a program to try and verify aspects of your original program, but how do you verify that the specification itself is correct?

At some point a human has to be able to read the code and decide that it matches the intent. This step can't be automated, and I certainly don't think the Idris example improves things. I'd argue that it's far easier to tell that this version is correct:

    fun insertionSort(arr, int n)
    {
       var i, key, j;
       for (i = 1; i < n; i++)
       {
           key = arr[i];
           j = i-1;
           while (j >= 0 && arr[j] > key)
           {
               arr[j+1] = arr[j];
               j = j-1;
           }
           arr[j+1] = key;
       }
    }

j / k navigate · click thread line to collapse