Notes on Idris (2017)(thebreakfastpost.com)

   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"

    #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.

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

    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