Здравствуйте, Воронков Василий, Вы писали:

ВВ>Запишешь мне какой будет тип у такой функции?

ВВ>

ВВ>let out x = write x $ out
ВВ>

ВВ>Аналог на ДжаваСкрипте:

ВВ>

ВВ>function out (x) {
ВВ>   write(x);
ВВ>   return out;
ВВ>}
ВВ>

ВВ>Когда закончишь — позови.

  Out[T](x : T) : T // T -> T
  {
    Write(x);
    x
  }

Здравствуйте, VladD2, Вы писали:

ВВ>>Аналог на ДжаваСкрипте:

ВВ>>

ВВ>>function out (x) {
ВВ>>   write(x);
ВВ>>   return out;
ВВ>>}
ВВ>>

ВВ>>Когда закончишь — позови.
VD>

VD>  Out[T](x : T) : T // T -> T
VD>  {
VD>    Write(x);
VD>    x
VD>  }
VD>

не оно. Надо вернуть не аргумент, а саму функцию

Здравствуйте, VladD2, Вы писали:

ВВ>>Когда закончишь — позови.
VD>

VD>  Out[T](x : T) : T // T -> T
VD>  {
VD>    Write(x);
VD>    x
VD>  }
VD>

Неа. Там рекурсивный тип. Точный аналог на Nemerle записать можно только так:

    def o(x)
    {
      Write(x);
      o
    }
    _ = o(1)(2)(3);

Компилятор же на это расскажет про циклический тип

Здравствуйте, hardcase, Вы писали:

H>Неа. Там рекурсивный тип. Точный аналог на Nemerle записать можно только так:
H>

H>    def o(x)
H>    {
H>      Write(x);
H>      o
H>    }
H>    _ = o(1)(2)(3);
H>

H>Компилятор же на это расскажет про циклический тип

А какой практический смысл этой хрени? По обсуждать в Философии?

Здравствуйте, Воронков Василий, Вы писали:

ВВ>+ Полиморфные варианты, все конструкторы которых к единой хербрандовой вселенной

Всё-таки Эрбрановой. В честь Жака Эрбрана.

Здравствуйте, Воронков Василий, Вы писали:

Да простит меня топикстартер, попробую изложить свою версию.

let foo x = if x==0 then 0 else "hi"
foo :: int -> int | string

Ф-я возвращает анонимный АТД. Чтобы выцепить само значение, требуется сделать матчинг с обоими вхождениями, что необходимо для обеспечения типобезопасности.
Различать int|string и string|int смысла не имеет.

Перегрузка функций:

let bar x = x + 1
bar :: int -> int
let bar x = x + "\n"
bar :: string -> string

Обнаружив такую перегрузку компилятор должен позволить вызвать функцию bar с аргументом int|string. Ее результатом будет опять-таки int|string.
Кроме того, если на момент компиляции фактический тип x известен, то тип результата может быть выведен более точно:

let z1 = bar 1
z1 :: int
let z2 = bar "hi"
z2 :: string

Аналогично, если ф-я bar задана для класса типов (например Num):

bar :: (Num a) => a -> a
let bar x = x * x

, то ее можно вызвать для, например, int|double и получить int|double. Но если "точный" тип параметра известен, то и тип результата можно вывести поточнее.

Вернемся к foo:

let z1 = foo 0
let z2 = foo 1

Какие типы у z1 и z2? Если определение foo известно на момент компиляции, то компилятор может вывести, что

z1 :: int
z2 :: string

И матчинга для них уже не потребуется.
Фактически, это эквивалентно тому, что компилятор переписывает foo во что-то подобное:

let foo 0 = 0
let foo x {where x != 0} = "hi"

и дальше поступает по аналогии с перегрузками bar.

По большому счету, определение foo может и не потребоваться в момент его вызова, если в момент компиляции foo компилятор добавляет необходимую метаинформацию о зависимости типа результата от значений (и типов) параметров. Если полный анализ ее кода не возможен или слишком сложен то он, возмозно, даже и не нужен — достаточно сделать подсказки для подмножества случаев, которые видны компилятору "невооруженным взглядом".

ВВ>Системы типов консервативны, они не пытаются доказать правильность программы, они доказывают ее возможную неправильность. Код вида foo x * foo y возможно неправильный (но частный случай foo 0 * foo 0 — правильный). Исходя из того, что выражение foo x * foo y в принципе может быть неправильным, система типов этот код не пропустит.

Допустим, для строк и целых определен оператор +.

let f x y = foo x + foo y
f :: int -> int -> int|string

тут возможны, по крайней мере, такие варианты:
1. Статическая система типов определение такой ф-ии не пропустит, т.к. int+string не определен.
2. Система типов ее пропустит. В рантайме будет кидаться что-то вроде NotImplementedException для f 0 1, f 1 0 и т.п. Возникает вопрос о "статичности" этой системы.
3. Компилятор сгенерирует code contract для этой ф-ии и будет его статически проверять и не давать вызвать эту ф-ю, пока ему не докажешь, что (x==0 && y==0)||(x!=0 && y!=0). Все статически типизированно.



В принципе, перегрузка ф-ий не дружит с каррингом. Можно попробовать побороть опять таки использованием таких анонимных АТД. Например,

f :: a -> a
let f x = x
f :: a -> b -> b
let f x y = y

//Результат:
f :: a -> a|(b->b)

и, на основании контекста, выводить, какую реализацию вызывать. Плюс придумать синтаксис для разрешения неоднозначностей, если возникнут.

ВВ>Есть два варианта:
ВВ>+ Функция, тип которой зависит от [типа] параметров
ВВ>+ Функция, тип которой зависит от значений параметров

ВВ>Первый вариант в статике возможен:
ВВ>printf "%d+%d=%d" 2 2 (2+2)

ВВ>Второй — нет:
ВВ>let myPrint fmt = printf fmt ...?

Не очень понятно. Возможно, имеется ввиду такой случай:

let myPrint fmt = \... -> printf fmt ...

Т.е. в зависимости от значения fmt тип "myPrint fmt" будет разный:
для "%d": int -> ()
для "%d%s": int -> string -> ()
так?

Если fmt статически известен, то вывести можно сразу. Если нет, то придется, видимо, мудрить с рекурсивными типами (что-то вроде type UniversalFuncType = a->() | b->UniversalFuncType) и матчить.
В принципе, если формат приходит не извне (пользовательский ввод, файл и т.п.), а формируется в коде, то компилятор кое-какую дополнительную информацию может и получить.
Эх, доберусь я до зависимых типов иии...

Здравствуйте, VladD2, Вы писали:


ВВ>>Когда закончишь — позови.
VD>

VD>  Out[T](x : T) : T // T -> T
VD>  {
VD>    Write(x);
VD>    x
VD>  }
VD>

Это совсем не то

Здравствуйте, VladD2, Вы писали:

H>>Компилятор же на это расскажет про циклический тип
VD>А какой практический смысл этой хрени? По обсуждать в Философии?

Например, Y-комбинатор:

\f -> (\x -> f (x x)) (\x -> f (x x))

Кстати, out в его обобщенном варианте rec:

let rec f x = f x $ rec f

достаточно полезен. Можно, к примеру писать так:

rec writen "Line1" "Line2"

Вместо:

writen "Line1" $ writen "Line2"

Здравствуйте, Воронков Василий, Вы писали:

ВВ>Например, Y-комбинатор:

ВВ>

ВВ>\f -> (\x -> f (x x)) (\x -> f (x x))
ВВ>

И на фиг он уперся в реальной то работе?

ВВ>Кстати, out в его обобщенном варианте rec:

ВВ>

ВВ>let rec f x = f x $ rec f
ВВ>

ВВ>достаточно полезен.

На фиг он не уперся. Просто ты совсем зафилосовствовался. А есть еще такой не маловажный принцип дизайна как простота.

ВВ>Можно, к примеру писать так:

ВВ>

ВВ>rec writen "Line1" "Line2"
ВВ>

ВВ>Вместо:

ВВ>

ВВ>writen "Line1" $ writen "Line2"
ВВ>

А можно писать так:

writen("Line1\nLine2")

или так

writen("Line1", "Line2")

или так

writen("Line1");
writen("Line2");

Для решаемой задачи это ровным счетом ничего не изменит. Так что по принципу бритвы Оккама — в топку.

Здравствуйте, VladD2, Вы писали:

ВВ>>

ВВ>>\f -> (\x -> f (x x)) (\x -> f (x x))
ВВ>>

VD>И на фиг он уперся в реальной то работе?

Что ты называешь "реальной работой"? Мейнстрим что ли?
Я вот вас не понимаю, честно говоря. Лямбда-исчисление вам в "реальной работе" не требуется, а вот без макросов никуда, да.

Большинству в "реальной работе" ну нужны ни ФП, ни МП, ни прочие страшные буквы. И что теперь, на бейсике писать?

ВВ>>Кстати, out в его обобщенном варианте rec:
ВВ>>

ВВ>>let rec f x = f x $ rec f
ВВ>>

ВВ>>достаточно полезен.
VD>На фиг он не уперся. Просто ты совсем зафилосовствовался. А есть еще такой не маловажный принцип дизайна как простота.

Простота чего? Системы типов? Не уверен, что это плюс. Как можно одновременно затаптывать динамику и ратовать за простую систему типов? Которая сгодится только факториалы писать.
Или речь о простоте языка? Так куда уж проще-то. Есть функции, все функции принимают один аргумент, есть операция применения функции. Все.

Здравствуйте, Воронков Василий, Вы писали:

ВВ>Что ты называешь "реальной работой"? Мейнстрим что ли?

Написание кода для решения реальных задач.

ВВ>Я вот вас не понимаю, честно говоря. Лямбда-исчисление вам в "реальной работе" не требуется, а вот без макросов никуда, да.

Лямбда-исчисления не требуются (это теория), а лямбды полезны... а Y-комбинаторы бесполезны. Единственное где я их видел — это тесты компиляторов. Слышал что в C# особо извращенные товарищи решают ими проблему отсутствия локальных функций (объявляют рекурсивную функцию по месту).

ВВ>Большинству в "реальной работе" ну нужны ни ФП, ни МП, ни прочие страшные буквы. И что теперь, на бейсике писать?

Это неверная постановка вопроса. Они не ненужные, а неизвестны и потому не применяются. А вот о существовании Y-комбинаторов многим известно. Но применять их на практике смысла нет. Это не более чем забавное проявление теории.

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

Что касается Y-комбинаторов, то они как бы даются в нагрузку за поддержку лямбд. Ничего специально делать для их появления не надо.

А вот то о чем ты говоришь требует. Но бенефитов от этого пока не видно. Так стоит ли вводить новую сущность, если в ней нет необходимости?

ВВ>Простота чего? Системы типов?

Простота языка. Система типов — это его часть.

ВВ>Не уверен, что это плюс. Как можно одновременно затаптывать динамику и ратовать за простую систему типов?

Важно иметь возможность решать реальные пробелмы. Если есть приемлемые средства решения проблемы, то еще одного способа ее решить не нужно.

ВВ>Которая сгодится только факториалы писать.
ВВ>Или речь о простоте языка? Так куда уж проще-то. Есть функции, все функции принимают один аргумент, есть операция применения функции. Все.

Ну, как видишь не очень то все просто. Уж лучше оперировать object-ом, чем усложнять систему типов ради прикольной безделицы.

Скажем так. Я понимаю что может дать зависимые или уникальные типы. Не уверен, что то что они дадут оправдает усложнение языка, но все же понимаю. Тут же я пока что не понимаю зачем это нужно. Если разумный объяснений не найдется, то я буду склонен считать, что исключительно для пенесометрии.

Здравствуйте, deniok, Вы писали:

D>Лямбды забыл спереди
D>

D>\f g h -> f `mapSum` g `mapSum` h :: (a1 -> b1) -> (a2 -> b2) -> (a3 -> b3) -> a1 | a2 | a3 -> b1 | b2 | b3
D>

D>но идея ясна.

Кабздец! И потом люди спрашивают почему мало кто хочет писать на хаскеле.

Здравствуйте, maxkar, Вы писали:

M>

M>const f : Function = function(a : int, b : int = 3) : int {
M>  return a + b;
M>}
M>f(3);
M>f(5, 6);
M>

Что это за язык?

Здравствуйте, maxkar, Вы писали:

M>Вот что-то в подобном роде используется в реальном коде. Обработчики 'about-dialog', 'format-drive-dialog' и т.п. могут находиться в различных подгружаемых модулях, описываются в конфиге.

Программирование на конфигах? А ради чего?

Здравствуйте, Воронков Василий, Вы писали:

ВВ>Более практической задачей был — "динамический" ML-ный printf, для которого строку формата можно формировать в рантайме.

А список параметров ты тоже в рантайме формировать будешь?

Здравствуйте, Воронков Василий, Вы писали:

ВВ>Ну так тип единственного параметра printf и вычисляется в компайл-тайме на основе *значения* строки формата.

В нормальных языках вывод типов может быть произведен и без строки формата. А вот в выводе типов по строке формата смысла нет. Вообще нет!

Ну, а написать код который возьмет типы параметров и по ним построить динамическую проверку строки формата задача не сложная.

Здравствуйте, FR, Вы писали:

FR>>>То есть никакого вывода возвращаемого значения, его тип заранее жестко задан?
D>>Что мешает ему быть выведеным? Выкидываем имя X, и возвращаемся к первому примеру.
D>>let foo x = if x == 0 then 0 else "bar" end
D>>foo :: int -> int | string

FR>Тогда мы получаем разновидность того, что в OCaml называется полиморфный вариант http://www.rsdn.ru/forum/philosophy/4251507.1.aspx

Автор: FR
Дата: 27.04.11

FR>Он по сути ослабляет статическую типизацию http://www.rsdn.ru/forum/decl/4032286.flat.aspx

Автор: Воронков Василий
Дата: 10.11.10

Думаю, что он имеет в виду другое. Он видимо имеет в виду вывод безымянного АлгТД по использованию внутри функции. При наличии функции генератора и функции потребителя соответствие типов можно будет проверить явно.

В Окамле же речь, как я понимаю, идет об одном, большом, расширяемомо АлгТД расширяемость которого и ослабляет типизацию.

Здравствуйте, VladD2, Вы писали:

ВВ>>Ну так тип единственного параметра printf и вычисляется в компайл-тайме на основе *значения* строки формата.
VD>В нормальных языках вывод типов может быть произведен и без строки формата. А вот в выводе типов по строке формата смысла нет. Вообще нет!
VD>Ну, а написать код который возьмет типы параметров и по ним построить динамическую проверку строки формата задача не сложная.

Замени "нормальные языки" на "Си-подобные". Выводить по типу параметров можно, если функция принимает несколько параметров. Если в языке вообще нет средств для объявления функций, принимающих несколько параметров, то вывод по формату — единственный по сути вариант. Некрасивость здесь только в том, что формат выглядит как строка, но на самом деле это не строка. А из-за этого возникает та же проблема, что и с $-строками в Немерле — даже в ресурсник не положишь.

Здравствуйте, VladD2, Вы писали:

ВВ>>Более практической задачей был — "динамический" ML-ный printf, для которого строку формата можно формировать в рантайме.
VD>А список параметров ты тоже в рантайме формировать будешь?

А списка параметров и нет. По сути есть лишь последовательные вызовы функции. Ты можешь вызвать функцию так: printf(x)(y) а можешь так: printf(x)(y)(z) — и в обоих случаях произойдет сатурация. Потребуется ли тебе вызвать функцию еще раз или не потребуется — вполне может определяться в рантайме.

Здравствуйте, VladD2, Вы писали:

ВВ>>Что ты называешь "реальной работой"? Мейнстрим что ли?
VD>Написание кода для решения реальных задач.

Реальной задачей может быть и разработка системы исчисления на основе парочки комбинаторов. Или доказательство теорем. Или написание примерчиков для rosettacode. Так что define "реальная".
Для большинства "реальные задачи" с разработкой компиляторов и веб-фреймворков тоже не связаны.

ВВ>>Я вот вас не понимаю, честно говоря. Лямбда-исчисление вам в "реальной работе" не требуется, а вот без макросов никуда, да.
VD>Лямбда-исчисления не требуются (это теория), а лямбды полезны... а Y-комбинаторы бесполезны.

Вот эту фразу я вообще не понимаю. Быть может, есть какие-то другие комбинаторы, которые ты считаешь полезными? Или что ты называешь "лямбдами"?

ВВ>>Большинству в "реальной работе" ну нужны ни ФП, ни МП, ни прочие страшные буквы. И что теперь, на бейсике писать?
VD>Это неверная постановка вопроса. Они не ненужные, а неизвестны и потому не применяются. А вот о существовании Y-комбинаторов многим известно. Но применять их на практике смысла нет. Это не более чем забавное проявление теории.

Ага, а еще одним забавным проявлением теории являются системы типов, в основании которых лежит типизированное лямбда-исчисление.

VD>В общем, чтобы фича применялась мало ее придумать и реализовать. Недостаточно даже если фича будет круто выглядеть. Нужно еще чтобы она была нужна на практике. Если она на практике ничего не дает, то и фича эта не нужна.
VD>Что касается Y-комбинаторов, то они как бы даются в нагрузку за поддержку лямбд. Ничего специально делать для их появления не надо.

(Я понял, тебе не нравятся Y-комбинаторы. Приведи тогда три своих любимых комбинатора, их и обсудим).
По существу — в рамках нетипизированного лямбда-исчисления делать ничего не надо. В рамках типизированного — чтобы записать его именно так, как я, а не через жопу, как это обычно делается, должна быть поддержа эквирекурсивных типов, о чем мы, собственно, тут и говорим.

VD>А вот то о чем ты говоришь требует. Но бенефитов от этого пока не видно. Так стоит ли вводить новую сущность, если в ней нет необходимости?

А я никого не убежаю что-то вводить. К тому же сделать это, подозреваю, весьма непросто. Речь всего лишь о том, что реальные, а не сферические, системы типов все же весьма ограничены, и динамика, которая позволяет записывать все as is, как оно и выглядит в "учебниках", часто смотрится на их фоне весьма выгодно.

Что до полезности. Ну я сталкивался с необходимости циклических типов при программировании в CPS-стиле. Да, в принципе их отсутствие как-то обходится, но код выглядит менее наглядно и замусоривается.

ВВ>>Простота чего? Системы типов?
VD>Простота языка. Система типов — это его часть.

Сложное утверждение на самом деле. Вот положим есть язык — Хаскель. Хаскель поддерживает higher-rank polymorphism. А есть система типов Хаскеля. В ней higher-rank polymorphism является undecidable.

ВВ>>Не уверен, что это плюс. Как можно одновременно затаптывать динамику и ратовать за простую систему типов?
VD>Важно иметь возможность решать реальные пробелмы. Если есть приемлемые средства решения проблемы, то еще одного способа ее решить не нужно.

Все это слишком общие понятия, чтобы ими оперировать. Что такое "реальные проблемы", какие средства мы считаем "приемлимыми", а какие — нет? Это все весьма субьективно.
Вот перечисли три реальные проблемы, которые ты решал последнее время. В ответ — перечислю свои (те, за которые деньги платят, а не "для души").

ВВ>>Которая сгодится только факториалы писать.
ВВ>>Или речь о простоте языка? Так куда уж проще-то. Есть функции, все функции принимают один аргумент, есть операция применения функции. Все.
VD>Ну, как видишь не очень то все просто. Уж лучше оперировать object-ом, чем усложнять систему типов ради прикольной безделицы.

В рамках untyped lambda calculus, которая, как говорится, есть отец и матерь, все действительно именно так просто. Функции, применение функций — больше ничего не надо. А вот в рамках typed...

VD>Скажем так. Я понимаю что может дать зависимые или уникальные типы. Не уверен, что то что они дадут оправдает усложнение языка, но все же понимаю. Тут же я пока что не понимаю зачем это нужно. Если разумный объяснений не найдется, то я буду склонен считать, что исключительно для пенесометрии.

Ну по крайней мере заметен прогресс. Раньше ты говорил, что зависимые типы не нужны, ибо есть макросы, и все это можно и нужно делать на макросах. Теперь ты видишь пользу, но усложнение языка считаешь неоправданным. Что ж, остался еще один шаг