LINUX.ORG.RU

[scheme][haskell][oop][fp] Мысли вслух

 , ,


5

7

Была на ЛОРе такая тема — [Haskell] простой вопрос. Хотелось бы немножко её развить и высказаться на тему предпочтения того или иного языка при изучении ФП (графомания mode on :)).

У Scheme есть довольно давняя история использования в качестве подопытного языка в курсах изучения ФП. Я не знаю чем это вызвано, но факт остаётся фактом — есть известный курс у MIT (или был?) и разные полезные книжки — SICP, HTDP, PLAI, OOPLAI, которые обычно и советуют читать если нужно ознакомиться с ФП.

Касательно SICP — одним из сторонников использования ML для целей изучения ФП была написана статья (http://www.cs.kent.ac.uk/people/staff/dat/miranda/wadler87.pdf) в которой достаточно хорошо освещены некоторые недостатки Scheme. Если говорить про Haskell, то тут всё так же. Далее, по пунктам (опуская кое-что из того что уже было в той статье).

Более явный синтаксис

Вместо

(define (foo x y z)
  (if (> (+ x (* y z) 1) 7) (print (+ x y)) (print (- x y))))

будет

foo x y z = if x + y * z + 1 > 7 then print $ x + y else print $ x - y

при этом по-прежнему можно написать выражение в префиксной форме:

(if' ((>) ((+) x ((*) y z) 1) 7) (print ((+) x y)) (print ((-) x y)))

почти как в Scheme. То есть, кроме префикса также есть (расширяемый пользователем) инфикс (в том числе функции вроде ($) и (.) позволяющие в некоторых случаях опускать лишние аргументы у функций и некоторые скобки в выражениях) и разные специальные формы (вроде if, let, лямбды и т.п.). Во всём что не касается макросов это более удобно. S-выражения обретают свой особый смысл только когда доходит до их цитирования:

'(if (> (+ x (* y z) 1) 7) (print (+ x y)) (print (- x y)))

и разбора с целью написания макросов. Тем не менее, для изучения именно ФП эта возможность незначительна (ФП не про макросы, в SICP и HTDP не ни слова про макросы, в PLAI есть только немного, в OOPLAI — побольше). Про то как правильно (ну, _правильно_, то есть без использования s-выражений) организовывать символьные вычисления (вроде дифференцирования из SICP) также расказывается в упомянутой статье.

Каррированные функции

Такое определение, например:

(define add
  (lambda (n)
    (lambda (m)
      (+ m n))))

заменяется простым

add = (+)

так как все функции уже каррированные (позволяют частичное применение). Фактически, в хаскеле функция с n аргументами сразу задаёт n разных функций (выбор конкретной функции осуществляется во время компиляции и не имеет эффекта во время выполнения). Некаррированные функции это функции от кортежей (те и другие переводятся друг в друга с помощью ФВП carry/uncarry).

Частичное применение, секции, pointfree запись

add2 = (+ 2)

add2 5
7

вместо

(define add2 (add 2))

(add2 5)
7

Мутабельные замыкания

Это единственная вещь которая есть в Scheme и которую можно не увидеть сразу в хаскеле (и про неё нет в той статье). Тот тред был как раз про них. Чтобы прояснить этот момент, ниже приводятся некоторые примеры из OOPLAI и их аналоги на хаскеле.

Простейший вариант:

(define counter
  (let ((count 0))
    (lambda ()
      (begin
        (set! count (add1 count))
        count))))

(counter)
1
(counter)
2

аналог:

counter = (=~ (+ 1)) <$> new 0

тут (=~ (+ 1)) играет роль мутирующего «метода», а (new 0) — мутируемого «объекта», (<$>) — применение «диспетчера» (тут — просто единичный анонимный «метод»). Вся конструкция функториальная (не монадическая). Использование:

ctr <- counter      -- Инстанцирование класса counter объектом ctr.
ctr                 -- Применение единственного метода ((=~ (+ 1)) который).
1                   -- Результат.
ctr                 -- Снова.
2                   -- Другой результат.

Чуть более сложный пример:

(define counter-
  (let ((count 0))
    (lambda (cmd)
      (case cmd
        ((dec) (begin
                 (set! count (sub1 count))
                 count))
        ((inc) (begin
                 (set! count (add1 count))
                 count))))))

(counter- 'inc)
1
(counter- 'dec)
0

Для начала определим имена методов dec и inc:

data CounterMethod = Dec | Inc

это не символы и не строки (так что код не будет ill-typed как в примере на Scheme, иначе говоря, применение несуществующего метода не пройдёт компиляции). И теперь функцию:

counter' = dispatch <$> new 0
  where dispatch obj Dec = obj =~ flip (-) 1
        dispatch obj Inc = obj =~ (+ 1)

тут dispatch играет роль диспетчеризирующей функции которая получает объект (obj) и имя метода, а затем изменяет объект (как того требует метод). (new 0) — начальный объект.

Пример:

ctr <- counter'     -- Инстанцирование класса counter' объектом ctr.
ctr Inc             -- Применение метода Inc на объекте ctr.
1
ctr Inc
2
ctr Inc
3
ctr Dec             -- Тут уже метод Dec.
2
ctr Dec
1
ctr Dec
0

Тут применение (ctr Inc) весьма похоже на каноничное, через точку, obj.method и является, по сути, посылкой сообщения объекту.

Третий пример:

(define stack
  (let ((vals '()))
    (define (pop)
      (if (empty? vals)
          (error "cannot pop from an empty stack")
        (let ((val (car vals)))
          (set! vals (cdr vals))
          val)))
    (define (push val)
      (set! vals (cons val vals)))
    (define (peek)
      (if (empty? vals)
          (error "cannot peek from an empty stack")
        (car vals)))
    (lambda (cmd . args)
       (case cmd
         ((pop) (pop))
         ((push) (push (car args)))
         ((peek) (peek))
         (else (error "invalid command")))))) 

(stack 'push 1)
(stack 'push 2)
(stack 'pop)
2
(stack 'peek)
1
(stack 'pop)
1
(stack 'pop)
; cannot pop from an empty stack

аналогично:

data StackMethod = Pop | Push | Peek

stack = dispatch <$> new []
  where
    dispatch x Pop _  = get x >>= (x =~ tail >>) . return . head
    dispatch x Push y = x =~ (y :) >> return y
    dispatch x Peek _ = head <$> get x

и пример:

stk <- stack :: IO (StackMethod -> Int -> IO Int)
                    -- stack это параметрически-полиморфный класс, в данном
                    -- случае берётся его спецификация когда элементы стека
                    -- имеют тип Int (можно взять что-то более общее).
                    -- Этот специфичный класс инстанцируется объектом stk.
mapM_ (stk Push) [1, 2, 3]
                    -- (stk Push) это применение метода Push на объекте stk,
                    -- с помощью ФВП mapM_ оно производится для всех элементов
                    -- списка.
repeat 4 $ stk Pop __ >>= print
                    -- 4 раза вызывается метод Pop, элементы печатаются.
                    -- Последний раз вызывается исключение (так как стек пуст).
3
2
1
*** Exception: Prelude.head: empty list

тут точно так же — в StackMethod перечислены нужные методы для стека, функция stack определяет класс, то есть объединение данных и функций с нужным поведением, она имеет тип IO (StackMethod -> a -> IO a), то есть принимает метод, элемент стека и возвращает элемент стека (в IO, мутабельно), сама функция в IO (вся структура данных ведёт себя мутабельно).

Дальше в OOPLAI начинают использовать макросы для придания более удобоваримого вида этим конструкциям. В настоящем (ну, _настоящем_ :)) ФП этого не нужно — примитивные ООП конструкции объединяющие данные и функции выглядят естественно и так, и являются частным случаем использования ФВП, IO и ADT с паттерн-матчингом (последние два — для удобства). Использование макро-системы может иметь смысл разве что если действительно нужно реализовать сложную ООП систему (например, со множественным наследованием и изменяемой иерархией классов, впрочем, обойтись одними функциями тут тоже можно, просто придётся делать больше механических действий).

Ещё пример:

-- | Данные — конструктор и аккессоры.
data Point = Point
  { x :: Double
  , y :: Double
  } deriving ( Show, Eq ) -- ad-hoc перегруженные функции.

-- | Методы привязываемые к данным (это уже _не_ ad-hoc перегруженные функции).
data PointMethod = Pos | Mov

-- | Класс (= функция), объединяющий данные и методы.
pointClass :: Double -> Double -> IO (PointMethod -> Double -> Double -> IO Point)
pointClass initX initY = dispatch <$> new (Point initX initY)
  where
    -- | (Динамический) диспетчер по методам. Он принимает объект (Var Point),
    -- имя метода (PointMethod, т.е. статическое, в данном случае, сообщение)
    -- и два опционных аргумента для методов (Double -> Double). Эту функцию
    -- можно помещать непосредственно в Point.
    dispatch :: Var Point -> PointMethod -> Double -> Double -> IO Point
    dispatch obj Pos _ _ = get obj
    dispatch obj Mov x y = obj =: Point x y
pnt <- pointClass 2 4         -- Инстанцирование класса pointClass объектом pnt
                              -- с начальными значениями полей 2 и 4.
:t pnt
pnt :: PointMethod -> Double -> Double -> IO Point
pnt Pos __ __                 -- Вызов метода Pos на объекте pnt.
Point {x = 2.0, y = 4.0}
pnt Mov 3 5                   -- Вызов метода Mov.
Point {x = 3.0, y = 5.0}
pnt Pos __ __                 -- Положение изменилось:
{x = 3.0, y = 5.0}

Нужно заметить, что это всё довольно примитивные конструкции (простые функции и IO). В случае использования ADT для имён методов получится динамическая диспетчеризация с фиксированным набором методов (well-typed), если же переписать функцию dispatch с завязкой на хэш-табличку (которая должна быть переменной в данных класса), то будет динамическая диспетчеризация с пополняемым набором методов и перегруженными методами (одни и те же сообщения можно посылать разным инстанцированным объектам, их dispatch будет их искать в хэш-таблице и обрабатывать, это уже ill-typed, то есть с исключениями вида «нет такого метода»). Разные прочие вещи вроде наследования и self точно также можно изобразить (аггрегация данных, представление иерархии классов в данных (в переменной или нет, в зависимости от возможности менять иерархию) и более сложная функция dispatch), но как-то не интересно.

P.S.

Код на хаскеле использует такие упрощения:

import Prelude hiding ( repeat )
import Data.IORef
import Control.Applicative
import Control.Monad

type Var a = IORef a

new :: a -> IO (IORef a)
new = newIORef

get :: IORef a -> IO a
get = readIORef

(=~) :: IORef a -> (a -> a) -> IO a
x =~ f = modifyIORef x f >> get x

(=:) :: IORef a -> a -> IO a
x =: x' = x =~ const x'

repeat :: Monad m => Int -> m a -> m ()
repeat = replicateM_

__ :: a
__ = undefined

P.P.S.

OOP / ООП в контексте данного поста — объектно-ориентированное программирование в духе объединения данных и процедур, то есть в духе C++, Java, Python и т.п. _Не_ ООП в духе классы = структуры, методы = перегруженные функции, наследование = схемы агрегаций и распространения методов (как это в CLOS и классах типов Haskell).

★★★★

Ответ на: комментарий от Miguel

А куда конкретнее? У тебя была написана нечитаемая фигня изобретёнными тобой криптографическими обозначениями.

Почему мной? Стандартная схемовская нотация.

Тогда дай ссылку, грамотей.

Читай тред, я не намерен делать за тебя твою работу.

anonymous
()
Ответ на: комментарий от anonymous

В каком именно смысле и с какими именно оговорками можно работать как с функциями в хаскеле.

Можно работать до тех пор, пока не получим противоречие модели с предметной областью. То есть до тех пор, пока свойства, которыми обладают мат. функции, не станут противоречить свойствам, которым обладают соответствующие термы.

anonymous
()
Ответ на: комментарий от anonymous

у него там во второй ветке ифа 1+f, без аппликации

Ну он спросил - почему не работает и как сделать правильно. Конечно, сначала мы перепишем nonsence 1 + f в f . (+ 1), а потом скажем, почему не работает (бесконечные типы).

quasimoto ★★★★
() автор топика
Ответ на: комментарий от anonymous

Почему мной? Стандартная схемовская нотация.

«curry :: narg -> 1arg» - это стандартная схемовская нотация?

Читай тред, я не намерен делать за тебя твою работу.

Понятно, слив защитан.

Miguel ★★★★★
()
Ответ на: комментарий от quasimoto

Ну и сказать как сделать правильно (явная рекурсия на типах). Причём, смотри, при попытке сделать элементарную вещь в хаскеле неправильно начинается такая ерунда (ты должен _явно_ запрограммировать бесконечный тип, а какой-нибудь лисп проглотил бы такое определение и не подавился), потому что элементарные вещи нужно делать правильно (сумма списка чисел это sum). Гораздо интереснее, что в хаселе есть много неэлементарных вещей (как в языке - система типов высшего порядка, вывод типов, классы типов, фун. зависимости, GADTs и т.п., так и в среде - лёгкая конкурентность, STM, раздельная компиляция и т.д.), которых в абстрактных «конка-что-то-там» языках не дождёшься.

quasimoto ★★★★
() автор топика
Ответ на: комментарий от anonymous

Ну мы знаем как ЯП без типов (лисп)

В лиспе куча латентных типов (и соответствующих тайп-тегов), тип Т, разные его подтипы, классы в CLOS, вывод типов в CMUCL/SBCL.

так и без редукций (хаскель)

Не смешно (http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/, хотя бы).

quasimoto ★★★★
() автор топика
Ответ на: комментарий от anonymous

Авторитетный источник, в котором будет что?

ну как маленький, естественно книга или статья в реферируемом источнике.

Определение функции curry?

да

Попросили определение - я дал определение. Чем оно тебя не устраивает?

Даже если забить на то, что оно на птичьем языке, и вне контекста теоретической базы (формализма), данное определение не устраивает тем, что нету ссылки на источник, в котором это определение описано. Что такое авторитетный источник написано выше.

qnikst ★★★★★
()
Ответ на: комментарий от anonymous

Нет, мы просто говорим о лямбдах от нескольких аргументов. Вне рамок какого-то конкретного ЯП.

Хочешь сказать, что существуют «просто лямбды» вне контекста ЯП и вне контекста лямбда исчисления (где есть только (\x . t), а (\x y . t) это сахар для (\x . (\y . t)))? Конечно, такое можно увидеть в моделях языков (у Харрисона или Пирса, например), но я об этом и говорю (лямбды и аппликации от нескольких аргументов в определении термов).

Неправильно! В хаскеле есть некоторая ф-я, которая называется curry, есть определенная модель ф-й хаскеля в ТК

Всё не так. curry в TK это полностью самодостаточная вещь, связанная с экспоненциалами и декартово-замкнутыми категориями. Где про неё можно почитать - Р. Голдблатт, «Топосы. Категорный анализ логики», 3.16; B. Pierce, «Basic category theory for computer scientists», 1.10; John C. Baez, Mike Stay, «Physics, Topology, Logic and Computation: A Rosetta Stone», несколько публицистично, в части про computation; wikipedia - CCC, Exponential, Currying, Apply. ССС это весьма общее понятие, так что curry тоже весьма общее, первичное, понятие - в категории Set (и в теории множеств вообще) это будет часть биекции, устанавливающей известный изоморфизм между A × B → C и A → [B → C], где [B → C] это функциональное пространство функций из B в C, в логике curry будет что-то другое, в квантовой физике - что-то третье (см. Baez & Stay), в моделях ЯП в CS основанных на лямбда исчислении это будет что-то вроде функции каррирования в хаскеле. И всё связанно Curry–Howard–Lambek (и т.д.) correspondence.

Вот это нормальная (в моём понимании) curry, что такое нормальная curry в твоём понимании? Вроде как, формальные (тем более категорные) модели лиспов строить не принято, нормальная curry это curry в лиспе? (не в теории категорий, не в теории множеств, не в логике, и не в лямбда исчислении).

quasimoto ★★★★
() автор топика
Ответ на: комментарий от anonymous

Функция curry (определяемое понятие) - это такая функция (общее понятие), что

Я знаю что нужно сделать, чтобы завершить этот спор - написать код curry на scheme (на голом R5RS, желательно), написать две _разных_ (математически, т.е. под observational equality) функции f и g и показать, что (curry f) и (curry g) это _одна и та же_ функция (в смысле observational equality). Тогда можно согласится, что, да, в scheme можно написать какую-то странную curry :). Могу предполагать, что если такое возможно, то это связанно с тем, что нет системы типов не позволяющей перепутать функции из классов a × b → z и a × b × c → z, например.

quasimoto ★★★★
() автор топика
Ответ на: комментарий от anonymous

Ок, еще одна переформулировка. Когда получим противоречие модели с предметной областью в схеме? Когда получим противоречие модели с предметной областью в хаскеле? Когда свойства, которыми обладают мат. функции, станут противоречить свойствам, которым обладают соответствующие термы в схеме? Когда свойства, которыми обладают мат. функции, станут противоречить свойствам, которым обладают соответствующие термы в хаскеле?

anonymous
()
Ответ на: комментарий от quasimoto

Ну он спросил - почему не работает и как сделать правильно. Конечно, сначала мы перепишем nonsence 1 + f в f . (+ 1), а потом скажем, почему не работает (бесконечные типы).

Этак получится ответ на вопрос «почему не работает f. (+ 1)», а не «почему не работает 1 + f» - то есть совсем другой вопрос.

anonymous
()
Ответ на: комментарий от Miguel

«curry :: narg -> 1arg» - это стандартная схемовская нотация?

Можешь вообще эту строку из определения убрать - ничего не изменится. Она там тольк для пояснения.

кококо

Что, простите?

anonymous
()
Ответ на: комментарий от quasimoto

потому что элементарные вещи нужно делать правильно

Не надо выдавать за «правильность» ограниченность конкретного хаскеля.

которых в абстрактных «конка-что-то-там» языках не дождёшься.

А зачем они нужны? Инструмент не является ценным сам по себе. Только в рамках приложения к какой-то задаче. Пока что известны факты того, как инструмент мешает (заставляет использовать неудобные и неочевидные «правильные» методы вместо естественных решений). А вот помогает - где?

anonymous
()
Ответ на: комментарий от quasimoto

В лиспе куча латентных типов (и соответствующих тайп-тегов), тип Т, разные его подтипы, классы в CLOS, вывод типов в CMUCL/SBCL.

Ок, без статических типов. То есть модель вычисления лиспа основана на нетипизированной лямбде.

Не смешно (http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/, хотя бы).

Там есть _операционная_ семантика хаскеля? Ведь без нее о наличии «редукций» в ЯП, понятное дело, говорить нельзя.

anonymous
()
Ответ на: комментарий от qnikst

да

Ок, приведи мне книгу или статью с определением curry в реферируемом источнике. Кстати, надо понимать, что если в реферируемом источнике не окажется определения Х, то Х не существует? Например - я уверен, не существует ни одного реферируемого источника с определением числа 8976589768958. Что из этого следует, не объяснишь?

anonymous
()
Ответ на: комментарий от anonymous

Можешь вообще эту строку из определения убрать - ничего не изменится. Она там тольк для пояснения.

Не надо усложнять определения чисто для пояснения.

Что, простите?

Сам сказал, сам не понял, а меня почему-то спрашивает.

Miguel ★★★★★
()
Ответ на: комментарий от quasimoto

З.Ы. чтобы пейсать программы, очевидно же :)

quasimoto ★★★★
() автор топика
Ответ на: комментарий от quasimoto

Хочешь сказать, что существуют «просто лямбды» вне контекста ЯП и вне контекста лямбда исчисления (где есть только (\x . t), а (\x y . t) это сахар для (\x . (\y . t)))?

Кто тебе мешает рассмотреть это дело в контексте лямбда-исчисления, где это _не_ сахар?

Всё не так. curry в TK это полностью самодостаточная вещь, связанная с экспоненциалами и декартово-замкнутыми категориями.

Ну а можем выбрать другую, неинъективную curry, и ничего существенно не изменится.

Вот это нормальная (в моём понимании) curry, что такое нормальная curry в твоём понимании?

Не понял. Ты своего определения curry так и не дал, рассказываешь что-то про ТК и т.п.. Мы уже установили, что ТК не первична, первичен ЯП и его термы. Которые, (если нам повезет) мы можем моделировать теоретико-(категорными|множественными) объектами. Но определения теоретико-(категорных|множественных) объектов не являются определениями объектов, которые они моделируют. Это мы должны взять моделируемый объект, взять модель - и доказать, что они эквивалентны. То есть начинаем мы именно от термов, и curry в моем понимании - определенный терм, удовлетворяющий определенным свойствам. Каким именно - я уже написал.

нормальная curry это curry в лиспе?

Нормальная curry - это терм. Не модель терма, а терм. В первую очередь. Какое там определение у модели нас не ебет. Так понятно?

anonymous
()
Ответ на: комментарий от anonymous

Когда получим противоречие модели с предметной областью в схеме? Когда получим противоречие модели с предметной областью в хаскеле?

Заранее этого никто не сможет сказать.

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

аналогично.

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

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

anonymous
()
Ответ на: комментарий от Miguel

Не надо усложнять определения чисто для пояснения.

А я и не усложнял.

anonymous
()
Ответ на: комментарий от quasimoto

Сильная система типов

Зачем?

лёгкая конкурентность, STM

Статика здесь не нужна.

раздельная компиляция?

Статика здесь не нужна.

Вывод?

anonymous
()
Ответ на: комментарий от Miguel

И да, что в твоём «определении» подразумевается под словом «функция»?

Смотри выше по треду, написано не раз.

anonymous
()
Ответ на: комментарий от anonymous

Кто тебе мешает рассмотреть это дело в контексте лямбда-исчисления, где это _не_ сахар?

Не кто, а что. Отсутствие такого варианта лямбда-исчисления.

anonymous
()
Ответ на: комментарий от anonymous

Т.е. вы не знаете, почему функции в хаскеле нельзя моделировать функциями в математическом смысле? И не знаете, чем функция в хаскеле отличается от процедуры в схеме? Просто решили это незнание в такой витиеватой форме выразить?

anonymous
()
Ответ на: комментарий от anonymous

Кто тебе мешает рассмотреть это дело в контексте лямбда-исчисления, где это _не_ сахар?

Ссылки на публикации про _такое_ лямбда исчисление?

Ну а можем выбрать другую, неинъективную curry, и ничего существенно не изменится.

Ну да, а можно под ζ(n) понимать функцию не имеющую ничего общего с дзета-функцией, «и ничего существенно не изменится» (?). Речь о том, что curry в ТК одна, фундаментальна, и других curry там нет.

Ты своего определения curry так и не дал, рассказываешь что-то про ТК и т.п.

У меня нет «своей» curry, я знаю только о curry из ТК и её приложений (в теории множеств, логике и т.п.). Соответственно, это для меня такой критерий правильности - язык должен реализовывать именно такую, строго определённую, curry. Если язык вообще не следует каким-то строгим определениям и реализует curry с произвольными, отличными от общепринятых, свойствами, то об этом вообще нет смысла говорить (сравнивать тёплое с мягким - формальное с неформальным).

То есть начинаем мы именно от термов

Я думал, что термы определимы только в рамках какой-то модели. Что за «термы» вне контекста модели? Нужно сначала установить _модель_ (теоретико-множественную или теоретико-категорную) и сказать «в рамках это модели терм это и т.д.».

Нормальная curry - это терм. Не модель терма, а терм. В первую очередь. Какое там определение у модели нас не ебет. Так понятно?

Ага, curry это некая НЁХ. Так понятно :)

quasimoto ★★★★
() автор топика
Ответ на: комментарий от anonymous

Ок, приведи мне книгу или статью с определением curry в реферируемом источнике.

quasimoto тебе уже N-раз приводил при ссылаясь на нормальные источники

Кстати, надо понимать, что если в реферируемом источнике не окажется определения Х, то Х не существует?

1). если определение объекта не выводится из других определений правил и т.д.

2). не несуществует, а неопределено, очевидно же.

Например - я уверен, не существует ни одного реферируемого источника с определением числа 8976589768958.

я уверен, что существует определение пространства натуральных чисел и полные и непротиворечивые правила записи натуральных чисел знаками [0-9], так, что число 897658976958 определено.

то из этого следует, не объяснишь?

то, что ты приводишь некорректные аналогии, и то что у тебя проблема с формальной логикой.

qnikst ★★★★★
()
Ответ на: комментарий от anonymous

А я и не усложнял.

Ты смешал синтаксис двух языков программирования, добавил своих собственных измышлений (типа слова «narg»), и обозвал это почему-то «определением».

Статика здесь не нужна.

Интересно. Покажешь, как сделать STM без статики?

Смотри выше по треду, написано не раз.

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

Miguel ★★★★★
()
Ответ на: комментарий от anonymous

Зачем?

А зачем нужен -Wall и прочие turn on all warnings в других языках? Compile-time verification даже в форме системы типов это тоже такая полезная фича.

Вывод?

Посыл был в том, что у хаскеля есть не только такой-то проработанный backgound (но такой негодный, не то что в языках основанных на комбинаторной форме лямбда исчисления, с динамической системой типов и т.п. - о чём ты начал говорить), но и, например, развитая реализация, библиотеки, сообщество (а что тут у языков основанных на комбинаторной форме лямбда исчисления, с динамической системой типов и т.п.? Зато можно написать 1 + f, что бы это ни значило).

quasimoto ★★★★
() автор топика
Ответ на: комментарий от Macil

Что за языки такие?

Это я перепутал, anonymous говорил:

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

Допустим в хаскеле надо f . g, f .: g и так далее, в конкантенативном ЯП этого ничего не надо. Просто пишем g f. и никаких комбинаторов определять тоже не надо. Тут суть простая - базовая операция аппликативных языков - это аппликация f x. А аппликация производится к аргументам. Базовая операция конкантенативных языков - это обратная композиция. И она записывается так же - f g. Поинт-фри в аппликативных ЯП изначально ущербно, потому что мы все равно никуда не можем уйти от аппликаций. Определение любой ф-и все ранво необходимо задавать через аппликацию, никаких других способов нет.

не комбинаторные (вроде unlambda) а конкатенативные (вроде forth).

quasimoto ★★★★
() автор топика
Ответ на: комментарий от quasimoto

Вот есть форт, фактор и другие конкантенативные ЯП, которые основаны на комбинаторной логике

Кстати, ?

quasimoto ★★★★
() автор топика
Ответ на: комментарий от anonymous

Не кто, а что. Отсутствие такого варианта лямбда-исчисления.

С чего вдруг он отсутствует?

anonymous
()
Ответ на: комментарий от quasimoto

Ссылки на публикации про _такое_ лямбда исчисление?

Не понял, зачем? Это заразно что ли? Если не существует публикации с упоминанием X, то X не существует? По-моему, в математике существует все то, существование чего можно вывести из аксиом. При чем тут публикации?

Ну да, а можно под ζ(n) понимать функцию не имеющую ничего общего с дзета-функцией, «и ничего существенно не изменится» (?). Речь о том, что curry в ТК одна, фундаментальна, и других curry там нет.

Ну а не в ТК могут быть другие curry.

У меня нет «своей» curry, я знаю только о curry из ТК и её приложений (в теории множеств, логике и т.п.).

То есть в хаскеле никакой curry нет. Ок.

Если язык вообще не следует каким-то строгим определениям и реализует curry с произвольными, отличными от общепринятых

А общепринятые - это какие?

Я думал, что термы определимы только в рамках какой-то модели.

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

Нужно сначала установить _модель_ (теоретико-множественную или теоретико-категорную) и сказать «в рамках это модели терм это и т.д.».

Для того, чтобы констатировать факт «камень упал» нам не нужно модели гравитационного поля.

Ага, curry это некая НЁХ. Так понятно :)

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

anonymous
()
Ответ на: комментарий от qnikst

quasimoto тебе уже N-раз приводил при ссылаясь на нормальные источники

Конкретную ссылку. Типа «curry в хаскеле - это то то то».

1). если определение объекта не выводится из других определений правил и т.д.

Ну так я свое определение curry и вывел из существующих определений/правил етк. в чем проблема?

Есть аксиомы, выводим из этих аксиом существование некоего объекта и присваиваем ему имя Х. Никаких научных публикаций для этого не нужно. Вообще говоря и доказательство существования не нужно - можно просто дать определение, назвать объект и потом ставить вопрос его существования. Например «назовем множество всех множеств НЕХ, существует ли НЕХ?»

я уверен, что существует определение пространства натуральных чисел и полные и непротиворечивые правила записи натуральных чисел знаками [0-9], так, что число 897658976958 определено.

Хорошо, дай определение числу 897658976958.

то, что ты приводишь некорректные аналогии, и то что у тебя проблема с формальной логикой.

Ты немного перепутал.

anonymous
()
Ответ на: комментарий от Macil

Ну, тогда любой комбинаторный парсер - конкатенативный ЯП.

Комбинаторные парсеры тоже применяются при помощи аппликаций.

anonymous
()
Ответ на: комментарий от quasimoto

Да, я несколько поторопился. В комбинаторных ЯП (типа унлямбды) есть аппликация, но нету лямбд. В конкантенативных нету аппликации, но, в принципе, могут быть лямбды.

anonymous
()
Ответ на: комментарий от anonymous

Не понял, зачем? Это заразно что ли? Если не существует публикации с упоминанием X, то X не существует? По-моему, в математике существует все то, существование чего можно вывести из аксиом. При чем тут публикации?

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

Ну а не в ТК могут быть другие curry.

не в ТК, а где? Ссылки/описание формализма с базовым набором аксиом в студию. А то есть такая curry, которая приходит на кухню и посывает карри всю еду, но блин в лиспах и схемах не такая карри! она не настоящая! этот недоязык ничего не позволяет!

Определение: карри это такая функция T, что для каждого объекта (e) из множества еды (E), находящегося на кухне K, переводит объект в пространство еды посыпанной карри (С) формально:

T: \forall (e \in E), K(e) = True => T(e) \in C

базовые свойства T(T(e)) = id

А общепринятые - это какие?

опирающиеся на существующие теории в рамках, которых есть и другие работы (ТК подойдёт)

Нет-нет-нет. Термы - не модель, термы - это то, для чего мы пишем модель.

ну и кашища....

Для того, чтобы констатировать факт «камень упал» нам не нужно модели гравитационного поля.

но нужна модель, в которой мы можем определить, что такое «камень», что такое «упал». А то вот мне, например, кажется, что камень начал движение по окружности вокруг центра Земли, какое тут нафиг упал?

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

ха-ха-ха!

qnikst ★★★★★
()
Ответ на: комментарий от anonymous

Конкретную ссылку. Типа «curry в хаскеле - это то то то».

В хацкеле curry из ТК, в ТК curry это: (с википедии)

Given a function f of type \scriptstyle f \colon (X \times Y) \to Z , currying it makes a function \scriptstyle \text{curry}(f) \colon X \to (Y \to Z) . That is, \scriptstyle \text{curry}(f) takes an argument of type \scriptstyle X and returns a function of type \scriptstyle Y \to Z . Uncurrying is the reverse transformation, and is most easily understood in terms of its right adjoint, apply.

так же читай Schönfinkel, Moses (1924). «Uber die Bausteine der mathematischen Logik»

Ну так я свое определение curry и вывел из существующих определений/правил етк. в чем проблема?

ну если ты не допустил ошибок, то твоя карри неинективна. Но какое это имеет отношение к реальности то?

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

статьи нужны для того, чтобы потом общаться с другими и другие могли понять о чём ты говоришь. Ещё раз ТВОЯ карри неинцективна, для ТВОЕЙ карри не существует обратной функции, ТВОЮ un-карри нельзя реализовать на haskell. В хацкеле curry из ТК, она инъкетивна, существует обратная функция и реализована uncurry. ТВОЕЙ теории не придерживается никто кроме тебя, ТК разработанная уже много лет теория. Вопрос, с чего бы вдруг ТВОЯ карри была «более настоящая» чем карри в haskell?

Хорошо, дай определение числу 897658976958.

не тупи, а.

qnikst ★★★★★
()
Ответ на: комментарий от Miguel

Интересно. Покажешь, как сделать STM без статики?

Clojure. Хаскелисты как всегда предпочитают ворочанию мешков кое-что другое.

unlog1c ★★★
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.