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

[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

[ex-ex-zhuzh.livejournal.com]

Это замечательный способ. На мой взгляд, даже в каком-то смысле идеальный. То есть в идеальном языке он должен быть самым простым, естественным и основным способом написания программ. Я при любой возможности им пользуюсь.

Еще на эту тему можно погуглить "theorems for free".

[thesz.livejournal.com]

От типов я иду редко.

Точнее, сейчас подумал, у меня это получается неосознанно.

Я иду не столько от самих типов, сколько от структуры функций, оперирующих над типами. Комбинаторика в чистом виде, с логическим обоснованием (довольно часто) каждого шага.