[Динамик не нужен] Анонимные алгебраические типы. - Философия программирования

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

def foo(x): if x == 0 then 0 else "bar" end

Я предлагаю статически типизированое решение, что то похожее на

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

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

Насколько я понимаю, до сих пор эти высказывания в силе.
Интересует достоверность высказывания б). Может ли кто объяснить не ссылаясь на священые писания почему это так. Я умных книжек не читал поэтому совершено не вижу в чем тут может быть проблема, какая разница один тип или несколько, плюс мне видится это это вполне реализуемое как сахар поверх какого нибудь

type IntString = X of int | Y of string

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

... << RSDN@Home 1.2.0 alpha 4 rev. 1111>>

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

D>def foo(x): if x == 0 then 0 else "bar" end
D>

D>Я предлагаю статически типизированое решение, что то похожее на
D>

D>let foo x = if x == 0 then 0 else "bar" end
D>foo :: int -> int | string
D>

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

D>Насколько я понимаю, до сих пор эти высказывания в силе.
D>Интересует достоверность высказывания б). Может ли кто объяснить не ссылаясь на священые писания почему это так. Я умных книжек не читал поэтому совершено не вижу в чем тут может быть проблема, какая разница один тип или несколько, плюс мне видится это это вполне реализуемое как сахар поверх какого нибудь
D>

D>type IntString = X of int | Y of string
D>

Чёрт знает насчёт теоретически возможного, но в текущих языках с АТД (Haskell, Ocaml) такой фокус не прокатит, потому что вызывающая функция должна явно "распаковывать" строковое или численное значение из типа IntString с помощью матчинга на один из конструкторов. Кроме того, по крайней мере в хацкеле, внутри модуля конструкторы уникальны.

То есть type IntString объявить действительно несложно и объявить функцию, которая его возвращает, даже неявно — несложно. А вот как вы себе представляете использование такой функции?

D>Так же можно обсудить, общую здравость идеи зависимости сигнатуры функции от входящих параметров.

Это у кого куда мозг повёрнут. Любители динамики совершенно спокойно мыслят функциями, которые утром возвращают строку, а вечером boolean; любители статики от такого делят на ноль и начинают собирать аргументы против. Мой посыл заключается в том, что здравость (любой) идеи всегда будет оценена субъективно, то есть обсуждение скатится в срач — оно вам надо?

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

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

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

T>Чёрт знает насчёт теоретически возможного, но в текущих языках с АТД (Haskell, Ocaml) такой фокус не прокатит, потому что вызывающая функция должна явно "распаковывать" строковое или численное значение из типа IntString с помощью матчинга на один из конструкторов. Кроме того, по крайней мере в хацкеле, внутри модуля конструкторы уникальны.

T>То есть type IntString объявить действительно несложно и объявить функцию, которая его возвращает, даже неявно — несложно. А вот как вы себе представляете использование такой функции?

Матчинг будет не по конструктору а по типу

let x =
    match x with
    | :? Int as y -> print "is int"
    | :? String as y -> print "is string"

D>>Так же можно обсудить, общую здравость идеи зависимости сигнатуры функции от входящих параметров.

T>Это у кого куда мозг повёрнут. Любители динамики совершенно спокойно мыслят функциями, которые утром возвращают строку, а вечером boolean; любители статики от такого делят на ноль и начинают собирать аргументы против. Мой посыл заключается в том, что здравость (любой) идеи всегда будет оценена субъективно, то есть обсуждение скатится в срач — оно вам надо?
Кто же спорит, кто то любит биться головой об стену, кто то нет. За объективность всегда можно взять мнение большенства, конечно учитывая что большенство может при этом быть не правым.

... << RSDN@Home 1.2.0 alpha 4 rev. 1111>>

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

D>Так же можно обсудить, общую здравость идеи зависимости сигнатуры функции от входящих параметров.

В OCaml есть вещь которая позволяет сделать нечто подобное, полиморфные варианты http://caml.inria.fr/pub/docs/manual-ocaml/manual006.html#toc36

open Printf

let foo x = 
  if x = 0 then `MyInt 0 else `MyStr "bar"
  
  
let print = function
  | `MyInt x -> printf "`MyInt = %d\n" x
  | `MyStr x -> printf "`MyStr = %s\n" x
  | `MyFloat x -> printf "`MyStr = %f\n" x
  
let _ = print (foo 0)
let _ = print (foo 1)

Их не нужно описывать перед использованием и они расширяемые, но как раз ослабляют статическую типизацию, и привносят
в язык динамику http://www.rsdn.ru/forum/decl/4032286.flat.aspx

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

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

D>а) действительно разобраться в том, что такое "алгебраический тип" и почему приведенный вами код никакого к ним отношения не имеет.
D>б) почитать о том, что такое система типов и почему приведенный вами код является классическим (см. того же Пирса) примером кода, который не пропустит любая система типов.
Гонит по обоим пунктам.

D>плюс мне видится это это вполне реализуемое как сахар поверх какого нибудь
Вполне себе вариант.
правда и сигнатуру функции тогда уж описывать так

foo :: int -> X int | Y string
let foo x = if x == 0 then X 0 else Y "bar" end

Ибо вот это:

let x =
    match x with
    | :? Int as y -> print "is int"
    | :? String as y -> print "is string"

Мне определенно не нравится.

... << RSDN@Home 1.2.0 alpha 4 rev. 1472>>

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

Я не понял ни тезиса, ни антитезиса, но можно так

foo :: Int -> Either Int String
foo x = if x == 0 then Left 0 else Right "bar"

Использовать так

> either (+42) length $ foo 0
42
> either (+42) length $ foo 1
3

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

D>Я предлагаю статически типизированое решение, что то похожее на
D>

D>let foo x = if x == 0 then 0 else "bar" end
D>foo :: int -> int | string
D>

Вроде бы в в Typed Scheme (входит в Racket, ранее известный как PLT Scheme) реализовано в точности это, называется union types.

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

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

D>Я не понял ни тезиса, ни антитезиса, но можно так
D>

D>foo :: Int -> Either Int String
D>foo x = if x == 0 then Left 0 else Right "bar"
D>

D>Использовать так
D>

>> either (+42) length $ foo 0
D>42
>> either (+42) length $ foo 1
D>3
D>

Это как раз и есть обобщеный IntString, вопрос можно ли убрать у
data Either a b = Left a | Right b
все имена оставив только a | b

... << RSDN@Home 1.2.0 alpha 4 rev. 1111>>

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

WH>Вполне себе вариант.
WH>правда и сигнатуру функции тогда уж описывать так
WH>

WH>foo :: int -> X int | Y string
WH>let foo x = if x == 0 then X 0 else Y "bar" end
WH>

WH>Ибо вот это:
WH>

WH>let x =
WH>    match x with
WH>    | :? Int as y -> print "is int"
WH>    | :? String as y -> print "is string"
WH>

WH>Мне определенно не нравится.

Чем оно сильно хуже кортежа? У того несколько позиций, у этого одна с несколькими типами. Мне как раз видется
(int | string)
(int , string)
неким подобием замкнутого базиса.

... << RSDN@Home 1.2.0 alpha 4 rev. 1111>>

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

D>Это как раз и есть обобщеный IntString, вопрос можно ли убрать у
D>data Either a b = Left a | Right b
D>все имена оставив только a | b

Ну, отдавая себе отчёт в том, что для дальнейшей унифицированной работы с получившимся хозяйством нужна (упорядоченная) пара функций (a->c)*(b->c), почему бы нет?

T>>Чёрт знает насчёт теоретически возможного, но в текущих языках с АТД (Haskell, Ocaml) такой фокус не прокатит, потому что вызывающая функция должна явно "распаковывать" строковое или численное значение из типа IntString с помощью матчинга на один из конструкторов. Кроме того, по крайней мере в хацкеле, внутри модуля конструкторы уникальны.

T>>То есть type IntString объявить действительно несложно и объявить функцию, которая его возвращает, даже неявно — несложно. А вот как вы себе представляете использование такой функции?

D>Матчинг будет не по конструктору а по типу

D>

D>let x =
D>    match x with
D>    | :? Int as y -> print "is int"
D>    | :? String as y -> print "is string"
D>

Если матчинг обязательный явный, то оно есть уже сегодня, если конструкторы будут названы так же: Int и String. Но я не думаю, что анонимность конструкторов тут самая большая беда. Чтобы воспользоваться значением, его всё-таки придётся из алгебраического типа распаковать — вот что самое неудобное. В динамике "оно само", без лишних switch/match.

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

T>Если матчинг обязательный явный, то оно есть уже сегодня, если конструкторы будут названы так же: Int и String. Но я не думаю, что анонимность конструкторов тут самая большая беда. Чтобы воспользоваться значением, его всё-таки придётся из алгебраического типа распаковать — вот что самое неудобное. В динамике "оно само", без лишних switch/match.
Ну в этом суть статики, нужно переодически подсказывать компилятору что да как, что бы избежать ряда проблем.

... << RSDN@Home 1.2.0 alpha 4 rev. 1111>>

D>def foo(x): if x == 0 then 0 else "bar" end
D>

И что? Даже в динамических языках функции возвращают значения одного и того же типа -- вариантного да, но не изменяемого значениями входных аргументов. foo *не возвращает* разные типы -- она возвращает один тип, просто этот тип допускает строковые и числовые значения.

Вопрос в том -- надо ли нам ограничивать типы насколько возможно (статический случай) или отпустить их насколько возможно (динамические языки). И тут я вижу два аргумента.

Один -- низкоуровневый, для С и подобных.

Сигнатура функции и типы её входных данных -- важная помощь компилятору в оптимизации. Сравните:

int f(int x);
void *f(void *x);

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

Второй -- высокоуровневый.

В таких языках как Haskell эта помощь становится не только помощью компилятору в производительности, но и помощью программисту в формировании абстракции. Рассмотрим пример вашего оппонента -- имея такую функцию ему придётся городить в коде рантаймовую проверку типа, который реально вернула foo на вызове foo(i), и есть шанс забыть, совершить ошибку, использовать не то значение и т.п. в Haskell же достаточно написать Either и сматчить Left / Right, как было показано выше по ветке -- и даже это уже во-первых произойдёт на компиляции во-вторых убережёт от кучи ошибок, в третьих сократит код.

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

Тогда уж и такой полиморфизм изобразить можно было бы

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

let bar i = i + 1
let bar s = s + "\n"

let x1 = foo 0
x1 :: int | string

let x2 = foo 1
x2 :: int | string

//Магия:
let z1 = bar x1
z1 :: int | string

let z2 = bar x2
z2 :: int | string

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

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

A>Тогда уж и такой полиморфизм изобразить можно было бы

:
A>

A>let bar i = i + 1
A>let bar s = s + "\n"
A>//Магия:
A>let z1 = bar x1
A>z1 :: int | string
A>let z2 = bar x2
A>z2 :: int | string
A>

Зачем себя ограничивать ad hoc полиморфизмом, когда можно определить параметрически

mapSum :: (a -> c) -> (b -> d) -> a | b -> c | d

и обслуживать себе любую сумму:

z :: int | string -> int | string
z = mapSum (\i -> i + 1) (\s -> s + "\n")

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

D>Зачем себя ограничивать ad hoc полиморфизмом, когда можно определить параметрически
D>

D>mapSum :: (a -> c) -> (b -> d) -> a | b -> c | d
D>

Плохая идея.
Что будешь делать если понадобиться маписать объедение 3х типов? Еще одну функцию писать?
А если три типа в два? А два в три?

... << RSDN@Home 1.2.0 alpha 4 rev. 1472>>

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

Вроде все тоже самое, можно было остановится на

A>let bar i = i + 1
A>let bar s = s + "\n"

bar :: int | string -> int | string

Тут же как раз работает матчинг по типу.

... << RSDN@Home 1.2.0 alpha 4 rev. 1111>>

Здравствуйте, WolfHound, Вы писали:
Для кортежей тоже приходятся писать новые функции
fst (a,_)
fst (a,_,_)

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

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

D>>Зачем себя ограничивать ad hoc полиморфизмом, когда можно определить параметрически
D>>

D>>mapSum :: (a -> c) -> (b -> d) -> a | b -> c | d
D>>

WH>Плохая идея.
WH>Что будешь делать если понадобиться маписать объедение 3х типов? Еще одну функцию писать?

Зачем, уже написана:

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

Если ещё задать разумную ассоциативность, то

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

WH>А если три типа в два? А два в три?
А это уже другие задачи

	От:	dotneter
	Дата:	27.04.11 16:09
	Оценка:	2 (1)

	От:	Temoto
	Дата:	27.04.11 16:47
	Оценка:	+1

	От:	dotneter
	Дата:	27.04.11 16:57
	Оценка:

	От:	FR
	Дата:	27.04.11 17:08
	Оценка:	6 (2)

	От:	WolfHound
	Дата:	27.04.11 17:20
	Оценка:

От:	Tilir	http://tilir.livejournal.com
Дата:	28.04.11 06:37
Оценка: