Notes on Idris (2017)

doublec's ATS articles are probably the most accessible introduction: https://bluishcoder.co.nz/tags/ats/index.html

Other than that the documentation is very decent for a one-man research project. (I say "research project", and it is, but it has huge practical value as well.)

Still, I have very high hopes for ATS.

Isn't that a non-extensible built-in that's handled "magically" by the compiler? (Apologies if that's wrong, it's been a few years since I've used O'Caml.)

In Idris it's possible to write a type-safe printf entirely in library code -- no magic.

E.g. safe resource deallocaion problem can be seen as a dependent-type problem (only let an initialized resource into a deallocator), but is usually solved with sort-of linear types, or even simpler (though more crude) means.

The problem is that both their proponents and detractors (as well as those of other verification approaches) confuse research and practice. Think of the field as early stages of pharmaceutical research; experiments in the lab show some promise as well as obstacles, but it's too early to tell which of the approaches, if any, would be able to work at a large scale in field conditions. As long as we don't confuse research and practice we can follow, enjoy and evaluate research on its own terms, rather than judging it based on criteria that may not be relevant at this stage. This is not to say that we cannot point out risks to field adoption, but research is research.

I, too, have my doubts about dependent types, but it's unfair to judge them harshly at this stage, when nobody knows how best to use them.

We have that for Java, too: http://www.openjml.org/

The great thing about contracts (as opposed to dependent types) is that they separate specification from verification. You could use proofs (fully- or semi-automatic), but you could also use weaker but cheaper forms of verification, such as concolic tests or randomized tests, generated from the contracts, or, weaker still, runtime assertions. Dependent types tie specification to a specific form of verification (proof).

A standardized specification language like JML can (and does) have many tools offering different forms of verification.

Both are mature enough to be in use, but are limited primarily by the fact that both languages have manual memory management, which is well understood via separation logic, but poorly supported by the tools.

I've written some blog posts about Frama-C:

* https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search....

* https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch....

* https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quic...

* https://maniagnosis.crsr.net/2017/08/AFL-verifying-quicksort...

   f : () -> Type
   f =
     let r = ref 0 in
     fun () ->
       let t = if !r = 0 then Int else String in
       r := r + 1;
       r

   x : f ()
   x = 17

   y : f ()
   y = "foo"

(Of course, the place where C++ is limited is its inability to template over non-concrete values, but I see nothing about its model that fundamentally limits its ability to conceptualize such a thing. It is still technically a dependently typed language even without the ability to do this, of course.) [edit: matt-noonan has told me that I am wrong on that last comment :(... so not "of course".]

    #include <stdlib.h>
    
    template <size_t S, typename E>
    class Vect {
      private:
        E data[S];
    
      public:
        const size_t size() const {
            return S;
        }
    
        E &operator [](size_t i) {
            return data[i];
        }
    
        const E &operator [](size_t i) const {
            return data[i];
        }
    };
    
    template <size_t N, size_t M, typename E>
    Vect<N + M, E> append(const Vect<N, E> &l, const Vect<M, E> &r) {
        Vect<N + M, E> v;
        for (size_t i(0); i != N; ++i)
            v[i] = l[i];
        for (size_t i(0); i != M; ++i)
            v[N+i] = r[i];
        return v;
    }

    int main() {
        Vect<4, int> a;
        Vect<2, int> b;
        Vect<6, int> c = append(a, b);
        Vect<8, int> d = append(a, b);
        return 0;
    }

    test.cpp:36:18: error: no viable conversion from 'Vect<4UL + 2UL aka 6, [...]>' to 'Vect<8, [...]>'
        Vect<8, int> d = append(a, b);
                     ^   ~~~~~~~~~~~~
    test.cpp:4:7: note: candidate constructor (the implicit copy constructor) not viable: no known conversion from 'Vect<4UL + 2UL, int>' to
          'const Vect<8, int> &' for 1st argument
    class Vect {
          ^
    1 error generated.

https://wiki.haskell.org/Liquid_Haskell

    template <typename T, int N> struct vec { T data[N]; };
    vec<T,n> repeat(int n, T const& x) {...}

Sometimes it feels like a kludge, but then I get to enjoy the nice IDEs, libraries that it has.

If only C++ had proper pattern matching support.

Of course, it isn't the only language I play with.

The only issue is that the language server seems to have a memory leak or something that leads to it taking a huge amount of memory and getting sluggish over the course of an extended development session.

Some loose thoughts that may or may not make sense:

- In Haskell, effectful computations (such as prints, variable updates, and so on) are first-class values (like integers, strings, and so on). This is the big idea.

- When effectful computations are first-class values, you can store them in data structures like lists. You can associate them with keys in maps. You can even stick them in priority queues.

- When effectful computations are first-class values, you can pass them around as arguments, or send them off as return values.

- When effectful computations are first-class values, you can transform their results, you can chain them together and you can create branches in them.

- When effectful computations are first-class values, you can perform them, then perform then again, then perform them 12 times, then discard them. Or discard them first and never perform them.

- When effectful computations are first-class values, you have decoupled "describing the action" from "executing the action". You can handle the effectful computation without being afraid of performing the effect.

- When description is decoupled from execution, you can abstract over the flow of control. You can have a loop that doesn't always increment its counter, because the incrementing operation is specified in a list somewhere instead.

- Abstracting over the flow of control can be about as confusing as it is dynamic and powerful. It can also be the most clear and obvious solution to some problems.

- Effectful computations as first-class values is a little like functions as first-class values: when you have tried it, you've found it's so convenient that you'd like to have it everywhere. (It's also a little like first-class functions in the sense that you can emulate first-class effects with first-class functions, but it easily becomes unwieldy.)

- Effectful computations as first-class values is even a little like Lisp metaprogramming. In Lisp, the flow of control can be rewired dynamically, because the code itself is a Lisp data structure. In Haskell, the flow of control can be rewired dynamically, because statements don't have to be executed the second you see them.

- The do notation, when used the traditional way, pulls a curtain over how effectful computations are first-class values. Computations in do notation are (to a first approximation) executed as soon as they are seen, because do notation was designed to intentionally hide the ways in which Haskell is a more powerful imperative language.

Sorry if that made things even more confusing than it cleared up.

----

Here's the most basic concrete example I can think of:

    repeated = do {
        putStrLn "Hello";
        putStrLn "Hello";
    }

    somewhatDRY = do {
        let greet = putStrLn "Hello";  -- not executed when put into variable
        greet;                         -- executed once here
        greet;                         -- and again here
    }

    countGreetings number = do {
        let greetings =                     -- infinite list of prints,
                repeat (putStrLn "Hello");  -- none of which is executed
        let enough =                        -- we take the first few prints,
                take number greetings;      -- still without executing any
        sequenceA_ enough;                  -- now we execute just the first ones
    }

    countGreetings number =
        let
            greetings = repeat (putStrLn "Hello")
            enough = take number greetings
        in
            sequenceA_ enough

In these examples I used sequenceA_, which is a plain library function that takes a list of effectful computations and returns a single effectful computation. The effect of the returned computation is the same as if all the effectful computations in the list was called one after the other.

I mention it's a plain library function because you wouldn't be able to define such a function – not even in the standard library – if effectful computations weren't first-class values...

----

I wrote a comment in the example saying "now we execute just the first ones". That's a lie, actually. Because like any effectful computation, also the return value of countGreetings is a first-class value. Meaning we could assign the return value of countGreetings to a variable, or stick it in a list, and so on, and nothing would be executed.

In order to avoid uncomfortable déjà vu, I'll In order to avoid uncomfortable déjà vu, I'll just leave off here and conclude that when effectful computations are first-class values, there is, in a sense, two phases when the code is run. First there's an evaluation phase, where effectful computations are constructed and passed around. Then there's an execution phase, which actually executes these effects. If your effectful computation isn't hit by the execution phase, it will never be executed – no matter how many times the evaluation phase goes over it.