![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Entry tags:
через типы - к реализации
Кстати, есть такой интересный способ мышления, когда для написания функции я думаю о её типе и вывожу реализацию из типа. Я его достаточно часто использую в 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'
Многие так делают? Может быть есть еще ситуации где типы сильно помогают?
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'
Многие так делают? Может быть есть еще ситуации где типы сильно помогают?
no subject
Еще на эту тему можно погуглить "theorems for free".
no subject
Нашел, читаю взахлёб
Ссылки, чтобы не забыть:
http://citeseer.ist.psu.edu/wadler89theorems.html - тут не качается что то :-/
http://portal.acm.org/citation.cfm?id=99404&dl=GUIDE&coll=ACM&CFID=15151515&CFTOKEN=6184618 отсюда взял
no subject
Точнее, сейчас подумал, у меня это получается неосознанно.
Я иду не столько от самих типов, сколько от структуры функций, оперирующих над типами. Комбинаторика в чистом виде, с логическим обоснованием (довольно часто) каждого шага.
no subject
no subject
А пример... Ну, вот сегодня. Сочинял комбинатор
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, из чего-то, наоборот, выдрать составную часть...Вот как-то так я и пишу. ;)
no subject
Слушай, а почему ты не пользуешься state как монадой? К чему все эти mapS, zipS?
no subject
Состояние требуется, когда надо сделать схему с состоянием. ;)
Например, с памятью - мое первое ее применение. ;)
no subject
no subject
no subject
http://lomeo.livejournal.com/25099.html
no subject
Надо этот метод применить для полезных вещей, наподобие решения систем квантовых дифференциальных уравнений. ;)
Мне надо генерировать данные в потоках и их соединять. Напрямую монада над самими потоками в этом мало поможет.
no subject
Соединение в потоках то работает (если ты про zip)
streamZipWith fun = liftM2 fun
Так что монада поможет.
no subject
Но мне кажется, это уже будет overdesign, некоторым образом.
Максимум, на что я сподоблюсь - если сподоблюсь вообще, - вот на такой трюк: http://www.brics.dk/RS/01/10/
Насчет решений квантовых систем я еще подумаю.
no subject
> (map + '(1 2 3) ' (4 5 6) '(7 8 9))
(12 15 18)
Но до такой вещи не додумался. В принципе, неплохой способ, жалко только, что это всё проистекает не от хорошей жизни, а от проблем в типизации Хаскеля. Трюк, как ты говоришь.
no subject
no subject