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

★★★★

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

Тип [Integer] это объект, термы принадлежат типу постольку, поскольку есть стрелки в его объект.

Меня вообще термы не интересуют, меня интересует семантика.

Из ⊥ в [Integer] может быть только одна стрелка

Что ты называешь «⊥»? Какой объект?

Понятие каноничного терма из логики

Очень может быть, но я-то тут при чём? Зачем ты вообще про эту фигню вспомнил?

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

И при чём тут эта ссылка? Она как-то отменяет тот факт, что в категории хаскельных типов и функций между ними декартова произведения () на себя просто не существует?

Это изоморфные картинки

И? «Изоморфно» и «Строится как» - разные вещи.

Ты всё это время говоришь про domain theory?

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

Я просто с ней вообще не знаком

А чего там знакомиться-то? Определение домена и морфизма доменов я уже сказал, тот факт, что эта категория декартово замкнута - достаточно тривиален, существование Y-комбинатора - чуть посложнее, но не слишком, вложение Hask в категорию доменов тоже примитивно.

Ну а я спрашиваю «в каком смысле они предполагаются быть равными»

Моя твоя не понимай. Есть два элемента одного множества, в каком смысле они могут быть равными?

зачем им быть вообще равными (и почему из их неравенства тут же вытекает не СССовость?)?

Ну нет никакой функции (теоретико-множественной) из Integer в Integer, которая соответствовала бы элементу undefined :: Integer -> Integer. Для const undefined есть, а для undefined - нету. А должна быть, если бы это была декартово-замкнутая категория.

Превратить это в аргумент категорного характера - механическая работа.

Впрочем, как я уже сказал, в Hask даже произведений нет, куда уж там экспонентам.

1 и const 1, вот, тоже не равны.

Depends. Если уж определять instance Num a => Num (b -> a), то в нём будет, в частности, и такое: fromInteger n = const $ fromInteger n (нет, можно и иначе, но это единственный осмысленный способ). А тогда 1 == const 1.

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

Меня вообще термы не интересуют, меня интересует семантика.

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

Что ты называешь «⊥»? Какой объект?

Это initial object, 0. Для типа A nullарными конструкторами будут стрелки 1 → A из terminal object (может быть от нуля и более таких стрелок), а undefined : 0 → A из initial object (только одна стрелка).

И при чём тут эта ссылка?

Это не контраргумент, это просто ссылка.

Впрочем, как я уже сказал, в Hask даже произведений нет, куда уж там экспонентам.

Она как-то отменяет тот факт, что в категории хаскельных типов и функций между ними декартова произведения () на себя просто не существует?

Ладно, это попроще, спрошу:

diag :: () -> ((), ())
diag () = ((), ())

то есть такое определение в чём-то не полно?

Ну нет никакой функции (теоретико-множественной) из Integer в Integer, которая соответствовала бы элементу undefined :: Integer -> Integer. Для const undefined есть, а для undefined - нету. А должна быть, если бы это была декартово-замкнутая категория.

Но при чём тут теоретико-множественные функции вообще? Наверно при том, что в теории доменов берут CPO, родственную Set, и вкладывают в неё Hask. Вместо того чтобы построить Hask (которая далека от Set) непосредственно (не CCC? тут нужен ясный контрпример, почему она таковой не является, без отсылок к теоретико-множественным функциям и теории доменов).

Кстати:

undefined :: Integer -> Integer
const undefined :: Integer -> Integer

тут undefined это вообще два разных терма, в первом случае это:

undefined : 0 → Integer ^ Integer

а во втором:

                          * Integer
0           Integer       |
*--undefined-->*--const-->| const undefined
                          v
                          * Integer 

то есть

undefined : 0 → Integer

И? «Изоморфно» и «Строится как» - разные вещи.

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

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

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

Десятичная система счисления - такой? Или учебник арифметики такого-то класса? :)

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

Вот её код, f x y ~ f (x, y), более менее (с точностью до местных значков) одинаков в любой теории - в хаскеле, в лямбда исчислении, теории множеств, логике, теории категорий.

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

ошибка

Система типов должна исключать такого рода ошибки.

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

Это initial object, 0.

Ну, здрасьте. А доказать существование?

то есть такое определение в чём-то не полно?

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

Вместо того чтобы построить Hask (которая далека от Set) непосредственно

Как?

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

Ну дык давай конструкцию, раз уж ты настаиваешь на некоем «непосредственном» построении.

тут undefined это вообще два разных терма

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

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

Почему топос-то?

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

Ну, здрасьте. А доказать существование?

Достаточно того, что есть undefined. Или того, что его всегда можно определить:

__ :: forall a. a
__ = __

или

__ :: forall a. a
__ = error "__"

С точностью до изоморфизма это единственная для каждого типа (forall a. a) стрелка из 0.

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

Да, в любой декартовой категории можно «копировать» и «удалять» информацию (чем классическое лямбда исчисление, в том числе хаскель, отличается от линейных и квантовых вариантов), если есть финитные произведения (декартово произведение и терминальный объект), то всегда можно определить диагональный X → X × X и удаляющий X → 1 морфизмы.

data (:×) :: * -> * -> * where
  (:×) :: forall a b. a -> b -> a :× b

fst :: forall a b. a :× b -> a
fst (x :× _) = x

snd :: forall a b. a :× b -> b
snd (_ :× y) = y

diag :: forall a. a -> a :× a
diag x = x :× x

diagUnit :: () -> () :× ()
diagUnit = diag

delete :: forall a. a -> ()
delete _ = ()

braid :: forall a b. a :× b -> b :× a
braid (x :× y) = y :× x

-- Symmetric property: braid ∘ braid = id

-- Curry / Uncurry / Hom / Op / "anti-types"?

Как?

Как семантические скобки из типо-термов в категорию (и обратно - синтаксические скобки из категории дают типо-термы внутреннего языка, синтаксис и семантика это сопряжённые функторы). Тут уже была ссылка на «Introduction to Categories and Categorical Logic» - там есть такие скобки из просто-типизированного лямбда исчисления в CCC (1.6.5). Для System F, зависимых типов, линейных вариантов лямбда исчисления или логик тоже существуют такие построения.

Ну дык давай конструкцию, раз уж ты настаиваешь на некоем «непосредственном» построении.

Это же тема для целой статьи, нет? :) По крайней мере, давай [ссылку на] конструкцию именно хаскеля в теории доменов.

Почему топос-то?

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

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

Система типов должна исключать такого рода ошибки.

Потому что иначе это будет применение f(x) функции f : A × B → C к аргументу x ∈ A.

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

Достаточно того, что есть undefined.

Для чего достаточно?

Или того, что его всегда можно определить:

Кого? undefined? При чём тут начальный объект?

стрелка из 0.

Опять за рыбу деньги. Откуда 0 взялся-то?

data (:×) :: * -> * -> * where

Это обычный тупль, (,). Но это НЕ декартово произведение в теоретико-категорном смысле.

Как семантические скобки из типо-термов в категорию

Чего? Вот это заклинание ты предлагаешь как конструкцию Hask?

Это же тема для целой статьи, нет? :)

Ну дык хоть намекнул бы.

По крайней мере, давай [ссылку на] конструкцию именно хаскеля в теории доменов.

[haskell] объясните механику рекурсивного определения (комментарий) и следующий за этим коммент — это для начала.

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

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

Другое дело, когда речь заходит о тотальном программировании, где нет никаких undefined, а любая программа завершается без ошибок. Там да, там топосы имеют смысл (хотя, как я понимаю, связь TotalFP с топосами — предмет активного исследования).

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

Десятичная система счисления - такой?

не нашел там информации конкретно по числу 88979879878 :)

Вот её код, f x y ~ f (x, y), более менее (с точностью до местных значков) одинаков в любой теории - в хаскеле, в лямбда исчислении, теории множеств, логике, теории категорий.

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

Система типов должна исключать такого рода ошибки.

Она ничего никому не должна.

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

Потому что иначе это будет применение f(x) функции f : A × B → C к аргументу x ∈ A.

Это твои домыслы, которые не имеют под собой никаких оснований.

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

Это обычный тупль, (,). Но это НЕ декартово произведение в теоретико-категорном смысле.

А чем оно плохо в качестве декартова произведения в категорном смысле??

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

Ну блин, сколько я ещё должен уговаривать посчитать морфизмы из () в ((), ())?

Вот вам полный список:

const undefined
const (undefined, undefined)
const ((), undefined)
const (undefined, ())
const ((), ())
\x -> x `seq` (undefined, undefined)
\x -> x `seq` ((), undefined)
\x -> x `seq` (undefined, ())
\x -> x `seq` ((), ())
\x -> (x, undefined)
\x -> (undefined, x)
\x -> (x, x)
\x -> (x, ())
\x -> ((), x)
Четырнадцать разных морфизмов. В то время как морфизмов из () в () всего три:
const undefined
const ()
id
Как известно, морфизмы A->BxC должны соответствовать парам морфизмов A->B и A->C (это просто из определения декартова произведения видно). А не соответствуют, 3*3/=14.

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

\x -> x `seq` (undefined, undefined)
\x -> x `seq` ((), undefined)
\x -> x `seq` (undefined, ())
\x -> x `seq` ((), ())

Замечательно, а ты сможешь доказать, что seq - это морфизм? Без этих 4 и const undefined, который не () -> ((), ()) потому что () != ((), ()) все сходится, то есть 3*3 = 9.

Ты бы лучше попробовал суммы построить.

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

Замечательно, а ты сможешь доказать, что seq - это морфизм?

Э... вообще-то, это хаскельная функция. Нет, можно, конечно, создать модель, в которой половины хаскельных функций просто не будет, но какой смысл?

Ну, не нравится seq, запиши так:

\x -> case x of () -> (undefined, undefined)
Ровно то же самое.

const undefined, который не () -> ((), ()) потому что () != ((), ())

Ты бредишь.

Prelude> :t const undefined :: () -> ((), ())
const undefined :: () -> ((), ()) :: () -> ((), ())

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

Ну, не нравится seq, запиши так:

Вот теперь лучше. И этот пример как раз демонстрирует суть - проблема не с произведениями, а с суммами. Вместо (/x -> (undefined, undefined)) можно брать любую другую функцию f и потом убедиться, что (case x of Any -> f x) != (f case x of Any -> x), что дает некоммутативность диаграммы для сумм.

Ты бредишь.

Да, забыл, что undefined < ((), ()).

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

И этот пример как раз демонстрирует суть - проблема не с произведениями, а с суммами.

Что означает эта фраза?

Нет, не так. Попробую выделить конкретику:

1) Где ты тут суммы увидел?

2) Какая проблема? Проблема отсутствия? Так в Hask нет ни сумм, ни произведений.

(/x ->

Гррррр. \x.

любую другую функцию f и потом убедиться, что (case x of Any -> f x) != (f case x of Any -> x)

Что значит «Any»? Попробуй сформулировать свой аргумент правильно.

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

Какой именно диаграммы? Понятие «диаграмма для сумм» не имеет определения в математике.

Да, забыл, что undefined < ((), ()).

Ты забыл, что undefined :: ((), ()).

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

1) Где ты тут суммы увидел?

В case x ...., x - сумма.

2) Какая проблема? Проблема отсутствия?

Ага.

Что значит «Any»? Попробуй сформулировать свой аргумент правильно.

по-хорошему надо так:

data A|B = left A | right B

(case (x :: A|B) of left x -> f x, right x -> f x) != f (case (x :: A|B) of left x -> x, right x -> x)

Какой именно диаграммы?

Диаграмму из определения сумм. f: A|B -> C, этому f должна соответствовать пара стрелок, такие, что f1 = f . left, f2 = f . right, но если выбрать в качестве f функцию, которая не обязательно вычисляет свой аргумент, то, подставив undefined на место х, получим, что для такой ф-и искомых f1/f2 не окажется - слева у нас всегда будет undefined, а справа можно получить все что угодно путем подбора требуемой f.

Ты забыл, что undefined :: ((), ()).

undefined :: что угодно, если на то пошло.

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

но если выбрать в качестве f функцию, которая

Ну можно, например, взять f x = id для определенности.

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

(case (x :: A|B) of left x -> f x, right x -> f x) != f (case (x :: A|B) of left x -> x, right x -> x)

(case (x :: A|B) of left x -> f1 x, right x -> f2 x) != f (case (x :: A|B) of left x -> x, right x -> x)

вот так

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

В case x ...., x - сумма.

x :: (). Какая, к чёрту, сумма?

data A|B = left A | right B...

По-нормальному:

data Either a b = Left a | Right b
case (x :: Either a a) of {Left x -> f x; Right x -> f x} != f (case (x :: Either a a) of {Left x -> x; Right x -> x}
Ну да, только это не относится к обсуждаемой теме никак.

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

вот так

Меня там тоже слегонца проглючило, когда я в хаскельный синтаксис это переводил.

Но это не важно, ибо всё равно к теме не относится.

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

Другое дело, когда речь заходит о тотальном программировании, где нет никаких undefined, а любая программа завершается без ошибок. Там да, там топосы имеют смысл (хотя, как я понимаю, связь TotalFP с топосами — предмет активного исследования).

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

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

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

Запись биекции.

Потому что иначе это будет применение f(x) функции f : A × B → C к аргументу x ∈ A.

Это твои домыслы, которые не имеют под собой никаких оснований.

Что? Ты хочешь доказать, что две функции математически эквивалентны, при этом используешь понятие «домен». И при этом же позволяешь себе такого рода применения. Математически, термов вроде (2 +) (где + : ℝ × ℝ → ℝ, например) или sqrt(1, 2, 3) (где sqrt : ℂ → ℂ) просто не существует, так что использовать "(f неполное применение) => ошибка" (т.е. неверно составленные термы) как аргумент просто нечестно.

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

Нет, можно, конечно, создать модель, в которой половины хаскельных функций просто не будет, но какой смысл?

Чтобы Hask была CCC. Если она таковой не является и вообще не декартова (не моноидальна?), то такую Hask остаётся только выкинуть - она таксономически не полезна.

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

Чтобы Hask была CCC.

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

Если она таковой не является и вообще не декартова (не моноидальна?), то такую Hask остаётся только выкинуть - она таксономически не полезна.

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

К тому же, хотя настоящих произведений, сумм и экспонент в ней нет (и, замечу, не может быть: есть теорема, что категория не может одновременно быть декартово замкнутой, иметь суммы, иметь Y-комбинатор и быть невырожденной), но 1) в ней есть хорошие приближения ((A, B) отличается от декартова произведения A и B лишь одним элементом (_|_)), и 2) она вкладывается в декартово замкнутую категорию (в категорию доменов) с сохранением стирающего функтора и Y-комбинатора.

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

Откуда 0 взялся-то?

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

Ну блин, сколько я ещё должен уговаривать посчитать морфизмы из () в ((), ())?

Почему const () это стрелка из () в ()?

() : 1 → ()
∀ (B ∈ Obj). const ∘ () : 1 → (B → ())

ну и морфизмов из () в () можно нагородить счётное количество (как минимум):

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

К тому же, хотя настоящих произведений, сумм и экспонент в ней нет (и, замечу, не может быть: есть теорема, что категория не может одновременно быть декартово замкнутой, иметь суммы, иметь Y-комбинатор и быть невырожденной), но 1) в ней есть хорошие приближения ((A, B) отличается от декартова произведения A и B лишь одним элементом (_|_)), и 2) она вкладывается в декартово замкнутую категорию (в категорию доменов) с сохранением стирающего функтора и Y-комбинатора.

есть теорема, что категория не может одновременно быть декартово замкнутой, иметь суммы, иметь Y-комбинатор и быть невырожденной

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

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

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

Дык намекнул бы, какую модель берём-то? А то пока всё, что я услышал — это то, что в ней есть 0.

Почему const () это стрелка из () в ()?

Ну, как бы

Prelude> :t const () :: () -> ()
const () :: () -> () :: () -> ()
Вот почему.

ну и морфизмов из () в () можно нагородить счётное количество (как минимум):

Ы?

id ∘ id

Здрасьте-приехали. То есть, то, что id . id и id в рамках языка не различимы вообще — это пофиг? А тождественный морфизм из () в () — это кто тогда? Не id? Потому что если он id, то id . id должно быть просто равно id, это сразу следует из определения тождественного морфизма.

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

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

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

Можно использовать её ограниченно - для моделирования типов данных и «хороших» (тотальных) функций и синтаксических конструкций (термов этих типов данных), в духе total functional / categorical programming. Ну и давать выборочно семантику этим хорошим функциям в виде семантических функторов (как для curry).

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

Вот почему.

То есть, то, что id . id и id в рамках языка не различимы вообще — это пофиг? А тождественный морфизм из () в () — это кто тогда? Не id? Потому что если он id, то id . id должно быть просто равно id, это сразу следует из определения тождественного морфизма.

Если нет разницы (под эквивалентностью) между id . id и id, то есть ли разница между id (для ()) и const () (для ())?

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

то есть ли разница между id (для ()) и const () (для ())?

Они различимы в рамках языка: id undefined даёт ошибку, const () undefined нормально завершается.

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

Математически, термов вроде (2 +) (где + : ℝ × ℝ → ℝ, например) или sqrt(1, 2, 3) (где sqrt : ℂ → ℂ) просто не существует, так что использовать "(f неполное применение) => ошибка" (т.е. неверно составленные термы) как аргумент просто нечестно.

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

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

То есть тот факт, что у этих ф-й разные типы

А какие у них разные типы (как в R5RS вообще выговорить «эта функция имеет такой-то тип»)?

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

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

А какие у них разные типы (как в R5RS вообще выговорить «эта функция имеет такой-то тип»)?

То ест типы не разные (точнее в обоих случаях тип T)? Значит термы корректны. в чем тогда твоя претензия?

Просто если не принимать во внимание ошибки

Ошибка - это вполне штатная ситуация, возврат _|_. С какой стати мы не должны принимать это во внимание?

то будет возможно либо ((f a) b), либо (f a b) - одни и те же значения, при одних и тех же a и b.

Следуя твоей логике все функции эквивалентны, если можно установить биекцию между доменами. Ну, в частности, возьмем функцию f1 = (+ 1) и f2 = (+ 2), эти функции равны, ведь (f1 x) то же самое, что и ((f2 x) + 1)! то есть надо просто вызывать по-разному.

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

Значит термы корректны. в чем тогда твоя претензия?

То есть еще раз - имеем два терма: (f1 0) и (f2 0). Первый возвращает, ну например, 0, второй - _|_. f1 = f2? да или нет?

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

Кстати, а как в Hask моделируются rank-2 полиморфные ф-и/типы? То есть с rank-1 все понятно - мы просто везде подставляем нужный полиморфный аргумент и полиморфных ф-й нет - остаются только мономорфные, которым соответствуют конкретные объекты Hask, при желании некоторые полиморфные функции (не все, конечно) можно считать естественными преобразованиями. Но у rank-2 полиморфный аргумент применить нельзя, каким объектам/стрелкам категории соответствуют такие ф-и? По крайней мере при использовании в рамках конкретного терма (как при rank-1)?

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

Кстати, а как в Hask моделируются rank-2 полиморфные ф-и/типы?

Как в Hask не знаю (я даже толком нигде не видел чёткого «Hask это ...»), а вообще - http://ncatlab.org/nlab/show/universal quantifier#in_topos_theory_6, http://ncatlab.org/nlab/show/dependent product, ещё в Sketches of an Elephant: A Topos Theory Compendium есть раздел про логики высших порядков в топосах.

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

в чем тогда твоя претензия?

Мне не нравится, что определённые в (define (sum1 x y) (+ x y)) и в (define ((sum2 x) y) (+ x y)) функции можно передать curry одинаковым образом - она будет каррировать одни функции, и не трогать другие. Не инъективная читерская curry :)

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

Прям таки _|_? В схеме?

Прям-таки да. _|_ - значение, которое возвращает виснущая/бросившая эксцепшен функция. По крайней мере такая модель вполне корректна.

Формально все по-другому, конечно - эксепшены реализуются через call/cc, семантика которого вполне строго определена и четко задана. То есть в обоих случаях (и (f1 0) и (f2 0)) мы имеем вполне корректные термы, которые редуцируются до нормальной формы согласно семантике схемы. Я никак не могу понять суть твоих претензий. Есть два термы. На одинаковых аргументов они дают разный результат. Следовательно они разные. Какие проблемы? С какой стати их следует считать одинаковыми?

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

Мне не нравится, что определённые в (define (sum1 x y) (+ x y)) и в (define ((sum2 x) y) (+ x y)) функции можно передать curry одинаковым образом - она будет каррировать одни функции, и не трогать другие.

Почему? Она все ф-и каррирует совершенно одинаковым четко определенным образом :)

Ну да, в хаскеле такую curry выразить нельзя. Но это же проблемы хаскиля.

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

Я никак не могу понять суть твоих претензий. Есть два термы. На одинаковых аргументов они дают разный результат. Следовательно они разные. Какие проблемы? С какой стати их следует считать одинаковыми?

Да, соглашусь, функции разные, но curry от них даёт одну и ту же функцию. В хаскеле аналог (только для 2-туплов):

class Curry t where
  curry' :: t

instance (a ~ a', b ~ b', c ~ c') => Curry (((a, b) -> c) -> a' -> b' -> c') where
  curry' = curry

instance (a ~ a', b ~ b', c ~ c') => Curry ((a -> b -> c) -> a' -> b' -> c') where
  curry' = id

такая curry' тоже неинъективна.

quasimoto ★★★★
() автор топика

Miguel, quasimoto, ну наконец-то вы иссякли!

Я аж устал следить за вашими излияниями...

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