Перехват исключений

http://www.haskell.org/haskellwiki/Anonymous_function

Почему обрабочик исключения имеет вид λ-терма

Потому что он должен получить описание ошибки (в твоём случае параметр e)

Это анонимная (лямбда) функция. Вместо неё можно воткнуть обычную.

catch (openFile f ReadMode) exceptionHandler
    where
        exceptionHandler e =
            hPutStr stderr ("Couldn’t open " ++
            f ++
            ": " ++
            show e))

Если С++ знаешь, то такая идея:

#include <functional>

// catch :: Exception e => IO a -> (e -> IO a) -> IO a
template <typename A, typename E>
A ctch(std::function<A()> const& af, std::function<A(E const&)> const& ef) {
    try {
        return af();
    } catch (E const& e) {
        return ef(e);
    }
}

#include <cstdio>

int main() {
    printf(
        "%d\n",
        // catch (do throw 42; return 1) (\(e :: Int) -> do print e; return 2)
        ctch<int, int>(
            []() { throw 42; return 1; },
            [](int const& e) { printf("%d\n", e); return 2; }
        )
    );
}

потому что catch это 2х параметрическая функция, а не управляющая структура.

Prelude> :t Prelude.catch
Prelude.catch :: IO a -> (IOError -> IO a) -> IO a
Prelude> :t Control.Exception.catch
Control.Exception.catch
:: GHC.Exception.Exception e => IO a -> (e -> IO a) -> IO a

Почему обрабочик исключения имеет вид λ-терма, и что такое е?

Потому что e — это стрелка. Единственный вариант, который я пока вижу. Нужно просто-типизированное LC это будет одна конструкция из стрелок/2-стрелок, нужно LC с зависимыми типами - другая, с субструктурными (линейными, в частности) - ещё третья. Т.е. фиксированное подмножество теории категорий само по себе довольно бедная метатеория, просто язык, в котором можно выразить все эти вещи. Мартин-Лёф предлагал формулировать разные теории типов в рамках метатеории LF, вот также это можно делать в рамках метатеории ТК.

Ну, например, берём декартово-замкнутую категорию Set, она же классический топос, т.е. категория всех малых множеств и тотальных функций, в agda она так и называется - «Set». Берём категорию всех малых категорий и функторов Cat (Set1 в agda) и утверждаем:

• Любой тип который может использоваться (ADTs, GADTs, Inductive families) это объект Set (объект топоса, в общем случае), т.е., как следствие, множество - множество всех термов данного типа.
• Любой параметрически-полиморфный тип это эндофунктор на Set, т.е. специального вида стрелка в Cat. (Непараметрический тип, который объект в Set, это вырожденный случай функтора из терминальной категории (как-то так)).
• Любой конструктор типа данных который может быть это стрелка в Set (стрелка в топосе, вообще).
• Любая функция которая может быть это тоже стрелка в Set, но отдельным классом (чтобы не путать стрелки-конструкторы и стрелки-функции). Как следствие, «функция» - тотальная функция между множествами.
• Любая композиция стрелок с учётом декартовых произведений и экспоненциалов это любой правильно составленный терм в данной системе (тут типизация из коробки).
• Любое определение конкретной редукции это 2-стрелка (струнная диаграмма).
• Любой конкретный ход редукций (вычислений) это композиции 2-стрелок (струнных диаграмм). + Правила построения редукций из коробки.

Например:

-- Тут рисуем коммутативную диаграмму:
ℕ : Set
0 : 1 → ℕ
s : ℕ → ℕ

-- Продолжаем коммутативную диаграмму:
+ : ℕ → (ℕ → ℕ)

-- Рисуем две струнных диаграммы, которые можно сочетать:
e₁(+) : + ∘ a ∘ 0 ⇒ a
e₂(+) : + ∘ a ∘ (s ∘ b) ⇒ s ∘ (+ ∘ a ∘ b)

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

Тут ещё интересно, что можно легко добавлять конструкторы и правила редукций (как если бы в хаскеле можно было дописывать ADT и pattern matching cases по разным модулям).

Сами по себе 2-стрелки это непосредственно струнные диаграммы, т.е., рисуя коммутативные диаграммы, получим схемы типов, рисуя струнные - flow chart.

• Любая конкретная оптимизация это 3-стрелка. Правила построения оптимизаций тоже из коробки.

Например, если есть линейная рекурсия:

f x = z
f y = g (f (h y))

(f не появляется в g и h), т.е.:

-- любая стрелка вида:
f : x + y → r

-- с 2-стрелками вида:
e₁(f) : f ∘ x ⇒ z
e₂(f) : f ∘ y ⇒ g ∘ f ∘ h ∘ y

то она убирается такой 3-стрелкой:

-- Рисуем диаграмму между струнными:
o(f, f′) : e(f) ≡> e(f′ ∘ z)

-- TCO форма:
e₁(f′) : f′ ∘ a ∘ x ⇒ a
e₂(f′) : f′ ∘ a ∘ y ⇒ f′ ∘ (g ∘ a) ∘ (h ∘ y)

и остаётся только TCO.

Процесс унификации по 3-стрелкам это процесс оптимизаций, а процесс унификации по 2-стрелкам - интерпретации или компиляции (тогда нужен target). Как компилировать в target - конструкторы, например, достаточно точно отражаются в си-подобные структуры и объединения в памяти, можно даже в случае (s : ℕ → ℕ) или (_:_ : a → [a] → [a]) или вообще (con : [no `t' appears] → t → t) пытаться делать не связные списки, а аллоцируемые/реаллоцируемые массивы. Про компиляцию редукций ничего не скажу - только, наверно, тут, в первую очередь, нужен критерий линейности представляемого терма и/или его линеаризация.

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

Поговорил с пастой - день прошел не зря.

кушать и спать не охота, вот и тянет пообщаться.

почему паста?

Потому что я где-то это уже видел.

Ну так должен же обработчик получить само исключение. Вот он его и получает, в параметре e.

Хотя такой код не скомпилируется. Ибо openFile возвращает Handle, а hPutStr — (). А catch требует, чтобы обе ветки давали результат одного типа. Можно сделать так:

catch (mapM Just $ openFile f ReadMode)
     (\e -> hPutStr stderr ("Couldn't open " ++ f ++ ": " ++ show e)
            >> return Nothing)

Почему обрабочик исключения имеет вид λ-терма, и что такое е?
Это анонимная (лямбда) функция. Вместо неё можно воткнуть обычную.
потому что catch это 2х параметрическая функция, а не управляющая структура.
Потому что e — это стрелка.
Хотя такой код не скомпилируется.

Охренеть. В хаскелле, чтобы обработать исключение, надо скурить лямбда-исчисление, исчисление предикатов, дискретку и теоркат? После этого хаскель кто-то вообще воспринимает всерьёз?

В то время как в нормальных языках это просто работает.

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

почему паста?

потому что это старое сообщение quasimoto на совсем другую тему. к предмету обсуждения отношения не имеет

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

Нет, конечно.

Но вот систему типов понимать надо. В конце концов, в каких-нибудь плюсах ты тоже не станешь писать

try {
  ...
  return "Success";
} catch (const MyException e&) {
  ...
  return 1;
}

это старое сообщение quasimoto

+. Определяю его сообщения (которые, обычно, не влезают в экран) с первых строк :)

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

Не надо.

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

Не надо.

почему паста?

https://www.google.com/search?q="Ну%2C например%2C берём декартово-замкн...

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

Не надо.

ORLY? Так напиши же «Hello, World!» на Хачкиле, а мы посмотрим.

main = putStrLn «Hello, world»

Ну, и что такое putStrLn?

Ты бы спросил лучше, что такое main

В main ляжет то, что вернет putStrLn. Ну, и что же это будет?

Ну, и что такое putStrLn?

функция

действие вывода «Hello world» на экран

функция

И что она возвращает? И да, что такое main?

И что она возвращает?

Возвращает действие IO()

И да, что такое main?

«действие», которое будет выполнено при запуске программы

И что она возвращает?

putStrLn :: String -> IO ()

«действие», которое будет выполнено при запуске программы

Что значит «действие»? Разве IO — это не монада?

Прямой аналог сишного

#include <stdio.h>
int main(){
    puts("Hello, world");
}

Prelude> :i putStrLn
putStrLn :: String -> IO () 	-- Defined in `System.IO'
Prelude> :i String
type String = [Char] 	-- Defined in `GHC.Base'
Prelude> :i Char
data Char = GHC.Types.C# GHC.Prim.Char# 	-- Defined in `GHC.Types'
instance Bounded Char -- Defined in `GHC.Enum'
instance Enum Char -- Defined in `GHC.Enum'
instance Eq Char -- Defined in `GHC.Classes'
instance Ord Char -- Defined in `GHC.Classes'
instance Read Char -- Defined in `GHC.Read'
instance Show Char -- Defined in `GHC.Show'
Prelude> :i GHC.Prim.Char#
data GHC.Prim.Char# 	-- Defined in `GHC.Prim'
Prelude> :i []
data [] a = [] | a : [a] 	-- Defined in `GHC.Types'
instance Eq a => Eq [a] -- Defined in `GHC.Classes'
instance Monad [] -- Defined in `GHC.Base'
instance Functor [] -- Defined in `GHC.Base'
instance Ord a => Ord [a] -- Defined in `GHC.Classes'
instance Read a => Read [a] -- Defined in `GHC.Read'
instance Show a => Show [a] -- Defined in `GHC.Show'
Prelude> :i (->)
data (->) a b 	-- Defined in `GHC.Prim'
instance Monad ((->) r) -- Defined in `GHC.Base'
instance Functor ((->) r) -- Defined in `GHC.Base'
Prelude> :i ()
data () = () 	-- Defined in `GHC.Tuple'
instance Bounded () -- Defined in `GHC.Enum'
instance Enum () -- Defined in `GHC.Enum'
instance Eq () -- Defined in `GHC.Classes'
instance Ord () -- Defined in `GHC.Classes'
instance Read () -- Defined in `GHC.Read'
instance Show () -- Defined in `GHC.Show'
Prelude> :i IO
newtype IO a
  = GHC.Types.IO (GHC.Prim.State# GHC.Prim.RealWorld
                  -> (# GHC.Prim.State# GHC.Prim.RealWorld, a #))
  	-- Defined in `GHC.Types'
instance Monad IO -- Defined in `GHC.Base'
instance Functor IO -- Defined in `GHC.Base'
Prelude> :i GHC.Prim.State#
data GHC.Prim.State# a 	-- Defined in `GHC.Prim'
Prelude> :i GHC.Prim.RealWorld
data GHC.Prim.RealWorld 	-- Defined in `GHC.Prim'
Prelude> :i Monad
... Functor, Eq, etc.

http://blog.ezyang.com/2011/05/unraveling-the-mystery-of-the-io-monad/

Что значит «действие»? Разве IO — это не монада?

IO - тип

Функции возвращают значения. Значение putStrLn «hi!» имеет тип IO, для которого действительно выполняются монадические правила

Что значит «действие»? Разве IO — это не монада?

ты не тот анон. неправильный

IO - это монада действия. но чтобы ее использовать, знать, что такое монада, нафиг не надо

IO - это монада действия. но чтобы ее использовать, знать, что такое монада, нафиг не надо

Т.е. в Хацкеле поощряется использование языка «вслепую», без понимания его механизмов?

И это все для того, чтобы понять, как работает «Hello, World»? Однако!

Что «всё»? Я спрашивал :i начиная от putStrLn и пока все фигурирующие типы не закончились (классы типов уж не стал). А теперь открой man 3 puts и продолжай читать их же и стандарт (или учебник) пока все встречающиеся термины не станут понятны (int, char, *, const, stdout и т.п.).

А так — что putStrLn, что puts «печатают на stdout». [ putStrLn "..." ] = [ puts "..." ] = либцэ/ОС(горшочек, вари!). Что ещё нужно?

А теперь открой man 3 puts и продолжай читать их же и стандарт (или учебник) пока все встречающиеся термины не станут понятны (int, char, *, const, stdout и т.п.).

Эти термины мне понятны. Что в них сложного?

А так — что putStrLn, что puts «печатают на stdout»

Ну разумеется.

puts: ssize_t write(int fd, const void *buf, size_t count)

putStrLn: (простыня из типов, инстансов, монад, функторов, морфизмов и т.п.)

Эти термины мне понятны.

Отлично.

А зачем ты сравниваешь write и putStrLn? Вот:

ssize_t write(int fd, const void *buf, size_t count);

fdWriteBuf :: Fd -> Ptr Word8 -> ByteCount -> IO ByteCount

int puts(const char *s);

putStrLn :: String -> IO ()

простыня из типов, инстансов, монад, функторов, морфизмов и т.п.

Ты троллишь прикидываясь тупым или тупишь прикидываясь троллем?)

Сам первый обмазался монадами, функторами, морфизмами и т.п. — сам придумал проблемы. А навертеть-то что ты перечислил можно где угодно, например — http://www.softlab.ntua.gr/~nickie/Papers/papaspyrou-2001-dsac.pdf. И вообще — если функция это морфизм в категории типов, а, например, конструктор функционального типа при фиксированном типе аргумента — эндофунктор и соответствующая монада в ней же, то это так, вне зависимости от того говорим мы об этом или нет. А если хочется об этом не говорить — ок, в сабжевом языке есть абстрактный тип IO и вполне конкретный типаж Monad (который, почему-то, называется именно так — хрен знает почему).

putStrLn: (простыня из типов, инстансов, монад, функторов, морфизмов и т.п.)

Ты бредишь.

Я вот тут перечитал ваш пример, и у меня возникла пара вопросов. Во первых вы описываете exceptionHandler e как функцию, принимающую 1 аргумент, а вызываете её вообще без аргументов

catch (openFile f ReadMode) exceptionHandler

catch :: Exception e => IO a -> (e -> IO a) -> IO a

Функция catch имет аргумент (e -> IO a) аргумент должен быть функцией высшего порядка (high-order function). Он принимает аргумент котырый указывает какое Исключение было выброшено, эта функция будет применена функцией catch в том случае если произойдет что-то нехорошее. Аргумент будет передан из функции catch.

Скобка и правда лишняя, опечатка