fun (x::xs) = fun' x xs
                where fun' a [] = \y -> y + a
                      fun' a (x::xs) = \y -> fun' (y + a + x) xs

saturate x f = if f is Fun then saturate x (f x) else f

process [] = []
process [x] = [x]
process (x::xs) = saturate x (fun xs) :: process xs

process [1..10]

saturate : (n:Nat) -> Int -> sumType n -> Int
saturate Z x f = f
saturate (S k) x f = saturate k x (f x)

process : List Int -> List Int
process [] = []
process [x] = [x]
process (x::xs) = saturate (length xs) x (fun xs) :: process xs

Type checking .\add.idr
*add> process [1..10]
[63,68,70,69,65,58,48,35,19,10] : List Int

fun : (xs : List Int) -> sumType (length xs)
fun xs = adder (length xs) (sum xs)

saturate : (n:Nat) -> Int -> sumType n -> Int
saturate Z x f = f
saturate (S k) x f = saturate k x (f x)

convertArgs : List String -> List Int
convertArgs [] = []
convertArgs (x::xs) = map cast xs

main : IO ()
main = do 
  as <- getArgs
  let xs = convertArgs as
  let f = fun xs                      -- вот тут тип f зависит от длины прочитанного списка
  print $ saturate (length xs) 100 f  -- но это не проблема

add.idr:35:When elaborating right hand side of main:
Can't unify
        sumType (Prelude.List.length xs)
with
        sumType (Prelude.List.length xs + 1)

fun [1..arg] 1 2 3

DM>>Не правда. Зависимые типы реально зависят от рантайм значений. И делают это статически. Такой вот коан.

module Main
import System

myType : Bool -> Type  -- тип, зависящий от значения
myType False = Int
myType True = String

create : (n:Bool) -> myType n   -- создадим значение, тип которого зависит от переданного аргумента
create False = 22
create True = "zebra"

useValue : (p:Bool) -> myType p -> String  -- тип второго аргумента зависит от рантайм значения первого
useValue False v = show $ 20 + v           -- если это инт, складываем с 20 и переводим в строку
useValue True v = "a " ++ v                -- если это строка, склеиваем с другой строкой

main : IO ()
main = do
  args <- getArgs          -- читаем аргументы командной строки, рантайм значение
  let p = length args > 1  -- передано ли что-то? рантайм значение
  let v = create p         -- тип v зависит от рантайм значения p, это или Int или String 
  print $ useValue p v     -- передаем значение типа, который мы не знаем статически, но точно можем обработать все равно

DM>>>Не правда. Зависимые типы реально зависят от рантайм значений. И делают это статически. Такой вот коан.

DM>module Main
DM>import System

DM>myType : Bool -> Type  -- тип, зависящий от значения
DM>myType False = Int
DM>myType True = String

DM>create : (n:Bool) -> myType n   -- создадим значение, тип которого зависит от переданного аргумента
DM>create False = 22
DM>create True = "zebra"

DM>useValue : (p:Bool) -> myType p -> String  -- тип второго аргумента зависит от рантайм значения первого
DM>useValue False v = show $ 20 + v           -- если это инт, складываем с 20 и переводим в строку
DM>useValue True v = "a " ++ v                -- если это строка, склеиваем с другой строкой

DM>main : IO ()
DM>main = do
DM>  args <- getArgs          -- читаем аргументы командной строки, рантайм значение
DM>  let p = length args > 1  -- передано ли что-то? рантайм значение
DM>  let v = create p         -- тип v зависит от рантайм значения p, это или Int или String 
DM>  print $ useValue p v     -- передаем значение типа, который мы не знаем статически, но точно можем обработать все равно
DM>

open core monad io

calc max acc n 
  | x < max = calc max x
  | else = Some x
  where x = n + acc

iterate f = do
  putStrLn "Need value:"
  x <- readAny
  match f x with
        Some x = mkIO x
        x = iterate x

do
  putStrLn "Max:"
  max <- readAny
  x <- iterate $ calc max 0
  putStrLn $ show x

Running module test3

Max:
42
Need value:
29
Need value:
11
Need value:
123
163

Session ended. Session taken: 00:00:08.4393606

f = fun [1,2,3]
f 1 2 3
//Вывод:
//12

В языке со статической типизацией данный код был бы невозможен, так как длина списка неизвестна нам на этапе компиляции, а следовательно, мы не можем определить, сколько именно аргументов будет у функции, которую возвращает fun.

#include <initializer_list>
#include <iostream>
#include <cstddef>
#include <cassert>
#include <vector>
using namespace std;

struct Variadic
{
    size_t n;
    template<typename ...Args>
    void operator()(Args ...args)
    {
        assert(n == sizeof...(args) );
    }
};

Variadic fun(vector<int> x)
{
    return {x.size()};
}

int main()
{
    vector<int> x{1,2,3};
    fun(x)(1,2,3); // Runtime OK
    cout << "OK" << endl;
    fun(x)(1); // assert fail
}

Ответ прост. Мы считаем ее чистой, потому что списки в функциональных языках сравниваются не ссылочно (как, к примеру, массивы в C#), а структурно. Поэтому результаты двух вызовов этой функции эквивалентны, что несложно проверить в GHCi:

Вовсе нет. Давайте представим, что массивы в C# сравниваются именно структурно. Таким образом, два массива с одинаковым набором элементов будут считаться равными. И тогда мы сможем написать такой код:

var arr1 = new int[] { 1,2,3 };
var arr2 = new int[] { 1,2,3 };

if (arr1 == arr2)
  Console.WriteLine("arr1 и arr2 это один и тот же массив.");

arr1[0] = 10;

if (arr1 != arr2)
  Console.WriteLine("arr1 и arr2 это разные массивы.");

В результате выведется:

arr1 и arr2 это один и тот же массив.
arr1 и arr2 это разные массивы.

Как же так? Мгновение назад массивы были одинаковыми, а теперь они разные?

Как вы понимаете, во всем виновата «изменчивая природа» массивов. Так как вы можете поменять значения «по месту» (в отличие от связных списков в Хаскелле, любая операция над которыми приводит к созданию нового списка), то структурная эквивалентность уже не годится.

double sin(double);
// ...
auto &&x = sin(0.0);
x = 0.11;

[...]
Definition: Two objects are equal if their corresponding parts are equal (applied recursively), including remote parts (but not comparing their addresses), excluding inessential components, and excluding components which identify related objects.
Once we have identified the parts of an object which must be tested for equality, we know from the earlier discussion that at least those parts must be copied by copy constructors or assignment operators. In particular, these operators must make copies of remote parts, rather than simply copying the pointers to them.
Now let us return to part of the logicians’ definition of equality. Recall that we would like the following statement to be true:

x == y ⇒ ∀ “reasonable” function foo, foo(x)==foo(y)

It is necessary to limit our expectations to some subset of possible functions foo.
For instance, this statement will not hold for the “address-of” function applied to distinct objects with equal values, nor will it hold for any other function which distinguishes between individual objects rather than between their values.
Considering an example will demonstrate some of the challenges facing a designer of generic components.
[...]

К тому же в большинстве популярных объектно-ориентированных языков, включая C#, понятие алгебраический тип попросту отсутствует.

#include <boost/variant.hpp>
#include <iostream>
#include <ostream>

using namespace std;
using namespace boost;


struct Cellphone { bool touch_screen; };
struct Laptop { double screen_size; };

typedef variant<Cellphone, Laptop> Product;

struct Print: static_visitor<>
{
    void operator()(const Cellphone &x) const
    {
        cout << "Cellphone, touch_screen:" << x.touch_screen << endl;
    }
    void operator()(const Laptop &x) const
    {
        cout << "Laptop, screen_size:" << x.screen_size << endl;
    }
};

int main()
{
    Cellphone phone = {true};
    Laptop laptop = {11.1};
    
    Product x = phone;
    apply_visitor(Print(), x);
    x = laptop;
    apply_visitor(Print(), x);
}

variant<ConcreteClass1, ConcreteClass2, function<void()>, unique_ptr<IAbstract>> x;

useValue : (p:Bool) -> myType p -> String  -- тип второго аргумента зависит от рантайм значения первого
useValue False v = show $ 20 + v           -- если это инт, складываем с 20 и переводим в строку
useValue True v = "a " ++ v                -- если это строка, склеиваем с другой строкой

  let p = length args > 1  -- передано ли что-то? рантайм значение
  let v = create p         -- тип v зависит от рантайм значения p, это или Int или String 
  print $ useValue p v     -- передаем значение типа, который мы не знаем статически, но точно можем обработать все равно

ВВ>Здесь нет зависимости от рантайм значений, ведь эта программа доказывается статически. "Доказывается статически" означает, что возможный диапазон значений нам известен в компайл тайм, и мы можем доказать, что ни при каких случаях не выйдем из этого диапазона. Откуда здесь взяться зависимости от рантайма? Тут ее нет

BB>А для того, чтобы программа была доказуема статически, ее нужно свести к набору значений, который известен уже в период компиляции. Никаких "нежданчиков" там быть не может. Так что это, мягко говоря, не одно и то же

a = \x -> 2 * x
b = \x -> 2 * x
c = \x -> x * 2
d = \x -> a x
e = \x -> x + x

has55 :: [Maybe Int] -> Bool
has55 [] = False
has55 (Just 5 : Just 5 : rest) = True
has55 (_ : rest) = has55 rest