через типы - к реализации
Jul. 5th, 2006 04:31 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
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'
Многие так делают? Может быть есть еще ситуации где типы сильно помогают?
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'
Многие так делают? Может быть есть еще ситуации где типы сильно помогают?
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
![[community profile]](https://www.dreamwidth.org/img/silk/identity/community.png){kind=small}
no subject
Date: 2006-07-05 01:46 pm (UTC)Еще на эту тему можно погуглить "theorems for free".
no subject
Date: 2006-07-05 02:03 pm (UTC)Нашел, читаю взахлёб
Ссылки, чтобы не забыть:
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
Date: 2006-07-05 02:24 pm (UTC)Точнее, сейчас подумал, у меня это получается неосознанно.
Я иду не столько от самих типов, сколько от структуры функций, оперирующих над типами. Комбинаторика в чистом виде, с логическим обоснованием (довольно часто) каждого шага.
no subject
Date: 2006-07-05 02:31 pm (UTC)no subject
Date: 2006-07-05 03:10 pm (UTC)А пример... Ну, вот сегодня. Сочинял комбинатор
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
Date: 2006-07-05 06:38 pm (UTC)Слушай, а почему ты не пользуешься state как монадой? К чему все эти mapS, zipS?
no subject
Date: 2006-07-05 06:55 pm (UTC)Состояние требуется, когда надо сделать схему с состоянием. ;)
Например, с памятью - мое первое ее применение. ;)
no subject
Date: 2006-07-06 07:59 am (UTC)no subject
Date: 2006-07-06 08:23 am (UTC)no subject
Date: 2006-07-07 07:43 am (UTC)http://lomeo.livejournal.com/25099.html
no subject
Date: 2006-07-07 07:56 am (UTC)Надо этот метод применить для полезных вещей, наподобие решения систем квантовых дифференциальных уравнений. ;)
Мне надо генерировать данные в потоках и их соединять. Напрямую монада над самими потоками в этом мало поможет.
no subject
Date: 2006-07-07 08:33 am (UTC)Соединение в потоках то работает (если ты про zip)
streamZipWith fun = liftM2 fun
Так что монада поможет.
no subject
Date: 2006-07-07 08:44 am (UTC)Но мне кажется, это уже будет overdesign, некоторым образом.
Максимум, на что я сподоблюсь - если сподоблюсь вообще, - вот на такой трюк: http://www.brics.dk/RS/01/10/
Насчет решений квантовых систем я еще подумаю.
no subject
Date: 2006-07-07 09:56 am (UTC)> (map + '(1 2 3) ' (4 5 6) '(7 8 9))
(12 15 18)
Но до такой вещи не додумался. В принципе, неплохой способ, жалко только, что это всё проистекает не от хорошей жизни, а от проблем в типизации Хаскеля. Трюк, как ты говоришь.
no subject
Date: 2006-07-07 10:04 am (UTC)no subject
Date: 2006-07-07 02:08 pm (UTC)