Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
К>>Первоначальная идея — _|_ для даты будет 1 для кодаты, и наоборот (1 для даты будет _|_ для кодаты).
L>Поясни, или дай ссылку на то, где писал, а то я сходу не пойму о чём речь.
Чтот найти не могу, в общем идея какая — типизированное ЛИ ты можешь написать на нетипизированном (что ты вроде как и сделал) и наоборот. Написать же обе можно лишь на языке, который будет противоречивым, к примеру на хаскеле с _|_ или, как Charity, на C (с другими проблеммами). В итоге мы нарвёмся или на зацикливание (хотя выполнимая в ТФП фунция такого не сделает) или на ограничения по времени/объёму памяти.
Я понимаю, что аналогия с датой/кодатой фиговая, но вот такая идея.
Здравствуйте, Курилка, Вы писали:
К>Здравствуйте, lomeo, Вы писали:
L>>Здравствуйте, Курилка, Вы писали:
К>>>Первоначальная идея — _|_ для даты будет 1 для кодаты, и наоборот (1 для даты будет _|_ для кодаты).
L>>Поясни, или дай ссылку на то, где писал, а то я сходу не пойму о чём речь.
К>Чтот найти не могу, в общем идея какая — типизированное ЛИ ты можешь написать на нетипизированном (что ты вроде как и сделал) и наоборот. Написать же обе можно лишь на языке, который будет противоречивым, к примеру на хаскеле с _|_ или, как Charity, на C (с другими проблеммами). В итоге мы нарвёмся или на зацикливание (хотя выполнимая в ТФП фунция такого не сделает) или на ограничения по времени/объёму памяти. К>Я понимаю, что аналогия с датой/кодатой фиговая, но вот такая идея.
Ты, когда говоришь про типизированную лямбду, какую вершину лямбда-куба имеешь в виду? Потому что в язычке интерпретатора lomeo типизация ad hoc, простенькая и для одной утилитарной цели — удобства построения интерпретатора.
Здравствуйте, Курилка, Вы писали:
К>Чтот найти не могу, в общем идея какая — типизированное ЛИ ты можешь написать на нетипизированном (что ты вроде как и сделал) и наоборот.
Я сделал нетипизированное на нетипизированном
К>Написать же обе можно лишь на языке, который будет противоречивым, к примеру на хаскеле с _|_ или, как Charity, на C (с другими проблеммами). В итоге мы нарвёмся или на зацикливание (хотя выполнимая в ТФП фунция такого не сделает) или на ограничения по времени/объёму памяти.
Да, типизированное ЛИ (если имеется в виду simply-typed, без fix) невозможно написать на нём самом.
К>Я понимаю, что аналогия с датой/кодатой фиговая, но вот такая идея.
Здравствуйте, deniok, Вы писали:
D>А как их маркировать? Грязь прячем в IO, невозможность полного паттерн матчинга — в Maybe (ну можем, по крайней мере, если не хотим error), а отсутствие гарантий завершаемости?
Не знаю пока. Использованием только data в параметрах, например. Вещественное число не является data, и его использование в функции делает функцию не тотальной (не проверяемой на тотальность). Или специальным ключевым словом, которое будет включать анализ на тотальность.
Да и дело не в маркировке, а в том, что автоматический анализ позволит нам точно узнать какие функции терминируемы.
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, Курилка, Вы писали:
К>>Чтот найти не могу, в общем идея какая — типизированное ЛИ ты можешь написать на нетипизированном (что ты вроде как и сделал) и наоборот. Написать же обе можно лишь на языке, который будет противоречивым, к примеру на хаскеле с _|_ или, как Charity, на C (с другими проблеммами). В итоге мы нарвёмся или на зацикливание (хотя выполнимая в ТФП фунция такого не сделает) или на ограничения по времени/объёму памяти. К>>Я понимаю, что аналогия с датой/кодатой фиговая, но вот такая идея.
D>Ты, когда говоришь про типизированную лямбду, какую вершину лямбда-куба имеешь в виду? Потому что в язычке интерпретатора lomeo типизация ad hoc, простенькая и для одной утилитарной цели — удобства построения интерпретатора.
Если честно — не готов сказать. Да и не уверен, что это тут принципиально. Я ведь не выдвигаю стройную теорию, а лишь озвучиваю свою идею, не более того.
Здравствуйте, Курилка, Вы писали:
G>> Такие функции лучше обернуть в Maybe...
K> тыж вроде монады не разобрал ещё? ???
А при чём здесь монады? ???
Я имел в виду обычный АлгТД Maybe a, у которого два варианта -- допустимое значение (Just a) и отсутствие такового (Nothing).
Вообще-то, для математических pertial-функций можно ввести спецтип, который будет включать PositiveInfinity, NegativeInfinity, Invalide, Valide...
Тогда:
Здравствуйте, geniepro, Вы писали:
G>Вообще-то, для математических pertial-функций можно ввести спецтип, который будет включать PositiveInfinity, NegativeInfinity, Invalide, Valide... G>Тогда: G>
Здравствуйте, lomeo, Вы писали:
L> Ну и будет, что однажды зайдя в Maybe мы уже из него не выйдем, т.е. используя в своей функции функцию с Maybe типом, мы обязаны также вернуть Maybe, ну так чем это отличается от поведения error?
Вовсе не обязательно, это ведь не монада IO... ;о)
Допустим, у нас есть некая функция, результат которой зависит от, например, операции деления, которая на некоторых параметрах этой функции даёт бесконечность.
В зависимости от наших задач у нас есть два варианта:
1) засунуть результат такой функции в Maybe;
2) принять в качестве деления на ноль какое-то дефолтное значение, а результат всей функции считать по-любому нормальным числом.
Здравствуйте, geniepro, Вы писали:
G>Здравствуйте, Курилка, Вы писали:
G>>> Такие функции лучше обернуть в Maybe...
K>> тыж вроде монады не разобрал ещё? ???
G>А при чём здесь монады? ??? G>Я имел в виду обычный АлгТД Maybe a, у которого два варианта -- допустимое значение (Just a) и отсутствие такового (Nothing).
Ага, читаем вики хотябы.
Ёжики кололись, плевались, но не понимали, что использовали монады
В том и суть монад, что так-то это вроде как обычный АлгТД
(хотя тут могу врать, т.к. не знаю точного мат. смысла термина "обычный АлгТД")
Здравствуйте, geniepro, Вы писали:
L>> Ну и будет, что однажды зайдя в Maybe мы уже из него не выйдем, т.е. используя в своей функции функцию с Maybe типом, мы обязаны также вернуть Maybe, ну так чем это отличается от поведения error?
G>Вовсе не обязательно, это ведь не монада IO... ;о)
Э-э-э.. Не понял при чём тут IO.
G>Допустим, у нас есть некая функция, результат которой зависит от, например, операции деления, которая на некоторых параметрах этой функции даёт бесконечность. G>В зависимости от наших задач у нас есть два варианта: G>1) засунуть результат такой функции в Maybe; G>2) принять в качестве деления на ноль какое-то дефолтное значение, а результат всей функции считать по-любому нормальным числом.
Да, я читал статью Тёрнера и знаю об этих вариантах.
Недостаток первого варианта я описал: однажды зайдя в Maybe, мы из него не выйдем.
Недостаток второго: неестественность некоторых результатов операций (как деление на 0, например), которая может привести к ошибкам в логике. Но тут я не поручусь — надо почитать как Runciman разбирается с этой проблемой.
Оба недостатка имеют практический характер. В первом случае неудобно, во втором противоестественно
Здравствуйте, Курилка, Вы писали:
G>>А при чём здесь монады? ??? G>>Я имел в виду обычный АлгТД Maybe a, у которого два варианта -- допустимое значение (Just a) и отсутствие такового (Nothing). К>Ага, читаем вики хотябы. К>Ёжики кололись, плевались, но не понимали, что использовали монады К>В том и суть монад, что так-то это вроде как обычный АлгТД К>(хотя тут могу врать, т.к. не знаю точного мат. смысла термина "обычный АлгТД")
АТД — это сумма произведений, или дизъюнкция конъюнкций
А суть монад в том, чтобы связывать вычисления. Если мы используем fromJust для Maybe вычисления — это уже не монадическое использование и говорить тут о монадах бессмысленно. Если же (как в ТФП) fromJust вещь запрещённая, то нам приходится протягивать значения до конца, т.е. мы получим связку типа Maybe a -> (a -> Maybe b) -> Maybe b — это уже монада.
Простой пример:
(/) :: (Num n) => n -> n -> Maybe n
Допустим мы считаем силу притяжения:
g * (m1 * m2) / (r^2)
Т.к. мы не можем сделать fromJust, то нам приходится тип этого выражения тоже выставлять в Maybe. Теперь допустим, что при расчёте числителя (или знаменателя) тоже используется (/). Значит тип у операции должен быть:
(/) :: (Num n) => Maybe a -> Maybe a -> Maybe n
Теперь предположим, что нам надо сложить что-нибудь с результатом деления (a/b + x). Значит и у операции (+) должен быть типа -> Maybe a. Таким образом, мы приходим к тому, что все операции над числами будут Maybe a -> Maybe a -> Maybe n. Зная это мы можем добавить сахара в язык и читать конструктор 123 как Just 123. Дальше — больше — какие то внешние операции, которые должны принимать только числа (а не Maybe) должны быть описаны с операцией над Nothing тоже:
printNum :: Num n => Maybe n -> IO () -> IO ()
Второй параметр — операция, в случае Nothing. Выделяя комбинатор получим:
catchNothing :: Num n => (n -> a) -> a -> Maybe n -> a
Первый параметр — работа с числом, второй — результат при Nothing, третий — собственно число. Например
printNum :: Num n => n -> IO ()
someExpr :: Num n => Maybe n
printMaybeNumWithErrorMsg = printNum `catchNothing` (print "Error!!")
main = printMaybeNumWithErrorMsg someExpr
Т.е. мы опять таки вернулись к haskell-евскому error Это именно то, о чём я говорю — при использовании Maybe мы получим поведение error. Смысл?
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
G>>>А при чём здесь монады? ??? G>>>Я имел в виду обычный АлгТД Maybe a, у которого два варианта -- допустимое значение (Just a) и отсутствие такового (Nothing). К>>Ага, читаем вики хотябы. К>>Ёжики кололись, плевались, но не понимали, что использовали монады К>>В том и суть монад, что так-то это вроде как обычный АлгТД К>>(хотя тут могу врать, т.к. не знаю точного мат. смысла термина "обычный АлгТД")
L>АТД — это сумма произведений, или дизъюнкция конъюнкций
Ну да, любой первоклассник это поймёт
L>А суть монад в том, чтобы связывать вычисления. Если мы используем fromJust для Maybe вычисления — это уже не монадическое использование и говорить тут о монадах бессмысленно. Если же (как в ТФП) fromJust вещь запрещённая, то нам приходится протягивать значения до конца, т.е. мы получим связку типа Maybe a -> (a -> Maybe b) -> Maybe b — это уже монада.
Т.е. ты считаешь что Монада не может являться АТД? Почему? Или я опять что-то неправильно понял?
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
К>>Т.е. ты считаешь что Монада не может являться АТД? Почему? Или я опять что-то неправильно понял?
L>Неправильно
L>Монада — это то, что использует операцию bind. А АТД это или нет, вопрос десятый.
Ну значит Maybe и то и другое, а geniepro на неё (него?) посмотрел как на АТД, а я(ты?) как на монаду.
В общем — peace
Здравствуйте, lomeo, Вы писали:
L>Э-э-э.. Не понял при чём тут IO.
Ну в смысле, что если в IO попадёшь, то хрен оттуда выберешся (учитывая, что в стандарте Хаскелл-98 нет unsafePerformIO)...
L>Недостаток первого варианта я описал: однажды зайдя в Maybe, мы из него не выйдем.
Почему?
L>Недостаток второго: неестественность некоторых результатов операций (как деление на 0, например), которая может привести к ошибкам в логике. Но тут я не поручусь — надо почитать как Runciman разбирается с этой проблемой.
Рунсиман предлагает два варианта: либо x/0=x, либо x/0=infinity, где infinity=1+infinity
Первый вариант неестественнен, второй запрещён в TFP...
Здравствуйте, lomeo, Вы писали:
L> Если же (как в ТФП) fromJust вещь запрещённая, то нам приходится протягивать значения до конца, т.е. мы получим связку типа Maybe a -> (a -> Maybe b) -> Maybe b — это уже монада.
Ладно, к чёрту Maybe, забудем об этом типе, что бы не съезжать не туда из-за ненужных ассоциаций...
И fromJust тоже туда же, в (_|_)...
Создадим новый, простенький тип MathResult:
data MathResult a = Invalid | Valid a
L> Простой пример: L> (/) :: (Num n) => n -> n -> Maybe n
L> Допустим мы считаем силу притяжения: L> g * (m1 * m2) / (r^2)
Можно поступить не только так (Ваш пример не показателен, примем, например, расчёт корней кв. ур.):
class Num n where
(+), (-), (*) :: n -> n -> n
class (Num n) => Floating n where
(/) :: n -> n -> MathResult n
sqrt :: n -> MathResult n
roots :: Double -> Double -> Double -> (MathResult Double, MathResult Double)
roots a b c = (x1, x2)
where
d = sqrt (b*b - 4*a*c)
e = 1 / (2*a)
(x1, x2) = case d of
Invalid -> (Invalid, Invalid)
Valid d -> case e of
Invalid -> (Invalid, Invalid)
Valid e -> (Valid (((-b)+d)/e), Valid (((-b)-d)/e))
Ужос получился. :о))
Вапще-то в данной задаче другого варианта поведения вроде как и не предусмотрено, а более подходящего примера в голову не идёт, блин...
Однако предположим, что задача позволяет подставлять вместо d и e какие-то дефолтные значения в случае их невалидности. Тогда эта функция вполне может вернуть не MathResult Double, а просто Double... Неужели так трудно представить такой вариант?
