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

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

ВВ>>Что как бы не исключает вышесказанного. Хаскелл, о котором в процитированном вами сообщении, речи вообще не шло, по умолчанию делает все функции полиморфными.
ВВ>>Это помогло или сейчас будет очередная истерика в стиле самодовольного невежества?

VE>Я вам немножко напомню, что речь была об Idris и ваших словах, что это благодаря "отложенной типизации". Вам уже 2 человека говорят, что это не так.
VE>

VE>Ну да, легко. Отложенная типизация в действии =)

По поводу Идриса я высказал *предположение* (я не знаю Идрис), что доказательство корректности (которое таки делается по месту применения) является частью типизации. Компилятору-таки нужно понять, что в принципе может вернуть функция и способен ли клиентский код это отработать. Так что, условно говоря, если в динамике мы имеем "List->хз_что", причем вместо "хз_что" может быть Foo или Bar, то в Идрисе будет "List->Foo|Bar", и нам требуется сначала доказать, что ничего другого быть не может.

Причем не столь и важно, как это называть. Называйте "доказательством из применения". Просто, видимо, некоторые термины, получившие популяризацию благодаря Москалю, действуют тут как красная тряпка на быка.

А вот спор уже начался на тему "отложенная типизация в языках, поддерживающих полиморфные функции есть а) немерлизм, б) полная ересь". Что как бы не совсем корректно. Кстати, интересно одно теперь приравнивается ко второму?

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

K>Легко видеть, что функция типизируется вовсе не по первому применению. И может и обязательно будет типизирована при определении и вовсе без всякого применения.
K>Ну и в немерле никакой "типизации по месту применения" нет там просто всегда выводится конкретный тип, т.е. ограничение на полиморфизм сильнее чем в хаскеле и даже сильнее велью-рестрикшн в эмэлях.

Ну как же нет-то. В обоих языках — это некая стратегия, которая применяется в ряде случаев. Объясняется ли это исключительно дотнетовой системой типов — хз. Но смысл в этом есть и так — зачем нам полиморфная функция, если она используется неполиморфно?
И что-то мне кажется, в других ML-ях также можно найти подобное; проверять сейчас, правда, лень.

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

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

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

ВВ>>>Что как бы не исключает вышесказанного. Хаскелл, о котором в процитированном вами сообщении, речи вообще не шло, по умолчанию делает все функции полиморфными.
ВВ>>>Это помогло или сейчас будет очередная истерика в стиле самодовольного невежества?

VE>>Я вам немножко напомню, что речь была об Idris и ваших словах, что это благодаря "отложенной типизации". Вам уже 2 человека говорят, что это не так.
VE>>

VE>>Ну да, легко. Отложенная типизация в действии =)

ВВ>По поводу Идриса я высказал *предположение* (я не знаю Идрис), что доказательство корректности (которое таки делается по месту применения) является частью типизации.
Что вы имеете в виду под "доказательство корректности по месту применения"?
Вот в таком коде доказательство корректности делается по месту применения?

foo :: Int -> Int
foo = id

main = print (foo 23) -- тут доказывается, что 23 - это Int

И имеет ли к приведённому выше коду термин, популяризованный Москалем?

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

ВВ>>По поводу Идриса я высказал *предположение* (я не знаю Идрис), что доказательство корректности (которое таки делается по месту применения) является частью типизации.
VE>Что вы имеете в виду под "доказательство корректности по месту применения"?
VE>Вот в таком коде доказательство корректности делается по месту применения?

VE>

VE>foo :: Int -> Int
VE>foo = id

VE>main = print (foo 23) -- тут доказывается, что 23 - это Int
VE>

А этот код требуется доказывать? Здесь есть зависимые типы?

VE>И имеет ли к приведённому выше коду термин, популяризованный Москалем?

Т.е. вы все-таки кривляетесь?

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

ВВ>Ну как же нет-то. В обоих языках — это некая стратегия, которая применяется в ряде случаев. Объясняется ли это исключительно дотнетовой системой типов — хз. Но смысл в этом есть и так — зачем нам полиморфная функция, если она используется неполиморфно?

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

ВВ>И что-то мне кажется, в других ML-ях также можно найти подобное; проверять сейчас, правда, лень.

Ограничение полиморфизма с разными вариациями и названиями, разумеется, во всех есть. А типизации по применению (если понимать под этим то, что я написал выше) наоборот — нет. Такое (упрощенно говоря) есть разве что в C++.

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

VE>>

VE>>foo :: Int -> Int
VE>>foo = id

VE>>main = print (foo 23) -- тут доказывается, что 23 - это Int
VE>>

ВВ>А этот код требуется доказывать? Здесь есть зависимые типы?

Ну так (Int -> Int) — это теорема, а id — ее (конструктивное) доказательство. А зависимые типы или нет — в данном случае значения не имеет.

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

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

ВВ>>Ну как же нет-то. В обоих языках — это некая стратегия, которая применяется в ряде случаев. Объясняется ли это исключительно дотнетовой системой типов — хз. Но смысл в этом есть и так — зачем нам полиморфная функция, если она используется неполиморфно?
K>По моему, "типизация по первому применению" означает, что могут быть нетипизированные декларации функций, которые будут типизированы только в том случае, если будут применены и не раньше этого. Ничего такого в хаскеле, эмэлях, немерле нет. Все функции типизируются даже без всяких применений и эти типы могут быть записаны синтаксически.

Что значит нетипизорованные декларации функций? Такие функции попросту не будут скомпилированы. Поэтому F# в данном случае использует тот же default int, а вот немерле, если я правильно помню, потребует аннотировать тип явно. Отложенная типизация только то, что функция типизируется по первому применению при наличии оного. И наверное это нормальная практика в случае, если полиморфный тип или слишком дорог (при рантайм полиморфизме).

В чем собственно проблема с этой терминологией, я не понимаю?

ВВ>>И что-то мне кажется, в других ML-ях также можно найти подобное; проверять сейчас, правда, лень.

K>Ограничение полиморфизма с разными вариациями и названиями, разумеется, во всех есть. А типизации по применению (если понимать под этим то, что я написал выше) наоборот — нет. Такое (упрощенно говоря) есть разве что в C++.

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

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

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

VE>>>

VE>>>foo :: Int -> Int
VE>>>foo = id

VE>>>main = print (foo 23) -- тут доказывается, что 23 - это Int
VE>>>

ВВ>>А этот код требуется доказывать? Здесь есть зависимые типы?

K>Ну так (Int -> Int) — это теорема, а id — ее (конструктивное) доказательство. А зависимые типы или нет — в данном случае значения не имеет.

Хорошо, и какое это имеет отношение к обсуждаемому? Это как-то противоречит тому, что Идрис строит доказательство функции из ее применения?

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

ВВ>Что значит нетипизорованные декларации функций?

То и значит, что они не типизированы.

ВВ>Такие функции попросту не будут скомпилированы.

Ну и что? Компилирование-то тут причем?

ВВ> Поэтому F# в данном случае использует тот же default int, а вот немерле, если я правильно помню, потребует аннотировать тип явно.

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

ВВ> Отложенная типизация только то, что функция типизируется по первому применению при наличии оного. И наверное это нормальная практика в случае, если полиморфный тип или слишком дорог (при рантайм полиморфизме).
ВВ>В чем собственно проблема с этой терминологией, я не понимаю?

Проблема в том, что то, о чем вы говорите, называется "ограничением полиморфизма" и есть практически везде. работа этого ограничения отличается разными особенностями, например, эвристиками разрешения неоднозначностей. Но работает это похожим образом.
Вот хаскель:

Prelude> let sum = \a b -> a + b in let foo = sum (2::Int) 40 in (foo, sum 2.0 42)

<interactive>:12:67:
    No instance for (Fractional Int)
      arising from the literal `2.0'
    Possible fix: add an instance declaration for (Fractional Int)
    In the first argument of `sum', namely `2.0'
    In the expression: sum 2.0 42
    In the expression: (foo, sum 2.0 42)

Prelude> let sum a b = a + b in let foo = sum (2::Int) 40 in (foo, sum 2.0 42)
(42,44.0)
it :: (Int, Double)

демонстрирует ту же проблему при ограничении полиморфизма и нормально работает без ограничения. Означает ли это что там типизация откладывается? Что функции типизируются по первому применению? Да нет конечно. Так никто не говорит и если кто-то будет — его не поймут. Это первая проблема. Вторая проблема в том, что эти "термины" описывают механизм типизации в таких языках неправильно.
Третья проблема в том, что вся эта ветка не имеет отношения к обсуждаемой теме. Она про разрешение противоречий при выводе типов. А функция на идрисе проаннотирована типом и типизирована тут же, на месте:

useValue : (p:Bool) -> myType p -> String

Ничего никуда не отложено, по применению ничего не типизируется.

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

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

ВВ>>>По поводу Идриса я высказал *предположение* (я не знаю Идрис), что доказательство корректности (которое таки делается по месту применения) является частью типизации.
VE>>Что вы имеете в виду под "доказательство корректности по месту применения"?
VE>>Вот в таком коде доказательство корректности делается по месту применения?

VE>>

VE>>foo :: Int -> Int
VE>>foo = id

VE>>main = print (foo 23) -- тут доказывается, что 23 - это Int
VE>>

ВВ>А этот код требуется доказывать? Здесь есть зависимые типы?

Хорошо, а здесь где что доказывается по месту?

foo : (n : nat) → (n > 5) → string
foo n _ = show n
foo n ()

p : nat
p = 10

proof : 10 > 5
proof = refl

main = putStrLn (foo p proof)

VE>>И имеет ли к приведённому выше коду термин, популяризованный Москалем?

ВВ>Т.е. вы все-таки кривляетесь?

Пытаюсь выяснить значение терминов, которые вы вводите.

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

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

ВВ>>Что значит нетипизорованные декларации функций?

K>То и значит, что они не типизированы.

ВВ>>Такие функции попросту не будут скомпилированы.

K>Ну и что? Компилирование-то тут причем?

ВВ>> Поэтому F# в данном случае использует тот же default int, а вот немерле, если я правильно помню, потребует аннотировать тип явно.
K>Насколько я помню, для локальных функций там типы выведутся с ограничением полиморфизма, если только полиморфность не проаннотировать явно.

"Там" — это где?

ВВ>> Отложенная типизация только то, что функция типизируется по первому применению при наличии оного. И наверное это нормальная практика в случае, если полиморфный тип или слишком дорог (при рантайм полиморфизме).
ВВ>>В чем собственно проблема с этой терминологией, я не понимаю?
K>Проблема в том, что то, о чем вы говорите, называется "ограничением полиморфизма" и есть практически везде. работа этого ограничения отличается разными особенностями, например, эвристиками разрешения неоднозначностей. Но работает это похожим образом.

То, о чем я говорю, называется отложенной типизацией. А в Хаскелле это ограничение полиморфизма, да.

K>Вот хаскель:
K>

K>Prelude> let sum = \a b -> a + b in let foo = sum (2::Int) 40 in (foo, sum 2.0 42)

K><interactive>:12:67:
K>    No instance for (Fractional Int)
K>      arising from the literal `2.0'
K>    Possible fix: add an instance declaration for (Fractional Int)
K>    In the first argument of `sum', namely `2.0'
K>    In the expression: sum 2.0 42
K>    In the expression: (foo, sum 2.0 42)

K>Prelude> let sum a b = a + b in let foo = sum (2::Int) 40 in (foo, sum 2.0 42)
K>(42,44.0)
K>it :: (Int, Double)
K>

K>демонстрирует ту же проблему при ограничении полиморфизма и нормально работает без ограничения. Означает ли это что там типизация откладывается? Что функции типизируются по первому применению? Да нет конечно. Так никто не говорит и если кто-то будет — его не поймут. Это первая проблема.

Да, вот только этот код действительно демонстрирует другое. И действительно никто не говорит об отложенной типизации в Хаскелле.
В том же F# нет никакого ограничения полиморфизма, что прекрасно видно по коду. "let sum x y = x+y" без применения не будет иметь обобщенный тип, а будет иметь тип int->int->int. При наличии первого применения будет типизирована по первому применению и может стать, скажем, string->string->string. Ограничением чего в данном случае является string->string->string?
По Немерле так и вовсе есть документ:
http://research.microsoft.com/en-us/um/people/moskal/pdf/msc.pdf

K>Вторая проблема в том, что эти "термины" описывают механизм типизации в таких языках неправильно.

Пруф, пожалуйста, что этот "термин" описывает механизм типизации в F# неправильно.

K>Третья проблема в том, что вся эта ветка не имеет отношения к обсуждаемой теме. Она про разрешение противоречий при выводе типов. А функция на идрисе проаннотирована типом и типизирована тут же, на месте:
K>

K>useValue : (p:Bool) -> myType p -> String
K>

K>Ничего никуда не отложено, по применению ничего не типизируется.

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

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

ВВ>Да, тип аннотирован явно. Только вот этого типа недостаточно, чтобы программа прошла проверку. Корректность функции должна быть доказана на основе применения.

Эта функция — корректна, компилируется и работает, этого типа достаточно и он меняться не будет.
Что значит "этого типа недостаточно, чтобы программа прошла проверку"?
Типа функции id : a -> a тоже недостаточно?

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

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

ВВ>>Да, тип аннотирован явно. Только вот этого типа недостаточно, чтобы программа прошла проверку. Корректность функции должна быть доказана на основе применения.

VE>Эта функция — корректна, компилируется и работает, этого типа достаточно и он меняться не будет.
VE>Что значит "этого типа недостаточно, чтобы программа прошла проверку"?
VE>Типа функции id : a -> a тоже недостаточно?

У меня не работает, типы используются правильно:

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
  print $ saturate 2 100 (fun xs)

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

DM>>Я перевел твою программу дословно. В ней ровно столько зависимости от рантайм значений, сколько в оригинале. Если в статически типизированной версии такой зависимости не усматривается, это лишь потому, что ее не было в исходном варианте.

ВВ>Ну зачем же обманывать? Моя программа работает корректно благодаря рантайм проверке типа, ты, конечно же, ее устранил, но теперь оказывается, что программа была переведена "дословно". Это нормальный подход к дискуссии для тебя?

Не было у тебя рантайм проверки типа, тип там везде один — dynamic (или как он там называтся в Эле). А была проверка тэга, который сидит в каждом значении. Именно такую проверку я и сделал, выразив этот тэг явно. Число возможных вариантов оказалось меньше, тэгов всего два возможных получилось, лишние были выкинуты. Поэтому это вполне себе дословный перевод: что делалось в оригинале, то и делается в переводе.

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

ВВ> говоришь как человек, который "других ФЯ" в глаза не видел. Причем довольно известных. Например, F#.

Спасибо, просветил меня насчет F#. Я и раньше знал, что это недоделка по мотивам приличного языка, но как-то запямятовал, что настолько убогая. Но ведь "нормальные" полиморфные функции там тоже есть? Это просто проблема слабого вывода типов, как я понял.

ВВ>Да повторяй хоть сотни раз. В твоей трактовке сам термин "зависимость от рантайм-значений" теряет всякий смысл. Я уже множество раз, разными словами, пытался объяснить, какой смысл я вкладываю в это утверждение. Мы зависим от рантайма только в том случае, когда не можем рассуждать о возможных значениях статически.

Раньше ты формулировал его по-другому. Теперь понятно. Что ж, просто у тебя абсолютно неправильное определение. Предлагаю его выкинуть на помоечку и почерпнуть правильное.

ВВ>>>Диапазон значений известен в компайл, соответственно, всё просчитывается статически.
DM>>Да. Но сами конкретные значения не известны, в этом вся суть.
ВВ>Вообще-то если конкретные значения известны, то обычно и само вычисление не требуется.

Какое именно вычисление? Речь же идет о типах, не забывай.

DM>>Как видим, о рантайм значениях можно рассуждать статически. Сюрприз!
ВВ>Можно подумать, это и правда было для тебя сюрпризом, судя по тому, с каким жаром ты сейчас об этом рассуждаешь.

Для меня-то нет, ведь это я тебе на ошибки в статье указываю, а не наоборот.

ВВ>Обработка означает, что код *может* работать неправильно, мы допускаем это и пишем другой код, который обрабатывает данную ситуацию. Т.е. мы не задаемся вопросом "при каких значениях этот код будет работать?"; у нас другой вопрос — "что делать, когда код не работает?"

А, навроде catch(...). Ну, тут понятно что делать — констатировать, что в программе баг и идти его исправлять. Обсуждать технику написания абсурдных программ с багами не очень интересно, по выразительности некорректных программ динамические языки конечно сложно превзойти. Я все же вел речь о способах выражения корректных программ.

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

ВВ>>>Да, тип аннотирован явно. Только вот этого типа недостаточно, чтобы программа прошла проверку. Корректность функции должна быть доказана на основе применения.

Я понял, речь идет не о "корректности функции", а о проверке типа выражения, в котором она применяется.

ВВ>У меня не работает, типы используются правильно:
ВВ>saturate : (n:Nat) -> Int -> sumType n -> Int
ВВ> let xs = convertArgs as
ВВ> print $ saturate 2 100 (fun xs)

Тут функция и ее тип корректные, но вызывается она не с подходящими типами аргументов, поэтому выражение saturate 2 100 (fun xs) не проходит проверку типов. Это как в List.map передавать не список, а число. Функция-то правильная, но используется неправильно.

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

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

DM>>>Я перевел твою программу дословно. В ней ровно столько зависимости от рантайм значений, сколько в оригинале. Если в статически типизированной версии такой зависимости не усматривается, это лишь потому, что ее не было в исходном варианте.

ВВ>>Ну зачем же обманывать? Моя программа работает корректно благодаря рантайм проверке типа, ты, конечно же, ее устранил, но теперь оказывается, что программа была переведена "дословно". Это нормальный подход к дискуссии для тебя?
DM>Не было у тебя рантайм проверки типа, тип там везде один — dynamic (или как он там называтся в Эле). А была проверка тэга, который сидит в каждом значении.

Давай только не уводить все в сторону "в динамике вообще один тип".
Вот это вот:

x is Fun

это проверка того, что x является функцией. Fun в данном случае не конструктор, а x не является алгебраическим типом.

DM>Именно такую проверку я и сделал, выразив этот тэг явно. Число возможных вариантов оказалось меньше, тэгов всего два возможных получилось, лишние были выкинуты. Поэтому это вполне себе дословный перевод: что делалось в оригинале, то и делается в переводе.

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

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

ВВ>>>>Да, тип аннотирован явно. Только вот этого типа недостаточно, чтобы программа прошла проверку. Корректность функции должна быть доказана на основе применения.

DM>Я понял, речь идет не о "корректности функции", а о проверке типа выражения, в котором она применяется.

ВВ>>У меня не работает, типы используются правильно:
ВВ>>saturate : (n:Nat) -> Int -> sumType n -> Int
ВВ>> let xs = convertArgs as
ВВ>> print $ saturate 2 100 (fun xs)

DM>Тут функция и ее тип корректные, но вызывается она не с подходящими типами аргументов, поэтому выражение saturate 2 100 (fun xs) не проходит проверку типов. Это как в List.map передавать не список, а число. Функция-то правильная, но используется неправильно.

Разве эта аналогия уместна? Такое применение saturate как у меня вполне соответствует сигнатуре функции, насколько я могу судить.

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

DM>Здравствуйте, Воронков Василий, Вы писали:
ВВ>> говоришь как человек, который "других ФЯ" в глаза не видел. Причем довольно известных. Например, F#.
DM>Спасибо, просветил меня насчет F#. Я и раньше знал, что это недоделка по мотивам приличного языка, но как-то запямятовал, что настолько убогая. Но ведь "нормальные" полиморфные функции там тоже есть? Это просто проблема слабого вывода типов, как я понял.

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

ВВ>>>>Диапазон значений известен в компайл, соответственно, всё просчитывается статически.
DM>>>Да. Но сами конкретные значения не известны, в этом вся суть.
ВВ>>Вообще-то если конкретные значения известны, то обычно и само вычисление не требуется.

DM>Какое именно вычисление? Речь же идет о типах, не забывай.

DM>>>Как видим, о рантайм значениях можно рассуждать статически. Сюрприз!
ВВ>>Можно подумать, это и правда было для тебя сюрпризом, судя по тому, с каким жаром ты сейчас об этом рассуждаешь.
DM>Для меня-то нет, ведь это я тебе на ошибки в статье указываю, а не наоборот.

В статье не идет речи о зависимых типах. Спор идет о том, возможна и в каком виде возможна вполне конкретная функция в статическом языке.

ВВ>>Обработка означает, что код *может* работать неправильно, мы допускаем это и пишем другой код, который обрабатывает данную ситуацию. Т.е. мы не задаемся вопросом "при каких значениях этот код будет работать?"; у нас другой вопрос — "что делать, когда код не работает?"
DM>А, навроде catch(...). Ну, тут понятно что делать — констатировать, что в программе баг и идти его исправлять. Обсуждать технику написания абсурдных программ с багами не очень интересно, по выразительности некорректных программ динамические языки конечно сложно превзойти. Я все же вел речь о способах выражения корректных программ.

Необязательно catch, хотя это тоже вариант. Вообще-то речь не идет о красивом или некрасивом коде. Речь идет о том, возможно ли fun на Ela реализовать в статике. Ты приводишь аналоги, которые работают — но иначе.

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

ВВ>Давай только не уводить все в сторону "в динамике вообще один тип".
ВВ>x is Fun
ВВ>это проверка того, что x является функцией. Fun в данном случае не конструктор, а x не является алгебраическим типом.

Эдак ты все сведешь к утверждениям вроде: вот это нельзя сделать на другом языке потому что это будет другой язык и будет выражено другими средствами.
С т.з. как теории типов, так и реализации многих ДЯП, в динамике как раз всего один тип, и он даже алгебраический. Если от этого не отнекиваться, то очевидно, как любую программу на динамически типизированном языке можно при желании один в один переписать на статическом. Но я согласен, это уже не интересная тема.