через типы - к реализации

[lomeo]

Кстати, есть такой интересный способ мышления, когда для написания функции я думаю о её типе и вывожу реализацию из типа. Я его достаточно часто использую в Haskell. Это вообще распространённая практика? Объясню на знакомом примере: например, мне надо написать функцию bind для State монады:



data State s a = State { runState :: s -> (a,s) }

Я знаю, что bind m f = join (fmap m f). Семантика join и fmap мне понятнее, чем bind, поэтому я буду писать через них. Функция join имеет тип m (m a) -> m a, т.е. State s (State s a) -> State s a. Т.е. нам нужно содрать один слой монады. У нас есть функция runState типа State s a -> s -> (a,s). Таким образом, применяя ее к первому аргументу (а у нас и нет ничего для State кроме конструктора и runState!) получим тип runState m :: s -> (State s a, s). Наша цель - получить отсюда (s -> (a,s)). Единственный способ, который бросается мне в глаза - это получить тип (State s a, s), а потом к его параметрам применить runState, чтобы получился тип State s a -> s -> (a,s), т.е. тот, который нам нужен. Разумеется, для этого мы обернём его конструктором и применим к (runState m) еще один аргумент, чтобы получить тип (State s a, s):

State $ \s -> doSomething (runState m s)

Итак у нас есть два типа State s a и s - это всё, что нам нужно для того, чтобы тип State s a вытащить наружу так, как мы это обсуждали:

State $ \s -> let (a,s') = runState m s in runState a s'

Это у нас join. Для fmap всё еще проще. Нам надо перевести тип State s a в тип State s b с помощью функции типа a -> b. Опять runState m имеет тип s -> (a,s). Для того, чтобы использовать функцию f :: a -> b необходимо вытащить параметр типа a, а для этого единственный способ - применить некий s к runState m. Ну, мы уже знаем, что для этого можно обернуть вызов конструктором и лямбдой:

State $ \s -> doSomething (runState m s)

Теперь runState m s :: (a,s) и мы легко вытаскиваем a и применяем к нему функцию f :: a -> b:

State $ \s -> let (a,s') = runState m s in (f a, s')

Это у нас fmap. Объединяем всё это в bind (к теме это не относится, но, дабы завершить - завершим) и получаем:

m >>= f = join (fmap f m) = State $ \s -> let (a,s') = runState (State $ \s -> let (a,s') = runState m s in (f a, s')) s in runState a s'

или после сокращений:

m >>= f = State $ \s -> let (a,s') = runState m s in runState (f a) s'


Многие так делают? Может быть есть еще ситуации где типы сильно помогают?

Comments

[lomeo.livejournal.com]

Как это? Можно пример? И что такое "структура функций, оперирующих над типами"?

[thesz.livejournal.com]

Ну, тип функции, в виде дерева.

А пример... Ну, вот сегодня. Сочинял комбинатор threadS startstate transformer inputs.

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

Первый вариант:

threadS startstate transformer inputs = ...
    where
        f i s = runSSt (transformer i) s

Это как раз то протягивание состояния.

У нас есть комбинатор zipS :: S a -> S b -> S (a,b) и mapS :: (a -> b) -> S a -> S b.

Мы можем собрать входы и входные состояния вместе через zipS и применить к ним mapS f, только f надо немного поменять:

threadS startstate transformer inputs = ...
    where
        inputsstates = zipS inputs states
        outsstates = mapS f inputsstates -- :: S (o,s)
        f (i,s) = runSSt (transformer i) s

Выходные состояния получить просто, также, как и выходы:

threadS startstate transformer inputs = outs
    where
        inputsstates = zipS inputs states
        outsstates = mapS f inputsstates   -- :: S (o,s)
        states' = mapS snd outsstates      -- :: S s
        states = delayS startstate states' -- :: S s
        outs = mapS fst outsstates         -- :: S o
        f (i,s) = runSSt (transformer i) s

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

Вот как-то так я и пишу. ;)

[lomeo.livejournal.com]

Понятно, спасибо.
Слушай, а почему ты не пользуешься state как монадой? К чему все эти mapS, zipS?

[thesz.livejournal.com]

S - это бесконечный поток событий. Все тот же самый data S a = S a (S a).

Состояние требуется, когда надо сделать схему с состоянием. ;)

Например, с памятью - мое первое ее применение. ;)

[lomeo.livejournal.com]

Да, с таким типом монаду не сделаешь :-/

[thesz.livejournal.com]

Мы ее параллельно пристегнем. ;)

[lomeo.livejournal.com]

Получилось, но вроде не то, что тебе нужно, нес па?
http://lomeo.livejournal.com/25099.html

[thesz.livejournal.com]

Прочитал. Почти все понял.

Надо этот метод применить для полезных вещей, наподобие решения систем квантовых дифференциальных уравнений. ;)

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

[lomeo.livejournal.com]

Что такое квантновые дифуры не знаю :-(

Соединение в потоках то работает (если ты про zip)

streamZipWith fun = liftM2 fun

Так что монада поможет.

[thesz.livejournal.com]

Похоже, поможет.

Но мне кажется, это уже будет overdesign, некоторым образом.

Максимум, на что я сподоблюсь - если сподоблюсь вообще, - вот на такой трюк: http://www.brics.dk/RS/01/10/

Насчет решений квантовых систем я еще подумаю.

[lomeo.livejournal.com]

Прочитал, спасибо, очень симпатичная вещь, я тоже одно время думал о неудобстве zipWithN, помня о таком простом и удобном лисповом map:

> (map + '(1 2 3) ' (4 5 6) '(7 8 9))
(12 15 18)

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

[thesz.livejournal.com]

Всем бы такие проблемы. ;)

[lomeo.livejournal.com]

У меня непритязательный вкус: мне вполне достаточно самого лучшего. (Окар Уайльд)