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

Я правильно понимаю, что Clojure не энфорсит это ограничение?

Clojure энфорсит это на уровне своего языка. Т.э. языковые средства для изменения состояния ref'ом не скомпилируются, если их вызвать извне dosync-блока. Но из-за Джавовского начала Clojure ничего не сможет поделать, если пользователь вызовет метод, который изменяет Java-вскую мутабельную структуру данных. Скажем ты поместил в ref экземпляр джавовского ArrayList'а и вне синк-блока вызвал ему clear(). Тут уже ССЗБ.

Все родные кложуровские структуры данных иммутабельны, естественно.

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

Т.э. языковые средства для изменения состояния ref'ом не скомпилируются, если их вызвать извне dosync-блока.

О. Круто. Надо будет изучить повнимательнее.

Но из-за Джавовского начала Clojure ничего не сможет поделать, если пользователь вызовет метод, который изменяет Java-вскую мутабельную структуру данных.

Не, ну, это-то понятно. Любой FFI ломает всякие языковые гарантии.

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

Не понял, зачем?

Затем, что может хоть там будет определение функции многих аргументов но без произведений. Потому что иначе не понятно о чем вы говорите.

Да, по поводу незнания отличия функций в хаскеле и процедур в схеме комментарии будут или ваши возражения по моделированию функций хаскеля математическими ф-ями снимаются?

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

Если не существует публикации с упоминанием X, то X не существует?

Ну типа того. По крайней мере, тебе будет не на что сослаться в дискуссии - нужны публикации, общепринятость (и чтобы это не были какие-нибудь очередные «торсионные поля»), традиция использования такого определения в научной литературе, в крайнем случае нужно твоё собственное построение (но тут не тот случай - речь идёт о целых моделях / теориях в которых есть лямбды отличные от типичных в ЛИ лямбд, curry отличная от типичной curry и т.д., просто пост на форуме это не тот формат, чтобы определять такие вещи - проще на что-то сослаться).

По-моему, в математике существует все то, существование чего можно вывести из аксиом.

А кто выводить будет? anonymous? :)

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

Где?

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

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

Можно ещё так:

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

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

Я же говорю - теория множеств, логика, ЛИ, ЯП основанные на ЛИ, ТК.

Термы ЯП (в написанных программах) нам даны. Их существование - экспериментальный факт.

Ты говоришь о искусственных языках как о естественных. В лингвистке всё именно так - там формализуют уже существующие, имперически, языки. Есть, конечно, ЯП возникшие «сами по себе» и их можно изучать только как антропологические явления, но где-то начиная с 50-ых годов (грамматики Хомского, BNF) есть традиция определять ЯП формально, в рамках каких-то моделей (можно взять как примеры стандарты схемы и хаскеля).

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

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

Напоминаю - тоже хочу посмотреть.

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

http://en.wikipedia.org/wiki/Tacit_programming

Посмотрел немного на APL:

(~R∊R∘.×R)/R←1↓⍳R

за теми или иными инфиксными операторами языка скрывается обычный «loop based approach». В языке в котором можно определить инфиксный оператор как обычную функцию это будет примерно так:

primes n = let r = [2 .. n] in neg (r ∊ r × r) / r

  where

    infixl 7 ×
    x × y = [[a * b | a <- x] | b <- y]

    infixr 5 ∊
    x ∊ m = [any (elem e) m | e <- x] -- map (flip any m . elem) x

    neg x = [not e | e <- x] -- neg = map not

    ix / x = catMaybes [if i then Just e else Nothing | e <- x | i <- ix]

тип выводится довольно общий:

primes :: (Enum a, Eq a, Num a) => a -> [a]
quasimoto ★★★★
() автор топика
Ответ на: комментарий от quasimoto

В родственниках apl интереснее возможность легко комбинировать функции, что-то типа использования функтора reader:
avg=: +/ % #
Что означает
avg = div <$> foldl1 (+) <*> length

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

список аксиом пожалуйста.

ZFC подойдет.

не в ТК, а где?

Где угодно. Да в том же ТК тоже можно.

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

Там все ясно. Но постараюсь следующий раз по-проще изъясняться.

но нужна модель, в которой мы можем определить, что такое «камень», что такое «упал».

Не нужно, конечно. Нам вообще понятия «камня» и «падения» не нужно. Они нужны лишь чтобы описать факт наблюдения. Самому же наблюдению отсутствие этих понятий не мешает. Вот какое-нибудь животное не знает ни что такое «камень», ни что такое «падение», и что такое «модель» оно тоже не знает, но это не мешает эивотному видеть падающий камень.

ха-ха-ха!

Что смешного?

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

В хацкеле curry из ТК

В хацкеле нет curry из ТК. В хацкеле вообще нету ф-й в математическом смысле. Вообще в ЯП не может быть функций в математическом смысле.

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

О чем и речь.

Но какое это имеет отношение к реальности то?

Как и любые теоретические выкладки - никакого, очевидно.

статьи нужны для того, чтобы потом общаться с другими и другие могли понять о чём ты говоришь. Ещё раз ТВОЯ карри неинцективна

Да не моя, а общепринятая curry. Но не из ТК, а из программирования. Которая преобразует ф-и многих (скольких угодно) аргументов в ф-и одного, а не ф-и из двух в ф-и одного.

не тупи, а.

Тебе можно, а мне - нельзя? Ты же с меня потребовал аналогичного определения.

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

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

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

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

Да, по поводу незнания отличия функций в хаскеле и процедур в схеме комментарии будут

О каком незнании речь?

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

Ну типа того.

То есть числа 88979879878 не существует? Я верно понял?

А кто выводить будет? anonymous? :)

Он самый :)

В принципе я дальше пояснил, что выводить существование даже и не обязательно.

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

Так что это за curry из хаскеля? Какое у нее определение? И публикации, пожалуйста.

Ты говоришь о искусственных языках как о естественных.

Я говорю об актуально существующих и наблюдаемых мною последовательностях символов. Чем они являются - термами искусственного/естественного языка или вообще рандомным набором букв - дело десятое.

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

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

anonymous
()
Ответ на: комментарий от quasimoto
(define (make-curry right?) 
  ;; The real code is here
  (define (curry* f args kws kvs)
    (unless (procedure? f)
      (raise-type-error (if right? 'curryr 'curry) "procedure" f))
    (let* ([arity (procedure-arity f)]
           [max-arity (cond [(integer? arity) arity]
                            [(arity-at-least? arity) #f]
                            [(ormap arity-at-least? arity) #f]
                            [else (apply max arity)])]
           [n (length args)])
      (define (loop args n)
        (cond
          [(procedure-arity-includes? f n)
           (if (null? kws) (apply f args) (keyword-apply f kws kvs args))]
          [(and max-arity (n . > . max-arity))
           (apply raise-arity-error f arity args)]
          [else
           (letrec [(curried
                     (case-lambda
                       [() curried] ; return itself on zero arguments
                       [more (loop (if right?
                                     (append more args) (append args more))
                                   (+ n (length more)))]))]
             curried)]))
      ;; take at least one step if we can continue (there is a higher arity)
      (if (equal? n max-arity)
        (if (null? kws) (apply f args) (keyword-apply f kws kvs args))
        (letrec ([curried
                  (lambda more
                    (let ([args (if right?
                                  (append more args) (append args more))])
                      (loop args (+ n (length more)))))])
          curried))))
  ;; curry is itself curried -- if we get args then they're the first step
  (define curry
    (case-lambda [(f) (define (curried . args) (curry* f args '() '()))
                      curried]
                 [(f . args) (curry* f args '() '())]))
  (make-keyword-procedure (lambda (kws kvs f . args) (curry* f args kws kvs))
                          curry))

(define curry  (make-curry #f))
(define curryr (make-curry #t))

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

Я не говорил, что не могу привести ссылку, я сказал, что мне лень это делать.

Это примерно то же самое. Учитывая, что повторять одну и ту же фигню по пятьсот раз тебе не лень.

И, более того, я указал, где ты можешь искомую информацию отсыкать.

Примерно как «на земле».

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

Примерно как «на земле».

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

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

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

То есть, первая часть возражений не вызывает?

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

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

Речь идет об обычном незнании. Вы неоднократно утверждали, что

В хацкеле вообще нету ф-й в математическом смысле. Вообще в ЯП не может быть функций в математическом смысле.

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

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

Речь идет об обычном незнании.

Не идет.

> На вопросы о том, почему это так, вы отвечали «ну, в общем, того-этого, так сказать, зависит от обстоятельств, на практике видно»

Это твои фантазии. ответ вполне конкретный - в ЯП есть только термы этого ЯП. В какой степени можно моделировать определенную часть этих термов математическими функциями - другой вопрос. И если даже можно - эти термы от этого математическими функциями не становятся.

Поэтому не понятно, на чем вообще базируется ваша уверенность в том что «В хацкеле вообще нету ф-й в математическом смысле» и так далее.

Она базируется на том, что никто не доказал их наличия. Математическая функция - это такой частный случай бинарного отношения. Покажи мне бинарные отношения в хаскеле. или хотя бы множества (без множеств бинарных отношений, очевидно, нет)..

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

В какой степени можно моделировать определенную часть этих термов математическими функциями - другой вопрос.

С практической точки зрения - тот же самый. Вы на него ответить не смогли.

И если даже можно - эти термы от этого математическими функциями не становятся.

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

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

С практической точки зрения - тот же самый.

И что это меняет?

Вы на него ответить не смогли.

А на него и нельзя ответить.

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

Это не важно что и кому интересно. Важны факты. А факты состоят в том, что ни в каком ЯП (в хаскеле в том числе) математический функций нет.

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

А на него и нельзя ответить.

Что означает «я не знаю, что на него ответить». О чем я и говорил.

А факты состоят в том, что ни в каком ЯП (в хаскеле в том числе) математический функций нет.

А числа-то, числа в каких-нибудь ЯП есть?

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

То есть числа 88979879878 не существует?

Есть общее определение частным случаем которого является данная запись (десятичные и любые другие системы счисления по постоянному основанию - та формула с суммой по произведениям чисел из записи и степеней основания, сами числа, например 0 .. 9, определяются в рамках данной модели чисел - как канонические термы арифметики Пеано, множества ZF, стрелки категории Nat и т.д., понятия «произведение», «сумма», «степень» также даются в рамках таких моделей).

Так что это за curry из хаскеля? Какое у нее определение? И публикации, пожалуйста.

The Haskell 98 Language Report.

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

Да, если говорить про все языки. Но если брать схему или хаскель, то там существование термов это не экспериментальный факт - их просто определили создатели этих языков (в т.ч. в стандартах) с помощью метаязыка (BNF, например). «Спека или GTFO», какие уж тут эксперименты.

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

А числа-то, числа в каких-нибудь ЯП есть?

Память конечна - чисел нет :)

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

Ох, во что превратилась бедная curry f x y = f (x, y).

А тут приведены примеры таких разных функций f и g, что для них curry f и curry g совпадают?

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

The Haskell 98 Language Report.

«Fast and Loose Reasoning is Morally Correct».

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

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

Это ничего не меняет. Как мы знаем, определение имеет вид: «Х есть Y (более общее понятие), которое удовлетворяет свойствам». Так вот - каково определение 88979879878? Как мне выделить это число из кучи других чисел? как мне определить именно _это_ число? И ссылки на литературу, пожалуйста, где я мог бы увидеть определение этого числа. Ну вы же, в конце концов, требуете с меня определения _конкретной функции_? Почему я не могу потребовать определения _конкретного числа_?

The Haskell 98 Language Report.

Ну определение-то напиши.

Да, если говорить про все языки.

Если говорить про любой конкретный ЯП.

Но если брать схему или хаскель, то там существование термов это не экспериментальный факт

А какой? Программа перед моими глазами - это не экспериментальный факт? Что тогда?

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

Нет, но разница не существенна.

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

Ты это всё серьёзно?

Так вот - каково определение 88979879878?

88979879878 ≡ 8 × 10⁰ + 7 × 10¹ + лень дописывать.

Теперь нужны определения 8, 10, 0, 7, 1, ×, + и ^ ?

Ну вы же, в конце концов, требуете с меня определения _конкретной функции_?

Ещё одно определение конкретной функции - http://ncatlab.org/nlab/show/currying. Собственно, так всегда - конкретные функции о которых можно сказать, что они существуют и играют какую-то существенную роль в структуре теории или её применениях, имеют конкретные определения в литературе (причём, множество равнозначных определений в разной литературе). Функции про которые никто никогда ничего не слышал, или которые не играют какой-либо существенной роли в структуре теории или её применениях (как число 88979879878) действительно нет смысла искать (да и неинтересно) и нет смысла просить доказательств их существования и ссылок на АИ. Но curry это не этот случай (что подтверждают многочисленные её определения в различной литературе).

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

Ну определение-то напиши.

Ты знаешь это определение (или можешь посмотреть его в Prelude). Также, можешь убедится, что эта Prelude.curry изоморфна (читай, то же самое что и) curry из лямбда исчисления, так как существует модель хаскеля как лямбда исчисления (HM или System F), и что эта Prelude.curry изоморфна (то же самое что и) curry из теории категорий, так как существует категорная модель хаскеля (Hask).

А какой? Программа перед моими глазами - это не экспериментальный факт? Что тогда?

Ну что, по-твоему, такое 88979879878? Тоже экспериментальный факт? Нет, это краткая запись канонического (или нет) терма ℕ, где термы ℕ _определены_ (в такой-то метатеории) как:

ℕ ∈ Set
0 ∈ ℕ
n ∈ ℕ | n′ ∈ ℕ

точно так же и в ЯП у которого термы заданы формально - просто вместо ℕ будет более сложная индуктивная конструкция.

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

(define (sum1 x y) (+ x y))

(define ((sum2 x) y) (+ x y))

Поэтому я и прошу R5RS. sum2 это уже не Scheme? Racket?

Вообще, печально - у sum1 домен, типа, декартово произведение, sum2, как я понимаю, уже каррированная, тем не менее, твоя curry её принимает в качестве аргумента (ill-typed). По сути, в этой curry две разные карри - одна для одного рода функций работает (от многих аргументов), другая для другого (уже каррированных).

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

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

и что эта Prelude.curry изоморфна (то же самое что и) curry из теории категорий, так как существует категорная модель хаскеля (Hask).

К сожалению, не совсем. Потому как категорная интерпретация типа A -> B, увы, не совсем совпадает с множеством морфизмов из интерпретации A в интерпретацию B.

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

Потому как категорная интерпретация типа A -> B, увы, не совсем совпадает с множеством морфизмов из интерпретации A в интерпретацию B.

Потому что морфизм это не терм а класс эквивалентности термов? Вместо CCC можно взять CC2C, тогда морфизм будет каноническим или лямбда-термом, а 2-морфизм классом эквивалентности (сложных) редукций.

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

Потому что морфизм это не терм а класс эквивалентности термов?

Нет. Потому что undefined и const undefined — разные вещи.

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

Потому что undefined и const undefined — разные вещи.

Так они и должны быть разными, разве нет? undefined : 0 → A, единственен для любого типа-объекта A, 0 — начальный объект категории типов, const ∘ undefined : B → A, для любых A и B.

Например:

undefined : ∀{a} {A : Set a} → A
undefined = undefined -- termination checking problem

constUndefined : ∀ {a b} {A : Set a} {B : Set b} → B → A
constUndefined = const undefined

Конечно, хаскель ломает строгую нормализацию, так что да, с помощью SystemF / Hask моделируется только некое его подмножество (без явной рекурсии, инфинитных данных, IO и т.п.).

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

undefined не терминируем. const undefined something редуцируется в тот же undefined, так что const undefined something тоже не терминируем.

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

const ∘ undefined : B → A

const ∘ undefined : 0 → (B → A).

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

В категории доменов — нет.

А что такое категория доменов? И зачем нужно рассматривать именно её (а не категорию Hask ≅ HaskTotal with ⊥ ≅ HaskTotal∗)?

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

А что такое категория доменов?

Категория, объекты которой — домены (т.е., частично упорядоченные множества, в каждого из которых есть 1) наименьший элемент, и 2) точная верхняя грань каждой возрастающей последовательности), а морфизмы — монотонные функции, сохраняющие супремумы возрастающих последовательностей (но, вообще говоря, не обязательно сохраняющие наименьший элемент).

И зачем нужно рассматривать именно её

Затем, что денотационная семантика, наиболее точно описывающая хаскель — это именно она.

а не категорию Hask ≅ HaskTotal with ⊥ ≅ HaskTotal∗

Это вообще чего?

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

Это вообще чего?

Тут такая же ситуация как с категорией SetPart всех малых множеств и частичных функций, которую можно заменить эквивалентной категорией Set⊥, то есть Set∗ (∗↓Set, ∗ — синглетон, с забывающим функтором Set∗ → Set).

Правда, я не знаю как категория может моделировать семантику (типы и синтаксис термов — да, семантика даётся, например, семантическим функтором или построением уже 2-категории редукций). Когда говорят о Hask имеют в виду некую CCC подходящую для моделирования хаскельных типов и термов (не редукций, которые определяют функции), есть ещё какие-то модели которые пригодны для задания в том числе семантики (частичных функций и строгости / нестрогости, в случае хаскеля)?

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

семантика даётся, например, семантическим функтором

Как в примере с curry / uncurry, которые задаются сопряжёнными функторами на –×b и b→– (или биекцией между двумя определёнными множествами стрелок в случае конкретной категории).

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

Тут такая же ситуация как с категорией SetPart всех малых множеств и частичных функций, которую можно заменить эквивалентной категорией Set⊥, то есть Set∗ (∗↓Set, ∗ — синглетон, с забывающим функтором Set∗ → Set).

Не пойдёт. К множествам нужно добавлять только один полюс. К хаскельным типам, в большинстве случаев, много — скажем, в типе [Integer] недостаточно добавить (_|_), надо ещё ((_|_) : (_|_)), (1 : (_|_)), ((_|_) : (_|_) : (_|_)) и ещё кучу всего.

Вот когда мы это всё добавим — получится категория доменов.

Когда говорят о Hask имеют в виду некую CCC

Категория Hask не является декартово замкнутой. Категория доменов — да, является, но Hask лишь вкладывается в неё. Декартова незамкнутость видна из того самого неравенства undefined /= const undefined.

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

в типе [Integer] недостаточно добавить (_|_)

⊥([Integer]) : ⊥ → [Integer] существует (стрелка из начального объекта существует для любого объекта).

надо ещё ((_|_) : (_|_))

Тут терм ⊥ в левом аргументе (:) нужно добавить не типу [Integer], а типу Integer, ⊥(Integer) : ⊥ → Integer существует, и типу [Integer] во втором аргументе. (Будем считать, для простоты, что у нас (:) :: Integer -> [Integer] -> [Integer]). Сам терм строится так:

                * ⊥
                |
                | ⊥
                v
                * [Integer]
⊥   Integer     |
*--⊥-->*--(:)-->| (⊥:)
                v
                * [Integer]

((_|_) : (_|_)), (1 : (_|_)), ((_|_) : (_|_) : (_|_))

Тут аналогично. Я не вижу в этих примерах двух разных неканоничных термов ⊥ которые нужно добавить типу [Integer] (это даже и невозможно, из начального объекта ⊥ в любой объект есть только одна стрелка) — каждому типу нужно добавить только один такой терм, при этом будет возможность строить такие выражения (по сути, эти ⊥ это всё разные стрелки, в хаскеле обходятся одним, но зато полиморфным, undefined, то есть семейством undefined термов каждого типа).

Категория Hask не является декартово замкнутой.

Где-то я слышал, что она именно CCC (http://pcapriotti.wordpress.com/2012/02/04/monoidal-instances-for-pipes тут, например, и где-то ещё). Но если нет, то значит она кривая :) Потому что просто-типизированное лямбда исчисление и System F строятся как CCC, а MLTT, например, как LCCC. Но частичные и нетерминируемые функции, инфинитные данные (которые суть коданные) вполне могут что-то сломать.

Декартова незамкнутость видна из того самого неравенства undefined /= const undefined.

Не вполне понимаю это неравенство — undefined это канонический терм (иначе говоря, терм в нормальной форме, его уже не во что редуцировать), тогда как const undefined это, во-первых, функция, во-вторых, const undefined something _эквивалентна_ (под бета-редукцией) undefined. Что значит «/=» в этой записи, какого рода равенство имеется ввиду? Ну и в случае CCC undefined : ⊥ → A, const : A → A ^ B, const ∘ undefined : ⊥ → A ^ B — в каком смысле они предполагаются быть равными (редукционно? Ну редукционно они и в хаскеле равны)?

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

Тут терм ⊥ в левом аргументе (:)

При чём тут левый аргумент? Я говорю о том, что всё вместе нужно добавить к типу [Integer]. Что в нём будут не только (_|_) и элементы вроде [], [1], [1,2,3],..., но и куча промежуточных.

двух разных неканоничных термов ⊥

Кто сказал «неканоничных (_|_)»? Что это такое вообще?

Где-то я слышал, что она именно CCC

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

Потому что просто-типизированное лямбда исчисление и System F строятся как CCC

Нет, они строятся как формальные языки и правила редукции. А вот денотационная семантика — да, как декартово-замкнутая категория. В Хаскеле же всё несколько иначе. В частности, если бы в Hask были бы декартовы произведения, то (undefined, undefined) было бы равно undefined. Вместо этого в Хаскеле используется боксинг, из-за которого получается лишний undefined в самом низу. А боксинг нужен для того, чтобы полиморфные функции реализовывать.

Не вполне понимаю это неравенство... undefined : ⊥ → A, const : A → A ^ B, const ∘ undefined : ⊥ → A ^ B — в каком смысле они предполагаются быть равными

Чего? const undefined :: a -> b, undefined :: a -> b, в чём проблема-то? Запусти ghci и посмотри сам:

(undefined :: Integer -> Integer) `seq` 0

и

(const undefined :: Integer -> Integer) `seq` 0
Два значения, одного типа, мы можем их различить — значит, они не равны.

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

всё вместе нужно добавить к типу [Integer]

Тип [Integer] это объект, термы принадлежат типу постольку, поскольку есть стрелки в его объект. Из ⊥ в [Integer] может быть только одна стрелка (undefined :: [Integer]), а все остальные термы, которые ты назвал, существуют постольку, поскольку существуют соответствующие _композиции_ (я одну такую нарисовал).

С тем же успехом можно дописывать каждому ADT nullарный конструктор UndefinedForThisType, и дописывать неполному case clause _ -> UndefinedForThatType.

Кто сказал «неканоничных (_|_)»? Что это такое вообще?

Понятие каноничного терма из логики (Как в Intuitionistic type theory, например, или просто можно мыслить это как терм в нормальной форме). Например, в случае натуральных чисел, 0, 1 (S(0)), 2 (S(S(0))), ... - каноничные термы, 2 + 2 - нет. Вот undefined, как стрелка из ⊥ в данный объект это каноничный терм, т.е. терм в нормальной форме, (undefined, undefined) - нет (я знаю, что в хаскеле это не так, и это «обычный падающий тупл», но это, как по мне, просто странное поведение - даже если функции частичны, я хочу, хотя бы, редукцию в понятный канонический терм).

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

Related. Там в качестве «category for Haskell» рассматриваются (как минимум) моноидально замкнутые категории (а в таких допустимо каррирование).

Нет, они строятся как формальные языки и правила редукции. А вот денотационная семантика — да, как декартово-замкнутая категория.

Это изоморфные картинки (Curry–Howard–Lambek correspondence, http://arxiv.org/abs/1102.1313, например, AFAIU безотносительно теории доменов там всё).

А вот денотационная семантика — да, как декартово-замкнутая категория.

Ты всё это время говоришь про domain theory? Я просто с ней вообще не знаком, поэтому могу тебя не понимать (все эти CPO / CPO⊥, CPPO / CPPO⊥).

Два значения, одного типа, мы можем их различить — значит, они не равны.

Ну а я спрашиваю «в каком смысле они предполагаются быть равными» - не равны, конечно, зачем им быть вообще равными (и почему из их неравенства тут же вытекает не СССовость?)? 1 и const 1, вот, тоже не равны.

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

Теперь нужны определения 8, 10, 0, 7, 1, ×, + и ^ ?

Нет, теперь нужен авторитетный источник, в котором указано, что «88979879878 ≡ 8 × 10⁰ + 7 × 10¹ + ...»

Ещё одно определение конкретной функции - http://ncatlab.org/nlab/show/currying. Собственно, так всегда - конкретные функции о которых можно сказать, что они существуют и играют какую-то существенную роль в структуре теории или её применениях, имеют конкретные определения в литературе (причём, множество равнозначных определений в разной литературе).

Но curry как раз к таким функциям и не относится. Естественно, мы говорим о curry в ЯП, не в том же теоркате.

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

Ты знаешь это определение (или можешь посмотреть его в Prelude).

То есть определение ф-и - это ее код? Так? То есть мы все-таки остановимся на том, что ф-я в ЯП - это класс эквивалентности определенных термов, а какая там у нее омдель - дело десятое?

Ну что, по-твоему, такое 88979879878? Тоже экспериментальный факт?

Естественно.

Нет, это краткая запись канонического (или нет) терма ℕ, где термы ℕ _определены_ (в такой-то метатеории) как:

Нет, это уже модель. А само «88979879878» - последовательность символов, которую мы экспериментально наблюдаем.

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

Поэтому я и прошу R5RS. sum2 это уже не Scheme? Racket?

Это просто сахар.

(define ((sum2 x) y) (+ x y)) -> (define (sum2 y) (lambda (x) (+ x y))).

твоя curry её принимает в качестве аргумента (ill-typed).

Нет, с типизацией все хорошо. curry принимает любую функцию.

По сути, в этой curry две разные карри - одна для одного рода функций работает (от многих аргументов), другая для другого (уже каррированных).

Я вижу перед собой одну единственную curry, которая работает одним, вполне определенным, формально заданным образом. Откуда ты взял вторую - мне неясно, поясни.

Хотя, почему sum1 и sum2 это разные функции?

У них разный домен, они принимаются разные значения на разных аргументов (точнее - они определены на разных аргументах). По-моему, если у ф-й разный домен, то они не могут совпадать, нет?

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

Конечно, нет, они не возвращают одинаковые значения для одинаковых аргументов. (sum1 0) -> ошибка, (sum2 0) -> лямбда.

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