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

★★★★

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

Матчатся.

Я понимаю о чём ты говоришь, но это просто другой язык (вот у тебя там значок подтипов).

Как минимум, не следует различать термы, у которых с точностью до альфа-конверсии совпадает нормальная форма.

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

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

Если строго, то curry это часть биекции

Нет. Функция некоего ЯП не является никакой «частью биекции» или еще чем-то вроде. Как следствие - все дальнейшие выкладки, очевидно, тоже неверны.

Любой другой curry это просто какая-то вольность речи

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

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

Ну дык а в вашем хаскеле ее вообще нет.

Конечно, всяких бессмысленных штук там вообще нет.

Формально строгое определение функции curry.

Ты путаешь «формально строгое» и «невнятными значками».

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

Я понимаю о чём ты говоришь, но это просто другой язык (вот у тебя там значок подтипов).

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

Мы не можем одновременно в подтипы, интуицию и классы эквивалентности :)

Как не можем? Во всей науке могут, а тут - не можем? :)

Все просто - есть некое определение ф-й (классы эквивалентности термов блаблабла), интуиция состоит в том, что мы не станем уточнять свойства эквивалентности и свойства термов - они, вообще говоря, нам понятны, т.к. мы знаем что есть ф-я в том или ином ЯП. Далее у нас есть совокупность неких математических объектов (математических функций, конкретно) и мы можем попытаться поискать какой-нибудь изоморфизм ЯП-функции <-> Мат-функции. Ну или хотя бы вложению в ту/иную сторону. Собственно, дефолтный вариант (ф-я многих переменых есть ф-я от кортежей) это лишь одно из многих вложений, не говоря уж о том, что само это вложение не обязательно. То есть, получив его мы можем анализировать наши классы эквивалентности термов, как буд-то это мат. функции. Но в любой момент мы можем «забыть» эту модель или сменить ее на другую. Она не является какой-то выделенной и единственно верной.

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

Конечно, всяких бессмысленных штук там вообще нет.

Вполне осмысленых тоже.

Ты путаешь «формально строгое» и «невнятными значками».

Ты путаешь «яничегонепонелпотмоучтоидиот» и «невнятные значки»

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

Ты путаешь «яничегонепонелпотмоучтоидиот» и «невнятные значки»

Слова бывают ничуть не менее строги, чем значки. И наоборот, значками можно записать любую чушь (причём даже большую, чем словами). Говорю тебе как математик.

Пока ты не определишь формально, что за curry и uncurry ты обсуждаешь, всем твоим словам грош цена.

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

Функция некоего ЯП не является никакой «частью биекции» или еще чем-то вроде.

Но [чистые] функции ЯП прекрасно моделируются бинарными отношениями на множествах.

функции нескольких аргументов

Кстати, что это такое? Как ты дашь этому определение? В рамках какой метатеории (в теории множеств?)?

Это же ваша проблема, что в хаскеле функции curry просто нет - ну нельзя ее выразить.

Да, пожалуй, в хаскеле нет никакой своей особой curry (как и лисповой curry). Curry есть в теории категорий. Я могу ссылаться на Goldblatt или Pierce, есть сколько угодно источников которые с той или иной стороны освещают этот предмет (любой материал по теории категорий, категорной логике или применении теории категорий в CS, в котором обсуждаются CCC вообще и экспоненциалы, в частности). Хаскель тут при том, что он более менее следует этой линии, если и привносит что-то чужеродное, то не ценой потери возможности построить модель.

Выше дано строгое определение функции curry.

Сошлись на АИ (or «прочитать строгое определение функции curry можно только на ЛОРе в таком-то треде»).

Как не можем? Во всей науке могут, а тут - не можем?

Можно сразу потребовать от изучающего, чтобы ему просто было ВСЁ ПОНЯТНО. Действительно, всё ведь интуитивно ясно - много аргументов у функций, карринг, применение по одному и т.д. Но модели нет.

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

Если любая функция имеет один аргумент, то почему это не работает (или что написать, чтоб работало)?

 f x = if x == 0 then 0 else x+f 
monk ★★★★★
()
Ответ на: комментарий от monk

то почему это не работает

Потому что не тайпчекается.

или что написать, чтоб работало

А что оно должно делать?

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

Пока ты не определишь формально, что за curry и uncurry ты обсуждаешь, всем твоим словам грош цена.

Я определил формально, см. выше.

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

А что оно должно делать?

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

Должно быть так

f 0 = 0

f 3 4 6 0 = (f 3) 4 6 0 = (3+f) 4 6 0 = (3+(4+f)) 6 0 = (3+(4+(6+f))) 0 =(3+(4+(6+0)))=13

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

Я определил формально

Тебе так кажется.

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

вернуть 0, если передан 0, иначе вернуть функцию

То есть, типизироваться это не должно в принципе. OK.

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

Но [чистые] функции ЯП прекрасно моделируются бинарными отношениями на множествах.

Ок, речь идет о модели. То есть, как выше - ф-и это определенные классы термов, мы эти классы моделируем бинарными отношениями. Для определенности - рассматриваем ЯП, в котором есть термы, задающие ф-и от нескольких аргументов. Если теперь положить, что такая ф-я - это ф-я от прямого произведения, то тогда мы не можем задать ф-и от кортежей - ведь кортеж это прямое произведение. Тогда две разные ф-и (ф-я от нескольких переменных и ф-я от кортежа по факту разные классы эквивалентности термов) моделируются одним и тем же мат. объектом, что будет приводить к противоречию. Ведь применимость ф-и тождественна корректности определенных термов, в этом случае определив ф-ю f x y = ..., будут корректны термы f x y и f(x, y), то есть тип x -> y -> z должен быть равен типу (x, y) -> z что на практике не выполняется (хотя, наверное, можно и сделать такой ЯП.

Curry есть в теории категорий.

Ну понятно. Но речь ведь не о ней, речь идет о некоей сущности ЯП, которая бы удовлетворяла определенным свойствам.

то не ценой потери возможности построить модель

Ее можно построить, просто другую. То есть на самом-то деле никто не мешает теоретико-категорно выразить лисповую curry аналогично обычной, ну не будет у нее обратной функции - ну и хрен с ней.

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

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

Ф-я от нескольких переменных и функция от кортежа - это одно и то же.

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

Потому что хаскель - не конкантенативный ЯП и поинт-фри/каррирование реализовано на уровне кривых костылей, я об этом уже говорил.

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

Ф-я от нескольких переменных и функция от кортежа - это одно и то же.

Функция от нескольких переменных:

(define (f x y) ...)

Функция от кортежа:

(define (f x) ...)

Это одно и то же? Да или нет?

anonymous
()

Охренительный тред рассуждений о простоте хаскеля.

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

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

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

Это не функции, а процедуры.

Какое определение функциия в ЯП ты используешь? Я знаю только одно:

функция - терм ЯП, удовлетворяющий определенным свойствам (своим для каждого ЯП). В Scheme функция - любой терм вида (lambda (arg ...) body ...) и термы, которые в него рассахариваются, как (define (name args ...) body ...) -> (define name (lambda (args ...) body ...)). Функции в хаскеле - соответственны, термы вида (\args ... -> body ...). Это общепринятое определение. если ты используешь какое-то другое определение (отличное от общепринятого) - то для начала скажи его.

Первая принимает гетерогенный список, вторая - тоже.

Не правда: [code]

(define (f x y) (+ x y))
(f '(1 2))

procedure f: expects 2 arguments, given 1: '(1 2)


[/code] Если она принимает гетерогенный список, то откуда же ошибка?

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

Приведи пример на языке с функциями.

Ну вот на scheme уже привел. Какие еще нужны примеры? Сишка? Паскаль? js? Python? Что-нибудь более экзотическое?

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

Но речь ведь не о ней, речь идет о некоей сущности ЯП, которая бы удовлетворяла определенным свойствам.

Речь шла о curry в хаскеле, которая обладает теми же свойствами что и curry в TK, и некой curry в лиспе, которая обладает другими свойствами и строго не определяется (по крайней мере, ссылки на модель приведено не было).

То есть на самом-то деле никто не мешает теоретико-категорно выразить лисповую curry аналогично обычной, ну не будет у нее обратной функции - ну и хрен с ней.

А можно определить ряд curry2 (Hom(a × b, z) ≅ Hom(a, b → z)), curry3 (Hom(a × b × c, z) ≅ Hom(a, b → c → z)), ... каждая из которых обладает всеми необходимыми свойствами (является частью биекции), и перегрузить их одной curry.

Либо считать кортеж (a, b, c, ...) сахаром над (a, (b, (c, ...))), а тип a × b × c × ... типом (a × (b × (c × ...))), и ввести curry' как curry' = curry' . flip . curry для Hom(a × b, z) ≅ Hom(a, b → z) и curry' = id для Hom(a', z') ≅ Hom(a', z').

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

Ты привел определение процедуры. Общепринятое определение функции: закон, по которому каждому элементу области определения ставится в соответствие элемент в области значений.

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

Ты привел определение процедуры. Общепринятое определение функции: закон, по которому каждому элементу области определения ставится в соответствие элемент в области значений.

Это определение математической функции, мы же говорим о функциях в ЯП. А в ЯП кроме термов вообще ничего нет.

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

Речь шла о curry в хаскеле

Я речь о хаскеле не вел, я вел речь о функции curry (не в хаскеле, не в лиспе - просто о такой функции, которая выполняет каррирование).

строго не определяется

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

А можно определить ряд curry2 (Hom(a × b, z) ≅ Hom(a, b → z)), curry3 (Hom(a × b × c, z) ≅ Hom(a, b → c → z)), ... каждая из которых обладает всеми необходимыми свойствами (является частью биекции), и перегрузить их одной curry.

И что изменится?

и ввести curry' как curry' = curry' . flip . curry

И так что изменится? Как не определяй - обратной ф-и у нее не будет.

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

Какой у f тип?

Назови это вместо типа стек-эффектом и ты напишешь для нее тип ;)

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

Термы определяют некие объекты, обладающие определенными свойствами. Например: функция, рациональное число и т.д. Понятно, что в языке есть терм, который по определенным правилам редуцируется, но на более высоком уровне это функция.

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

не в хаскеле, не в лиспе - просто о такой функции, которая выполняет каррирование

Определение, блджад! :)

«строгое определение» функции в ЯП - это код этой функции, реализацию можешь посомтреть.

Код на каком языке, если «не в хаскеле, не в лиспе»?

Если же мы говорим о функции curry просто, вне привязки к конкретному ЯП, то единственное строгое определение будет иметь форму «curry - это функция, удовлетворяющая таким-то таким-то условиям». Я такое определение дал.

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

И что изменится?

И так что изменится? Как не определяй - обратной ф-и у нее не будет.

Будет нормальная curry, с обратной функцией. Что нужно _ещё_ сделать, чтобы её сломать (чтобы она уже не была частью биекции) я не знаю (и зачем её ломать - тоже не знаю).

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

Термы определяют некие объекты

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

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

Определение, блджад! :)

Я же уже писал. curry :: narg -> 1arg, curry (lambda (x1 ... xn) body ...) = (lambda (x1) (lambda (x2) ... (lambda (xn) body ...) ...)).

Код на каком языке, если «не в хаскеле, не в лиспе»?

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

С таким определением ты не сможешь проводить никаких рассуждений

Почему же? Есть некий объект, который удовлетворяет вполне определенным свойствам, почему бы мне не рассуждать о том, какие свойства могут следовать из описанных?

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

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

Будет нормальная curry, с обратной функцией.

Это как? Не будет у нее обратной функции ни в первом ни во втором. В первом случае curry вообще не функция, а ряд функций, но если определить ее как «объединение» ф-й этого ряда - то непонятно какую из uncarryn применять при конструировании обратной. То есть обратной нет. Во втором случае curry' = curry' . flip . curry (как ты сам написал), если существует обратная, то flip . curry = id, curry = id, что неверно.

Никакая модель не даст тебе построить обратную для curry, т.к. существование обратной в твоей модели вело бы к существованию обратной в деоретико-множественной модели (и в любой другой). А в ней это неинъективная функция.

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

Ну и с какими именно оговорками можно считать «термы определенного вида» в схеме и в хаскеле функциями?

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

Я же уже писал. curry :: narg -> 1arg, curry (lambda (x1 ... xn) body ...) = (lambda (x1) (lambda (x2) ... (lambda (xn) body ...) ...)).

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

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

что не отменяет наличия:

Hom(x1 × x2 × … × xN , z) ≅ Hom(x1, x2 → x3 → … → xN → z)

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

Я же уже писал. curry :: narg -> 1arg, curry (lambda (x1 ... xn) body ...) = (lambda (x1) (lambda (x2) ... (lambda (xn) body ...) ...)).

Это не определение, а какое-то говно. Определения пишутся так: «<определяемое понятие> — это такое <более общее понятие>, что <условия>».

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

Должно быть так

Что-то вроде

{-# LANGUAGE FlexibleInstances #-}

-- | Explicit functorial recursion. @f@ must be a functor.
data Mu t f = In { out :: f (Mu t f) } | Side t

-- | Infinite type for (Integer -> (Integer -> ...)) type scheme.
type InfInteger = Mu Integer ((->) Integer)

instance Show InfInteger where
  show (Side x) = show x
  show (In f) = show $ f undefined

f :: Integer -> InfInteger
f 0 = Side 0
f n = In $ \m -> if m == 0 then Side (m + n) else f (m + n)

-- > f 0
-- 0
-- > f 1
-- *** Exception: Prelude.undefined
-- > out (out (out (f 1) 2) 3) 0
-- 6
-- > out (out (out (f 1) 2) 3)
-- No instance for (Show (Integer -> Mu Integer ((->) Integer)))

Вот так:

f 0 = 0
f n = f . (+ n)

не получится:

Occurs check: cannot construct the infinite type: c0 = b0 -> c0

т.е. он выводит:

f :: Integer -> Integer
f :: Integer -> Integer -> Integer
f :: Integer -> Integer -> Integer -> Integer
...

а сформировать автоматически бесконечный тип не умеет.

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

Потому что хаскель - не конкантенативный ЯП и поинт-фри/каррирование реализовано на уровне кривых костылей, я об этом уже говорил.

В том примере дело в системе типов (infinite types - Integer -> Integer матчится с (a -> b), равно как и (Integer -> Integer -> Integer), но хаскель такого не позволяет, т.е. не создаёт тип (a -> b*), т.е. (a -> (b -> (b -> ...)))).

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

curry :: narg -> 1arg, curry (lambda (x1 ... xn) body ...) = (lambda (x1) (lambda (x2) ... (lambda (xn) body ...) ...)).

narg это произведение n типов? 1arg это тип? lambda (x1 ... xn) означает, что в языке есть поддержка не сахарных лямбд и аппликаций от нескольких аргументов? Что насчёт lambda (x1 ... xn . xs) - их поддержка тоже есть? Итого, это у тебя не любой ЯП, а scheme.

В первом случае curry вообще не функция, а ряд функций, но если определить ее как «объединение» ф-й этого ряда - то непонятно какую из uncarryn применять при конструировании обратной.

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

Во втором случае curry' = curry' . flip . curry (как ты сам написал), если существует обратная, то flip . curry = id, curry = id, что неверно.

Ты доказываешь, что curry' не инъективна, или что curry не инъективна? curry тут инъективна, curry' = curry' . curry (нужен flip или нет зависит от левой/правой ассоциативности (,) и (×)) когда тип аргумента curry' это функция из произведения и curry' = id в противном случае. Т.е., опять же, такая curry это сахар над обычной curry (с типом аргумента в виде функции из произведения двух типов)

Никакая модель не даст тебе построить обратную для curry, т.к. существование обратной в твоей модели вело бы к существованию обратной в деоретико-множественной модели (и в любой другой). А в ней это неинъективная функция.

curry в TK - биективная.

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

тебя уже 3 раза попросили привести ссылку на авторитетный источник

Авторитетный источник, в котором будет что? Определение функции curry? Ты дебил?

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

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

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

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

Это не определение, а какое-то говно. Определения пишутся так: «<определяемое понятие> — это такое <более общее понятие>, что <условия>».

У меня это и написано.

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

условие 1: curry :: narg -> 1arg

условие 2: curry (lambda (x1 ... xn) body ...) = (lambda (x1) (lambda (x2) ... (lambda (xn) body ...) ...))

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

В том примере дело в системе типов

Нет, если бы ты посомтрел на определение, то увидел бы, что дело не в этом. у него там во второй ветке ифа 1+f, без аппликации. Какие типы не ставь - оно не будет работать в аппликативном ЯП.

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

Кроме термов есть ещё типы и редукции, как минимум.

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

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

У меня это и написано.

Нет.

- это такая функция

Так, уже прогресс. Далее, что подразумевается под словом «функция»? Теоретико-множественная? Функция из какого-то языка программирования? Морфизм в какой-то категории?

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

narg это произведение n типов? 1arg

narg - тип функции >=1 аргументов, 1arg - тип функции одного аргумента.

lambda (x1 ... xn) означает, что в языке есть поддержка не сахарных лямбд и аппликаций от нескольких аргументов?

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

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

То есть сама curry в данном случае не функция и обратной у нее тоже нет. Потому что у не-функции обратной функции быть не может :)

Поступим так - если обратная ф-я есть, то определи ее :)

Ты доказываешь, что curry' не инъективна, или что curry не инъективна? curry тут инъективна, curry' = curry' . curry (нужен flip или нет зависит от левой/правой ассоциативности (,) и (×)) когда тип аргумента curry' это функция из произведения и curry' = id в противном случае. Т.е., опять же, такая curry это сахар над обычной curry (с типом аргумента в виде функции из произведения двух типов)

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

curry в TK - биективная.

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

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

Нет.

В каком месте нет? Что именно нет? Конкретнее.

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

Выше это уже сто раз обжовано, читай, я не собираюсь повторяться.

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

В каком месте нет? Что именно нет? Конкретнее.

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

Выше это уже сто раз обжовано, читай, я не собираюсь повторяться.

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

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

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

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