Re[36]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 30.11.13 18:33
Оценка: +1
Здравствуйте, Воронков Василий, Вы писали:

ВВ>>>saturate : (n:Nat) -> Int -> sumType n -> Int

ВВ>>> print $ saturate 2 100 (fun xs)

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


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


По-моему, не соответствует. Чтобы применение было корректным, тут (fun xs) должно иметь тип sumType 2, но этого типа оно не имеет, а имеет sumType (length xs). О чем компилятор и сообщает.
Can't unify
        sumType (Prelude.List.length xs)
with
        sumType (Prelude.Classes.fromInteger 2)
Re[25]: Неправильное введение в функциональное программирование
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 30.11.13 18:41
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Я так понял "ересь", "ненормальный" и "немерле" теперь являются синонимами.

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

Я бы отталкивался от теории типов, штук вроде System F, лямбда-куба и т.п.

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


Так языки с завтипами как раз статически типизированы, ровно поэтому и возникло возражение.

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


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


Я тоже говорю не о красивом коде, а о корректном.
Реализованы мои аналоги, конечно, иначе, но соответствуют постановке задачи (например, соответствие числа аргументов длине списка), т.е. реализовать подобные функции в статике таки можно. Просто несколько не в той статике, которая подразумевалась в статье.
Re[32]: Неправильное введение в функциональное программирование
От: Klapaucius  
Дата: 30.11.13 18:48
Оценка: +1
Здравствуйте, Воронков Василий, Вы писали:

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

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

В немерле.

ВВ>То, о чем я говорю, называется отложенной типизацией.


Нет, в ваших примерах именно ограничение полиморфизма.

ВВ>Да, вот только этот код действительно демонстрирует другое. И действительно никто не говорит об отложенной типизации в Хаскелле.

ВВ>В том же F# нет никакого ограничения полиморфизма, что прекрасно видно по коду. "let sum x y = x+y" без применения не будет иметь обобщенный тип, а будет иметь тип int->int->int. При наличии первого применения будет типизирована по первому применению и может стать, скажем, string->string->string. Ограничением чего в данном случае является string->string->string?

Именно по коду и видно, что есть. Вот смотрите: для того, чтоб функцию выполнить нам нужно функцию конкретизировать, заполнить все параметры со штрихами в ее типе, точно так же, как и во все параметры функции что-то передать. F#, как я уже сказал, — это два языка с различающимися системами типов. Типы "языка inline-функций" могут быть в том числе и такими, какие в основном языке невозможны:

> let inline sum x y = x+y;;

val inline sum :
  x: ^a -> y: ^b ->  ^c
    when ( ^a or  ^b) : (static member ( + ) :  ^a *  ^b ->  ^c)


Пока мы остаемся в рамках "inline-F#" все хорошо:

> let inline x2 x = sum x x;;

val inline x2 :
  x: ^a ->  ^b when  ^a : (static member ( + ) :  ^a *  ^a ->  ^b)


Но если мы используем inline-функцию в обычной, нам придется заполнить все параметры с крышечкой, точно так же, как нам нужно заполнить все параметры со штрихами чтоб что-то выполнить. Вот тут и наступает ограничение полиморфизма. В данном случае — "крышечного".
Конкретные типы нужно откуда-то брать, это можно сделать с той или иной степенью хитрости, но тут можно только из типов по умолчанию:
> let x2 x = sum x x;;

val x2 : x:int -> int

А где-то из применения и т.д. Если же это невозможно — вывод типов сдается и просит проаннотировать тип вручную. Это не только определение типа по применению (может по возвращению, например), а F# не всегда и по применению может:

> let foo x = x.Length in foo [|1|];;

  let foo x = x.Length in foo [|1|];;
  ------------^^^^^^^^

stdin(46,13): error FS0072: Lookup on object of indeterminate type 
based on information prior to this program point. A type annotation 
may be needed prior to this program point to constrain the type of 
the object. This may allow the lookup to be resolved.


Некоторые применения в F# равнее прочих:

> [|1|] |> fun x -> x.Length;;
val it : int = 1
> fun x -> x.Length <| [|1|] ;;

  fun x -> x.Length <| [|1|] ;;
  ---------^^^^^^^^

stdin(52,10): error FS0072: и т.д.


Этот недоделанный алгоритм мономорфизации в F# и является прямым родственником локального вывода типов из Немерле (в котором он действительно выводит тип по применению и отложенно и работает в более сложных случаях). Аналогов основного, "обобщающего" вывода типа (в F# это как обычно какая-то вариация алгоритма-W) в немерле нет.

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


С.м. выше, вы говорили что функции "типизируются по применению" а F# даже тип по применению вывести не может. С другой стороны — в других случаях может без всякого применения.

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


Это не верно.
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[33]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 30.11.13 18:58
Оценка:
Здравствуйте, Klapaucius, Вы писали:

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


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

ВВ>>"Там" — это где?
K>В немерле.

Москаль же вполне подробно описывает, что и как там выводится. Посмотри "Type inference with deferal".
Выше же ты утверждаешь, что типизации по применению нет и в Немерле.

ВВ>>То, о чем я говорю, называется отложенной типизацией.

K>Нет, в ваших примерах именно ограничение полиморфизма.
ВВ>>Да, вот только этот код действительно демонстрирует другое. И действительно никто не говорит об отложенной типизации в Хаскелле.
ВВ>>В том же F# нет никакого ограничения полиморфизма, что прекрасно видно по коду. "let sum x y = x+y" без применения не будет иметь обобщенный тип, а будет иметь тип int->int->int. При наличии первого применения будет типизирована по первому применению и может стать, скажем, string->string->string. Ограничением чего в данном случае является string->string->string?

K>Именно по коду и видно, что есть. Вот смотрите: для того, чтоб функцию выполнить нам нужно функцию конкретизировать, заполнить все параметры со штрихами в ее типе, точно так же, как и во все параметры функции что-то передать. F#, как я уже сказал, — это два языка с различающимися системами типов. Типы "языка inline-функций" могут быть в том числе и такими, какие в основном языке невозможны:

K>
>> let inline sum x y = x+y;;
K>val inline sum :
K>  x: ^a -> y: ^b ->  ^c
K>    when ( ^a or  ^b) : (static member ( + ) :  ^a *  ^b ->  ^c)
K>


Инлайн — это инлайн. Было бы очень странно, если бы инлайн типизировался по первому применению.

K>Пока мы остаемся в рамках "inline-F#" все хорошо:


K>
>> let inline x2 x = sum x x;;
K>val inline x2 :
K>  x: ^a ->  ^b when  ^a : (static member ( + ) :  ^a *  ^a ->  ^b)
K>

K>Но если мы используем inline-функцию в обычной, нам придется заполнить все параметры с крышечкой, точно так же, как нам нужно заполнить все параметры со штрихами чтоб что-то выполнить. Вот тут и наступает ограничение полиморфизма. В данном случае — "крышечного".
K>Конкретные типы нужно откуда-то брать, это можно сделать с той или иной степенью хитрости, но тут можно только из типов по умолчанию:
K>
>> let x2 x = sum x x;;
K>val x2 : x:int -> int
K>

K>А где-то из применения и т.д. Если же это невозможно — вывод типов сдается и просит проаннотировать тип вручную.

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

Я не понимаю, в чем проблема. Не устраивет термин "отложенная"? Мое утверждение понимается так, как будто в языке *всегда* используется отложенная типизация? Нет, не всегда. Иногда — используется. А иногда (в F#, кстати, нередко) все вообще аннотировано явно.

K>Это не только определение типа по применению (может по возвращению, например), а F# не всегда и по применению может:

K>
>> let foo x = x.Length in foo [|1|];;
K>  let foo x = x.Length in foo [|1|];;
K>  ------------^^^^^^^^
K>stdin(46,13): error FS0072: Lookup on object of indeterminate type 
K>based on information prior to this program point. A type annotation 
K>may be needed prior to this program point to constrain the type of 
K>the object. This may allow the lookup to be resolved.
K>


K>Некоторые применения в F# равнее прочих:


K>
>> [|1|] |> fun x -> x.Length;;
K>val it : int = 1
>> fun x -> x.Length <| [|1|] ;;

K>  fun x -> x.Length <| [|1|] ;;
K>  ---------^^^^^^^^

K>stdin(52,10): error FS0072: и т.д.
K>


K>Этот недоделанный алгоритм мономорфизации в F# и является прямым родственником локального вывода типов из Немерле (в котором он действительно выводит тип по применению и отложенно и работает в более сложных случаях). Аналогов основного, "обобщающего" вывода типа (в F# это как обычно какая-то вариация алгоритма-W) в немерле нет.


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

K>С.м. выше, вы говорили что функции "типизируются по применению" а F# даже тип по применению вывести не может. С другой стороны — в других случаях может без всякого применения.

В F# этот алгоритм сильно отличается от немерлового, в котором собственно ХМ вообще не используется, насколько я понимаю. Но тем не менее — иногда F# таки выводит тип по применению и отложенно.

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

K>Это не верно.
Re[34]: Неправильное введение в функциональное программирование
От: VoidEx  
Дата: 30.11.13 20:37
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

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


ВВ>
ВВ>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)
ВВ>


Конечно неправильно, и вы сами это видите. 2 никак не равняется length xs.
Re[23]: философия статики
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 01.12.13 08:48
Оценка: 2 (1) :)
Здравствуйте, Воронков Василий, Вы писали:

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


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

Мысль 1. Если получилось все термы в программе непротиворечиво снабдить типами, то все ок, у нас есть корректная программа, свободная от рантайм ошибок типизации. И если получилось, значит мы смогли рассудить о значениях статически. Если же по какой-то причине мы не может о них статически рассуждать, то и типизировать статически программу не выйдет, она не будет считаться корректной. Фактически, твои вопрошания свелись к "можем ли мы в статике сделать то, чего нельзя делать в статике?". Видимо, не можем.

Мысль 2. По какой причине может возникнуть такое затруднение со статической расстановкой типов? В языках попроще (вплоть до хаскеля) обычно есть явное разграничение между термами и типами. Это два отдельных языка, термы строятся так-то, типы строятся так-то, связываются они через а::Т ("терм а имеет тип Т"). Поскольку это разные языки, они могут где-то расходиться в выразительной силе, и какому-то выражению на языке термов может не соответствовать ни одно выражение на языке типов. Такое выражение не получится типизировать в этой системе типов.

Но системы с зависимыми типами тут разительно отличаются. Они убирают эту грань между двумя подъязыками термов и типов, теперь это все один язык термов. 42 это терм, и Int это терм, и термы могут выступать в роли типов (связка "терм а имеет тип Т" синтаксически выглядит как "терм : терм", а не "терм : тип"). В результате поскольку слева и справа от : ("имеет тип") один и тот же язык, выразительность одинаковая, и по крайней мере этот источник нетипизируемости каких-то выражений устраняется.

Мысль 3. Системы типов в приличных местах строятся не от балды, а основываются на стройных идеях из логики и теории категорий (произведение-конъюнкция, копроизведение-сумма-дизъюнкция, экспонента-следствие и т.п.) в результате чего имеем соответствие Карри-Говарда, согласно которому типы это логические утверждения в интуиционистской логике, а имеющие их термы — это их доказательства. Написал тело функции нужного типа — значит написал конструктивное доказательство теоремы. В этом свете любой код, у которого нет статического типа — это доказательство без утверждения. И всякое бестиповое программирование — это тоже попытка строить доказательства без утверждений. Есть в этом что-то шизофреническое, рациональной деятельностью это сложно назвать.
Re[34]: Неправильное введение в функциональное программирование
От: Klapaucius  
Дата: 01.12.13 14:55
Оценка:
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Выше же ты утверждаешь, что типизации по применению нет и в Немерле.


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

Отложенный вывод типов в Немерле есть, но его нет в F#. Москальский алгоритм называется отложенным, как я понимаю, чтоб подчеркнуть его отличие от "жадного" алгоритма Карделли. И отличие это заключается в механизме работы с сабтайпингом. Именно оно позволяет выводить типы в тех случаях, для которых я показал, что F# типы вывести наоборот не может. Т.е. никакого отложенного вывода типов там нет.

ВВ>Инлайн — это инлайн. Было бы очень странно, если бы инлайн типизировался по первому применению.


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

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


Если вы то, что вы показали для F# называете "типизацией по первому применению", то почему вы тогда соглашаетесь с тем, что с хаскелем тут ничего общего нет, ведь вывод типов в F# работает в основном как в хаскеле и совсем не так как в немерле.

ВВ>Я не понимаю, в чем проблема. Не устраивет термин "отложенная"? Мое утверждение понимается так, как будто в языке *всегда* используется отложенная типизация? Нет, не всегда. Иногда — используется. А иногда (в F#, кстати, нередко) все вообще аннотировано явно.


Три проблемы я перечислил. Оказалось, что есть и четвертая. Создается ложное впечатление, что в F# используется тот же способ мономорфизации в присутствии сабтайпинга, что и в немерле. Но название немерлевского алгоритма как раз и подчеркивает его отличие от родственных тому, что используется в F#.

ВВ>В F# этот алгоритм сильно отличается от немерлового, в котором собственно ХМ вообще не используется, насколько я понимаю.


В прошлом посте я так и написал. В F# есть алгоритм общего вывода типов (вариация Х-М), а есть простая реконструкция типов при ограничении полиморфизма. В немерле же общего вывода нет вообще, а реконструкция как раз навороченная.

ВВ>Но тем не менее — иногда F# таки выводит тип по применению и отложенно.


Иногда F# выводит типы как хаскель, а как немерле никогда, что я продемонстрировал на примерах.
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[24]: философия статики
От: Воронков Василий Россия  
Дата: 01.12.13 18:19
Оценка:
Здравствуйте, D. Mon, Вы писали:

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


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


DM>Пофилософствую немножко.

DM>Если открыть учебники по теории типов и дизайну ЯП, там говорится, что в статической типизации тип — это некая синтаксическая конструкция, которая приписывается (порой компилятором, когда есть вывод типов) каждому терму (выражению) в исходном коде программы. Нужна она как раз для статических рассуждений о возможных значениях.
DM>Мысль 1. Если получилось все термы в программе непротиворечиво снабдить типами, то все ок, у нас есть корректная программа, свободная от рантайм ошибок типизации. И если получилось, значит мы смогли рассудить о значениях статически. Если же по какой-то причине мы не может о них статически рассуждать, то и типизировать статически программу не выйдет, она не будет считаться корректной. Фактически, твои вопрошания свелись к "можем ли мы в статике сделать то, чего нельзя делать в статике?". Видимо, не можем.

Ага, надо было, наверное, ставить вопрос — а можем ли мы на одном Тьюринг-полном языке решить задачу, решенную на другом. Видимо, можем. На то он и Тьюринг-полный.

DM>Мысль 2. По какой причине может возникнуть такое затруднение со статической расстановкой типов? В языках попроще (вплоть до хаскеля) обычно есть явное разграничение между термами и типами. Это два отдельных языка, термы строятся так-то, типы строятся так-то, связываются они через а::Т ("терм а имеет тип Т"). Поскольку это разные языки, они могут где-то расходиться в выразительной силе, и какому-то выражению на языке термов может не соответствовать ни одно выражение на языке типов. Такое выражение не получится типизировать в этой системе типов.


DM>Но системы с зависимыми типами тут разительно отличаются. Они убирают эту грань между двумя подъязыками термов и типов, теперь это все один язык термов. 42 это терм, и Int это терм, и термы могут выступать в роли типов (связка "терм а имеет тип Т" синтаксически выглядит как "терм : терм", а не "терм : тип"). В результате поскольку слева и справа от : ("имеет тип") один и тот же язык, выразительность одинаковая, и по крайней мере этот источник нетипизируемости каких-то выражений устраняется.


DM>Мысль 3. Системы типов в приличных местах строятся не от балды, а основываются на стройных идеях из логики и теории категорий (произведение-конъюнкция, копроизведение-сумма-дизъюнкция, экспонента-следствие и т.п.) в результате чего имеем соответствие Карри-Говарда, согласно которому типы это логические утверждения в интуиционистской логике, а имеющие их термы — это их доказательства. Написал тело функции нужного типа — значит написал конструктивное доказательство теоремы. В этом свете любой код, у которого нет статического типа — это доказательство без утверждения. И всякое бестиповое программирование — это тоже попытка строить доказательства без утверждений. Есть в этом что-то шизофреническое, рациональной деятельностью это сложно назвать.


Это что, в Кащенко так программируют? Безтипового программирования не бывает. Программист так или иначе подразумевает типы и делает утверждения, а вот конкретный компилятор может уже его утверждения проверить (типизировать) или довериться рантайму. ФП как раз безтиповое изначально и без типов прекрасно обходится.
Re[25]: философия статики
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 01.12.13 18:36
Оценка: +1 :)
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Ага, надо было, наверное, ставить вопрос — а можем ли мы на одном Тьюринг-полном языке решить задачу, решенную на другом. Видимо, можем. На то он и Тьюринг-полный.


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

ВВ>Это что, в Кащенко так программируют? Безтипового программирования не бывает. Программист так или иначе подразумевает типы и делает утверждения, а вот конкретный компилятор может уже его утверждения проверить (типизировать) или довериться рантайму. ФП как раз безтиповое изначально и без типов прекрасно обходится.


Если эти утверждения остаются несформулированными, у них большой шанс быть или неверными или просто абсурдными.
Что до Кащенко, то это лучше спросить у того, кто в одном абзаце говорит "ФП как раз безтиповое изначально и без типов прекрасно обходится" и "Безтипового программирования не бывает".
Re[35]: Неправильное введение в функциональное программирование
От: Воронков Василий Россия  
Дата: 01.12.13 22:34
Оценка:
Здравствуйте, Klapaucius, Вы писали:

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

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

Интересно, конечно. Ты еще текстовые макросы вспомни. Отложенная типизация означает, что тип функции уточняется по первому применению.

K>Отложенный вывод типов в Немерле есть, но его нет в F#. Москальский алгоритм называется отложенным, как я понимаю, чтоб подчеркнуть его отличие от "жадного" алгоритма Карделли. И отличие это заключается в механизме работы с сабтайпингом. Именно оно позволяет выводить типы в тех случаях, для которых я показал, что F# типы вывести наоборот не может. Т.е. никакого отложенного вывода типов там нет.


В F# с выводом типов все дрвольно запутанно и сложно. Х-М там все равно используется сильно модифицированный; AFAIR там вообще разные стратегии вывода типов для разных случаев, ибо поддерживается глобальный вывод типов, а снаружи у нас дотнет. Поэтому таки да, такая стратегия как отложенный вывод типа функции там таки используется. И даже *по твоим примерам* хорошо видно, что это не усечение полиморфизма, ибо без применения глобальная функция вида let sum x y = x+y все равно не будет иметь полиморфный тип.

ВВ>>Инлайн — это инлайн. Было бы очень странно, если бы инлайн типизировался по первому применению.

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

Все-все выводится по ХМ? В дотнетовой системе типов? Ну-ну. Это про какой-то другой язык рассказываешь, не про F#.

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

K>Если вы то, что вы показали для F# называете "типизацией по первому применению", то почему вы тогда соглашаетесь с тем, что с хаскелем тут ничего общего нет, ведь вывод типов в F# работает в основном как в хаскеле и совсем не так как в немерле.

Потому что в Хаскелле этого нет, в Хаскелле усечение полиморфизма.

ВВ>>Я не понимаю, в чем проблема. Не устраивет термин "отложенная"? Мое утверждение понимается так, как будто в языке *всегда* используется отложенная типизация? Нет, не всегда. Иногда — используется. А иногда (в F#, кстати, нередко) все вообще аннотировано явно.

K>Три проблемы я перечислил. Оказалось, что есть и четвертая. Создается ложное впечатление, что в F# используется тот же способ мономорфизации в присутствии сабтайпинга, что и в немерле. Но название немерлевского алгоритма как раз и подчеркивает его отличие от родственных тому, что используется в F#.

Проблема одна. Нет, вернее, две. Первоначально ты пытался утверждать, что этого нет даже в немерле. Данный вопрос, я так понимаю, мы замяли? Осталось теперь замять вопрос с F# и можно начинать спорить о чем-то другом, как здесь принято.

ВВ>>В F# этот алгоритм сильно отличается от немерлового, в котором собственно ХМ вообще не используется, насколько я понимаю.

K>В прошлом посте я так и написал. В F# есть алгоритм общего вывода типов (вариация Х-М), а есть простая реконструкция типов при ограничении полиморфизма. В немерле же общего вывода нет вообще, а реконструкция как раз навороченная.
ВВ>>Но тем не менее — иногда F# таки выводит тип по применению и отложенно.
K>Иногда F# выводит типы как хаскель, а как немерле никогда, что я продемонстрировал на примерах.

На примерах с инлайн? Смешно.
Re[26]: философия статики
От: Воронков Василий Россия  
Дата: 01.12.13 22:37
Оценка:
Здравствуйте, D. Mon, Вы писали:

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


ВВ>>Ага, надо было, наверное, ставить вопрос — а можем ли мы на одном Тьюринг-полном языке решить задачу, решенную на другом. Видимо, можем. На то он и Тьюринг-полный.


DM>Самое смешное, что завтипы часто требуют тотальность, а она влечет Тьюринг-худобу. Мы привыкли иметь Тьюринг-полноту как нечто само собой разумеющееся, но это скорее баг, чем фича. Возможность бесконечных циклов все портит по части reasoning, но при наличии коиндукции не особенно нужна на практике.


ВВ>>Это что, в Кащенко так программируют? Безтипового программирования не бывает. Программист так или иначе подразумевает типы и делает утверждения, а вот конкретный компилятор может уже его утверждения проверить (типизировать) или довериться рантайму. ФП как раз безтиповое изначально и без типов прекрасно обходится.

DM>Если эти утверждения остаются несформулированными, у них большой шанс быть или неверными или просто абсурдными.

Статика вс. динамика — это действительно настолько интересная тема или просто больная мозоль?

DM>Что до Кащенко, то это лучше спросить у того, кто в одном абзаце говорит "ФП как раз безтиповое изначально и без типов прекрасно обходится" и "Безтипового программирования не бывает".


Ага, потому что в процесс программирования еще вовлечен человек. И вот он-то как раз не может без типов, а языки программирования без них прекрасно обходятся. Так что да. Безтипового программирования не бывает, а языки — вполне. Все же это человек делает утверждения, а не компилятор.
Re[36]: Неправильное введение в функциональное программирование
От: Klapaucius  
Дата: 02.12.13 10:19
Оценка: +1
Здравствуйте, Воронков Василий, Вы писали:

ВВ>Интересно, конечно. Ты еще текстовые макросы вспомни. Отложенная типизация означает, что тип функции уточняется по первому применению.


ОК. Тоесть Х-М это и есть "отложенная типизация"? Уточнение (раньше у вас была типизация) типа по первому применению я продемонстрировал.

ВВ>В F# с выводом типов все дрвольно запутанно и сложно. Х-М там все равно используется сильно модифицированный; AFAIR там вообще разные стратегии вывода типов для разных случаев, ибо поддерживается глобальный вывод типов, а снаружи у нас дотнет.


Лично я даже не видел статьи с описанием. Т.е. известно, что в хаскеле вывод типов InsideOut(X), в скале Colored Local Type Inference, для немерле обсуждаемое описание есть. А Сайм то ли нетеоретик и писать ленится, то ли общая нетеоретическая атмосфера в комьюнити не способствует распространению ссылки на статью и делает ее негуглибельной. На вопрос "как работает вывод типов" отвечают обычно "ну эта, работает он, обычно, сверху вниз и слева направо, значить"

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


Зависит от того, что вы под этим подразумеваете. Пока может Х-М может и F# а как только появляется сабтайпинг так F# сразу перестает мочь в подавляющем большинстве случаев.
Если вы под этим понимаете "как в немерле", то нет, не используется.

ВВ>И даже *по твоим примерам* хорошо видно, что это не усечение полиморфизма, ибо без применения глобальная функция вида let sum x y = x+y все равно не будет иметь полиморфный тип.


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

ВВ>Все-все выводится по ХМ? В дотнетовой системе типов? Ну-ну. Это про какой-то другой язык рассказываешь, не про F#.


Я же пишу черным по белому, языком пушкина и достоевского на разные лады, что и чем выводится, а что реконструируется и мономорфизуется. В дотнетной системе типов Х-М всего не выведешь, ну так F# и не выводит!

ВВ>Потому что в Хаскелле этого нет, в Хаскелле усечение полиморфизма.


Ну и в F# тоже ограничение полиморфизма. Вы в нем ошибки "велью рестрикшн" никогда не видели что ли?

ВВ>Проблема одна. Нет, вернее, две. Первоначально ты пытался утверждать, что этого нет даже в немерле. Данный вопрос, я так понимаю, мы замяли? Осталось теперь замять вопрос с F# и можно начинать спорить о чем-то другом, как здесь принято.


Я же не могу ваши мысли читать. Когда вы выдумываете термин, я выдвигаю гипотезы-расшифровки. Если это первая гипотеза — то нет ни там, ни там. Если это означает "отложенный вывод типов как в немерле", то очевидно, что в немерле это есть. Ну а в F# этого нет. Если это означает Х-М и ограничение полиморфизма — то это во всех эмелях есть и в хаскеле, а в немерле наоборот нет. В Idris, что характерно, нет ничего из вышеперечисленного.

K>>Иногда F# выводит типы как хаскель, а как немерле никогда, что я продемонстрировал на примерах.

ВВ>На примерах с инлайн? Смешно.

И на примерах без инлайн. Я бы сказал, особенно на примерах без инлайн. Смешно или нет — это к делу не относится. По существу возражения есть?
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.