Функциональное программирование — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(Кр2)
м (rollbackEdits.php mass rollback)
 
(не показаны 63 промежуточные версии 7 участников)
Строка 8: Строка 8:
 
* аппликация левоассоциативна: a b c d <tex> \Rightarrow </tex> ((a b) c) d
 
* аппликация левоассоциативна: a b c d <tex> \Rightarrow </tex> ((a b) c) d
 
* сокращения раскрываются во вложенные лямбды (сразу с расставлением скобок): λ a b c . M <tex> \Rightarrow </tex> λ a . (λ b . (λ c . (M)))
 
* сокращения раскрываются во вложенные лямбды (сразу с расставлением скобок): λ a b c . M <tex> \Rightarrow </tex> λ a . (λ b . (λ c . (M)))
Важно: тело абстракции забирает всё до конца то скобки, в которую заключено
+
Важно: тело абстракции забирает всё до конца той скобки, в которую заключена.
  
 
Итого: ((((λ a . (λ b . ((λ c . (λ d . (λ e . (e)))) a))) (x y)) y) (λ f . (x))) y
 
Итого: ((((λ a . (λ b . ((λ c . (λ d . (λ e . (e)))) a))) (x y)) y) (λ f . (x))) y
Строка 19: Строка 19:
  
 
=== Решение ===
 
=== Решение ===
В нормальной форме нет редукций. Если нормальная форма существует, то её можно достичь при помощи редукций нормальным порядком, а аппликативным можно и достичь.
+
В нормальной форме нет редукций. Если нормальная форма существует, то её можно достичь при помощи редукций [[#Нормальный порядок редукции|нормальным порядком]], а [[#Аппликативный порядок редукции|аппликативным]] можно и не достичь.
  
 
# Уже в нормальное форме, как ни странно
 
# Уже в нормальное форме, как ни странно
# λ b . y
+
# λ a . y
  
 
==Нормальный порядок редукции==
 
==Нормальный порядок редукции==
Строка 29: Строка 29:
 
[http://softoption.us/content/node/46 Здесь] про стратегии редуцирования с примерами и определениями.
 
[http://softoption.us/content/node/46 Здесь] про стратегии редуцирования с примерами и определениями.
  
'''Нормальный порядок редуцирования''' {{---}} самым первым делом раскрывается самый левый самый внешний редекс.
+
'''Нормальный порядок редуцирования''' {{---}} сначала раскрывается самый левый самый внешний редекс.
 
Пример не очень удачный, так в нём всего одна редукция, после которой получится: y (y (y (λ b . (x (x (x (λ c d . d) y)) x)))) y
 
Пример не очень удачный, так в нём всего одна редукция, после которой получится: y (y (y (λ b . (x (x (x (λ c d . d) y)) x)))) y
  
Строка 39: Строка 39:
 
[http://pv.bstu.ru/flp/fpLectures.pdf Здесь] ещё про стратегии редуцирования, но немного другим языком (может быть, кому-то более понятным).
 
[http://pv.bstu.ru/flp/fpLectures.pdf Здесь] ещё про стратегии редуцирования, но немного другим языком (может быть, кому-то более понятным).
  
'''Аппликативный порядок редуцирования''' {{---}} первым делом редуцирования самый правый самый глубокий терм. То есть сначала упрощаем "аргументы" аппликации.
+
'''Аппликативный порядок редуцирования''' {{---}} первым делом редуцируем самый левый самый глубокий терм. То есть сначала упрощаем "аргументы" аппликации.
  
 
Те же примеры (во всех случаях одна редукция будет произведена):
 
Те же примеры (во всех случаях одна редукция будет произведена):
Строка 47: Строка 47:
 
((λ x . y) (λ z . t)) ((λ a b c . a b c ((λ s . t) y) (λ t . x) u) (λ x . x)) ((λ x . x x) z) <tex> \Rightarrow </tex>
 
((λ x . y) (λ z . t)) ((λ a b c . a b c ((λ s . t) y) (λ t . x) u) (λ x . x)) ((λ x . x x) z) <tex> \Rightarrow </tex>
 
((λ x . y) (λ z . t)) ((λ a b c . a b c ((λ s . t) y) (λ t . x) u) (λ x . x)) (z z)
 
((λ x . y) (λ z . t)) ((λ a b c . a b c ((λ s . t) y) (λ t . x) u) (λ x . x)) (z z)
 +
 +
== Ленивый порядок редукции ==
 +
 +
'''Ленивый порядок редуцирования''' {{---}} это когда мы якобы заворачиваем терм в коробку, и если делаем редукцию в одном из термов коробки, то она делается во всех. При этом сам порядок редуцирования нормальный.
 +
 +
То есть пример:
 +
 +
(λ f . f f) ((λ x . x) z)
 +
 +
Сначала делаем обычную редукцию нормальным порядком и получаем:
 +
 +
((λ x . x) z) ((λ x . x) z)
 +
 +
А потом после редукции нормальным порядком надо сделать изменения сразу в двух термах, потому что они якобы в коробках, и получим суммарно за 2 редукции:
 +
 +
z z
  
 
==Выписать систему уравнений типизации==
 
==Выписать систему уравнений типизации==
Строка 54: Строка 70:
 
Сначала надо дать типы всем термам и подтермам, раздавая каждый раз новые буквы новым переменным и термам. А потом связать эти буквы по следующим правилам:
 
Сначала надо дать типы всем термам и подтермам, раздавая каждый раз новые буквы новым переменным и термам. А потом связать эти буквы по следующим правилам:
 
* если у нас абстракция (λ x . M) :: T0, x :: T1, M :: T2, то добавляем в систему T0 = T1 -> T2,
 
* если у нас абстракция (λ x . M) :: T0, x :: T1, M :: T2, то добавляем в систему T0 = T1 -> T2,
* если имеет аппликацию (M N) :: T0, M :: T1, N :: T2, то добавляем T1 = T2 -> T0
+
* если имеем аппликацию (M N) :: T0, M :: T1, N :: T2, то добавляем T1 = T2 -> T0
 
* если у нас переменная в теле абстракции встречается несколько раз и мы раздаём каждый раз ей новые буквы, то надо будет потом приравнять типы в аргументе абстракции и внутри её тела.
 
* если у нас переменная в теле абстракции встречается несколько раз и мы раздаём каждый раз ей новые буквы, то надо будет потом приравнять типы в аргументе абстракции и внутри её тела.
  
Строка 118: Строка 134:
 
* [https://pp.vk.me/c625826/v625826822/9174/QRhQIqwNX5Q.jpg]
 
* [https://pp.vk.me/c625826/v625826822/9174/QRhQIqwNX5Q.jpg]
  
Разбор будет по фоткам 3 и 4 (остальные задания аналогичны):
+
Разбор будет по фоткам 3, 4, 5 (остальные задания аналогичны):
  
 
== N1. Порядок редуцирования ==
 
== N1. Порядок редуцирования ==
Строка 125: Строка 141:
 
== E0. Определить примитивные конструкции ==  
 
== E0. Определить примитивные конструкции ==  
  
* pair = \ x y p . p x y
+
pair = \ x y p . p x y
 +
fst  = \ r . r (\ x y . x)
 +
snd  = \ r . r (\ x y . y)
 +
fix  = \ f . (\ x . f (x x)) (\ x . f (x x))
 +
 
 +
Легко проверить, что fst (pair a b) = a, подставив и сделав редукции.
 +
 
 +
== E1. Превратить let-биндинги в один большой лямбда-терм. ==
 +
 
 +
Конструкция
 +
 
 +
'''let''' x = z '''in''' y
 +
 
 +
превращается в
 +
 
 +
(\x . y) z
 +
 
 +
А пример просто превратится в
 +
 
 +
(\foo. [main]) [foo]
 +
 
 +
где [foo] {{---}} тело foo, [main] {{---}} тело main.
 +
 
 +
== E2. let-биндинги, но с возможной взаимной рекурсией ==
 +
 
 +
foo = foo ((\ a . bar) foo)
 +
 
 +
bar = (\ a . y) y (\ b . y)
 +
 
 +
main = (\ a . foo (a z) (y y)) y
 +
 
 +
=== Решение ===
 +
<font color=magenta> '''Осторожно! Магия''' </font>
 +
 
 +
Расписывать формальный алгоритм довольно нудно и неприятно, поэтому здесь объяснение того, что происходит, а на примере должно быть понятно.
 +
 
 +
Сначала по каждому терму из условия надо составить терм с таким же именем, только штрихованный. В нём мы будем использовать первые буквы остальных термов. Фиксируем порядок аргументов, например для foo' это будет f b m. Тогда у всех остальных термов будет циклический порядок. То есть для bar' будет b m f, а для main' {{---}} m f b.
 +
 
 +
Теперь пишем foo'. Сначала используем fix. Потом абстракцию, аргументами которой является нужный набор из циклических перестановок (см. соответствие выше), а телом абстракции является тело foo с изменениями. Если встречается имя терма из задания, то надо его заменить на нужный циклический порядок. И если имена первых букв по каким-то причинам не подходят (коллизятся со связанными переменными), то надо более удачные имена этим переменным придумать.
 +
 
 +
Итого, после преобразований:
 +
 
 +
foo'  = fix (\ f b m . f b m ((\ a . b m f) (f b m)))
 +
bar'  = fix (\ b m f . (\ a . y) y (\ b . y))
 +
main' = fix (\ m f b . (\ a . f b m (a z) (y y)) y)
 +
 
 +
Результирующий терм выглядит как вызов штрихованной функции в нужной циклической перестановке:
 +
 
 +
main = main' foo' bar'
 +
 
 +
Но так как в этом задании дополнительные термы использовать нельзя, то main', foo', bar' надо проинлайнить в main.
 +
 
 +
== N2. Раскрыть, как в E1 и нормализовать ==
 +
 
 +
В общем, в задании всё сказано. Надо превратить в один большой терм как в E1, а затем нормализовать, как в задании из первой кр.
 +
 
 +
== S1. Расписать систему уравнений типов ==
 +
 
 +
Как в первой кр.
 +
 
 +
== TP1. Убрать сокращения и расставить скобки ==
 +
 
 +
Именно это и требуется сделать. Разве что там вместо тела абстракции расписан её тип. А (->) в типе в отличие от аппликации правоассоциативна, то есть в
 +
 
 +
a -> b -> c
 +
 
 +
скобки ставятся следующим образом:
 +
 
 +
a -> (b -> c)
 +
 
 +
Итого:
 +
* дано: (\ a b . b -> b -> a) x
 +
* получается: (\ a . (\ b . b -> (b -> a))) x // вроде бы тут как раз весь тип внутри не надо заключать в скобки
 +
 
 +
== TF1. Составить терм по типу ==
 +
 
 +
Тут надо пользоваться логикой. Вроде бы во всех примерах можно решить методом пристального взгляда. Мотивация: чтобы решение системы уравнений типов совпадало с полученным типом. Но в некоторых случаях довольно трудно (или даже невозможно) придумать терм по типу, например здесь не придумывается:
 +
 
 +
(a -> b) -> b -> a
 +
 
 +
=== Решение ===
 +
 
 +
Дано: forall a b c . (b -> c -> a) -> (c -> b) -> c -> a
 +
 
 +
Ответ: \f g c . f (g c) c
 +
 
 +
== A1. Закодировать типы по Чёрчу (без взаимной рекурсии) ==
 +
 
 +
<code>
 +
  '''data''' Doctor a = Minute a | Maybe a a a
 +
  '''data''' Hour a b = Hour (Hour b b) (Doctor a) (Doctor b) | Roll b (Doctor a)
 +
</code>
 +
 
 +
=== Решение ===
 +
У каждого типа есть <tex> N \geqslant 1</tex> конструктов, а у каждого конструктора есть <tex> K \geqslant 0 </tex> аргументов.
 +
 
 +
Фиксируем тип с <tex> N </tex> конструкторами. Каждый конструктор <tex> C_i </tex> этого типа превращается в абстракцию, в которой сначала идут <tex> K_i </tex> переменных {{---}} аргументы конструктора, а потом <tex> N </tex> переменных, отвечающих конструкторам. В теле просто выбирается нужный конструктор и применяется ко всем аргументам.
 +
 
 +
caseTypeName тоже является абстракцией, которая принимает сначала одну переменную, которая "выбирает" нужный конструктор, затем набор переменных в количестве числа конструкторов. В теле просто применяется первая переменная ко всем остальным.
 +
 
 +
<code>
 +
  <font color=green>-- сначала Doctor </font>
 +
  Minute = \ a . \ x y . x a
 +
  Maybe  = \ a b c . \ x y . y a b c
 +
  caseDoctor = \ p . \ x y . p x y
 +
  <font color=green>-- теперь Hour </font>
 +
  Hour = \ a b c . \ x y . x a b c
 +
  Roll = \ a b . \ x y . y a b
 +
  caseHour = \ p . \ x y . p x y
 +
</code>
 +
 
 +
Интересное наблюдение: переменная p в case является как раз нужным конструктором, в котором уже подставлены все аргументы этого конструктора.
 +
 
 +
== A2. Закодировать типы через <tex> \mu </tex> - комбинатор ==
 +
 
 +
'''data''' Return a b = List (Return b a) (Return b a) b | Roll (Return a a) (Return a a) (Mice a)
 +
'''data''' Mice a = Bucket (Mice a) (Return a a) | Haystack (Mice a) a
 +
 
 +
=== Решение ===
 +
 
 +
<font color=magenta> '''Магия как в E2!''' </font>
 +
 
 +
Опять делаем соотвествие между TypeName и TypeName'. Чтобы написать TypeName', необходимо преобразовать объявление дататипов по следующим правилам:
 +
* сначала идёт mu (это как fix, только для типов),
 +
* потом какая-нибудь уникальная буква для типа (например x для Return и y для Mice),
 +
* после точки абстракция, которая сначала принимает в качестве аргумента другую уникальную букву, а затем аргументами параметры типа,
 +
* T1 | T2 заменяется на T1 + T2,
 +
* T1 T2 заменяется на T1 <tex> \times </tex> T2,
 +
* параметры типа оставляем как есть,
 +
* если в конструкторе идёт наш тип, то пишем нашу уникальную букву, а затем уникальную букву другого типа, а если другой типа {{---}} наоборот; после чего параметры конструктора,
 +
* если тип не наш и не буковка параметр датайпа, и не принимает параметров (например Nothing), то пишем 1 вместо неё.
 +
 
 +
Return' = mu x . \ y . \ a b . (x y b a) <tex> \times </tex> (x y b a) <tex> \times </tex> b + (x y a a) <tex> \times </tex> (x y a a) <tex> \times </tex> (y x a)
 +
Mice'  = mu y . \ x . \ a . (y x a) <tex> \times </tex> (x y a a) + (y x a) <tex> \times </tex> a
 +
 
 +
После этого пишем ответ:
 +
 
 +
Return = Return' Mice'
 +
Mice  = Mice' Return'
 +
 
 +
== H1. Написать Haskell-код какой-нибудь структуру данных ==
 +
 
 +
* [[Квадродеревья | Квадродерево]]: [http://pastebin.com/jV4DeRvv ссылка на pastebin]
 +
*: не совсем то, что требует Ян, но я пока не распарсил то, что он требует; возможно, более правильная версия появится позже
  
 
=Кр3=
 
=Кр3=
 +
===ITMOPrelude===
 +
#gromakovsky
 +
#* [https://github.com/gromakovsky/haskell-course-ru/blob/master/ITMOPrelude/Primitive.hs Primitive.hs]
 +
#* [https://github.com/gromakovsky/haskell-course-ru/blob/master/ITMOPrelude/List.hs List.hs]
 +
# yakupov
 +
#* [https://github.com/yakupov/Haskell_lab/blob/master/ITMOPrelude/Primitive.hs Primitive.hs]
 +
#* [https://github.com/yakupov/Haskell_lab/blob/master/ITMOPrelude/List.hs List.hs]
 +
# itanf
 +
#* [https://github.com/itanf/ITMO-Training-FunctionalProgramming/blob/master/ITMOPrelude/Primitive.hs Primitive.hs]
 +
#* [https://github.com/itanf/ITMO-Training-FunctionalProgramming/blob/master/ITMOPrelude/List.hs List.hs]
 +
 +
==Primitive==
 +
===Nat===
 +
data Nat
 +
(+.)
 +
(-.)
 +
(*.)
 +
 +
divides :: Nat -> Nat -> Bool
 +
 +
===Rat===
 +
data Rat
 +
(%+)
 +
(%-)
 +
(%*)
 +
(%/)
 +
 +
euler :: ?
 +
 +
==List==
 +
 +
===Угадайка===
 +
Дают тип, надо написать название функции из '''List.hs''' и реализовать её.
 +
 +
===Комбинаторика===
 +
 +
'''Тут можно использовать только набор заранее определённых функций листа( среди которых нет даже ''++'' )'''
 +
 +
subsequences :: [a] -> [ [ a ] ]
 +
 +
permutations :: [a] -> [ [ a ] ]
 +
 +
==Algebra==
 +
class Monoid a where
 +
mempty :: a
 +
mappend :: a -> a -> a
 +
 +
class Monoid a => Group a where
 +
ginv :: a -> a
 +
 +
mconcat :: (Monoid a) => List a -> a
 +
mconcat = foldr mappend mempty
 +
 +
instance Monoid Unit where
 +
mempty   = Unit
 +
mappend _ _ = Unit
 +
 +
instance Group Unit where
 +
ginv _ = Unit
 +
 +
instance (Monoid a, Monoid b) => Monoid (Pair a b) where
 +
mempty   = Pair mempty mempty
 +
mappend a b = Pair {fst = fst a `mappend` fst b,
 +
snd = snd b `mappend` snd b}
 +
 +
instance (Monoid a) => Monoid (Maybe a) where
 +
mempty = Just mempty
 +
mappend (Just a) (Just b) = Just $ mappend a b
 +
mappend _ _   = Nothing
 +
 +
newtype First a = First { getFirst :: Maybe a}
 +
 +
instance Monoid (First a) where
 +
mempty = First Nothing
 +
mappend (First Nothing) x = x
 +
mappend x _   = x
 +
 +
newtype Last a = Last { getLast :: Maybe a}
 +
 +
instance Monoid (Last a) where
 +
mempty   = Last Nothing
 +
mappend x (Last Nothing) = x
 +
mappend _ x   = x
 +
 +
newtype Any = Any { getAny :: Bool }
 +
 +
instance Monoid Any where
 +
mempty   = Any False
 +
mappend (Any a) (Any b) = Any $ a || b
 +
 +
newtype All = All { getAll :: Bool }
 +
 +
instance Monoid All where
 +
mempty   = All True
 +
mappend (All a) (All b) = All $ a && b
 +
 +
-- Лексикографическое сравнение
 +
instance Monoid Tri where
 +
mempty   = EQ
 +
mappend LT _ = LT
 +
mappend EQ a = a
 +
mappend GT _ = GT
 +
 +
newtype Sum a = Sum { getSum :: a }
 +
 +
instance Monoid (Sum Nat) where
 +
mempty   = Sum natZero
 +
mappend (Sum a) (Sum b) = Sum $ a +. b
 +
 +
newtype Product a = Product { getProduct :: a }
 +
 +
instance Monoid (Product Nat) where
 +
mempty   = Product natOne
 +
mappend (Product a) (Product b) = Product $ a *. b
 +
 +
instance Monoid (Sum Int) where
 +
mempty   = Sum intZero
 +
mappend (Sum a) (Sum b) = Sum $ a .+. b
 +
 +
instance Group (Sum Int) where
 +
ginv = Sum . intNeg . getSum
 +
 +
instance Monoid (Product Int) where
 +
mempty   = Product intOne
 +
mappend (Product a) (Product b) = Product $ a .*. b
 +
 +
instance Monoid (Sum Rat) where
 +
mempty   = Sum ratZero
 +
mappend (Sum a) (Sum b) = Sum $ a %+ b
 +
 +
instance Group (Sum Rat) where
 +
ginv = Sum . ratNeg . getSum
 +
 +
instance Monoid (Product Rat) where
 +
mempty   = Product ratOne
 +
mappend (Product a) (Product b) = Product $ a %* b
 +
 +
instance Group (Product Rat) where
 +
ginv = Product . ratInv . getProduct
 +
 +
instance Monoid (List a) where
 +
mempty = Nil
 +
mappend = (++)
 +
 +
==Categories==
 +
 +
class Category cat where
 +
id  :: cat a a
 +
(.) :: cat b c -> cat a b -> cat a c
 +
 +
class Functor f where
 +
fmap :: (a -> b) -> f a -> f b
 +
 +
class Monad m where
 +
(>>=) :: m a -> (a -> m b) -> m b
 +
return :: a -> m a
 +
 +
class (Functor f) => Applicative f where
 +
pure :: a -> f a
 +
(<*>) :: f (a -> b) -> f a -> f b
 +
 +
class Functor m => MonadJoin m where
 +
returnJoin :: a -> m a
 +
join :: m (m a) -> m a
 +
 +
data Identity a = Identity a
 +
runIdentity a = a
 +
 +
instance Monad Identity where
 +
return x = Identity x
 +
(Identity x) >>= f = f x
 +
 +
data Maybe a = Just a | Nothing
 +
 +
instance Monad Maybe where
 +
Nothing  >>= f  =  Nothing
 +
(Just x) >>= f  =  f x
 +
return x = Just x
 +
 +
instance Monad [] where
 +
  m >>= f  = concat (map f m)
 +
  return x = [x]
 +
 +
class MonadFish m where
 +
returnFish :: a -> m a
 +
(>=>) :: (a -> m b) -> (b -> m c) -> (a -> m c)
 +
 +
data State s r = State (s -> (r, s))
 +
 +
runState (State f) s = f s
 +
 +
instance Monad (State s) where
 +
return r = State (\s -> (r, s))
 +
(State x) >>= f = State h
 +
where
 +
h s0 =
 +
let
 +
(r1, s1) = x s0
 +
State g = f r1
 +
(r2, s2) = g s1
 +
in
 +
(r2, s2)
 +
 +
newtype IdentityCPS a = IdentityCPS {runIdentityCPS :: forall r . (a -> r) -> r}
 +
 +
caseIdentityCPS :: IdentityCPS a -> (a -> r) -> r
 +
caseIdentityCPS = \x -> \f -> runIdentityCPS x f
 +
 +
constrIdentityCPS :: a -> IdentityCPS a
 +
constrIdentityCPS = \a -> IdentityCPS $ \f -> f a
 +
 +
instance Functor IdentityCPS where
 +
fmap f ma = IdentityCPS $ \g -> caseIdentityCPS ma (\a -> g (f a))
 +
 +
instance Applicative IdentityCPS where
 +
pure = constrIdentityCPS
 +
mf <*> ma = IdentityCPS $ \g -> caseIdentityCPS ma (\a -> caseIdentityCPS mf (\f -> g (f a )))
 +
 +
instance Monad IdentityCPS where
 +
return = constrIdentityCPS
 +
ma >>= f = IdentityCPS $ \g -> caseIdentityCPS ma (\a -> runIdentityCPS (f a) g)
 +
 +
newtype MaybeCPS r a = MaybeCPS {runMaybeCPS :: (a -> r) -> r -> r}
 +
 +
caseMaybeCPS :: MaybeCPS r a -> (a -> r) -> r -> r
 +
caseMaybeCPS = \x -> \f -> \g -> runMaybeCPS x f g
 +
 +
justCPS :: a -> MaybeCPS r a
 +
justCPS a = MaybeCPS $ \f -> \g -> f a
 +
nothing :: MaybeCPS r a
 +
nothing = MaybeCPS $ \f -> \g -> g
 +
 +
instance Functor (MaybeCPS r) where
 +
fmap f ma = MaybeCPS $ \g -> \h -> caseMaybeCPS ma (\a -> g (f a)) h
 +
 +
instance Applicative (MaybeCPS r) where
 +
pure = justCPS
 +
mf <*> ma = MaybeCPS $ \g -> \h -> caseMaybeCPS ma (\a -> caseMaybeCPS mf (\f -> g $ f a) h) h
 +
 +
instance Monad (MaybeCPS r) where
 +
return = justCPS
 +
ma >>= f = MaybeCPS $ \g -> \h -> caseMaybeCPS ma (\a -> runMaybeCPS (f a) g h) h
 +
 +
newtype StateCPS s a = StateCPS {runStateCPS :: forall r . s -> (s -> a -> r) -> r}
 +
 +
caseStateCPS :: (StateCPS s a) -> ((s -> (s, a)) -> r) -> r
 +
caseStateCPS = \x -> \f -> f $ \s -> runStateCPS x s (\s -> \a -> (s, a))
 +
 +
state' :: (s -> (s, a)) -> StateCPS s a
 +
state' st = StateCPS $ \s -> \f -> let (s', a) = st s in f s' a
 +
 +
instance Functor (StateCPS s) where
 +
fmap f sa = StateCPS $ \s -> \g -> caseStateCPS sa (\st -> let (s', a) = st s in g s' (f a))
 +
 +
instance Applicative (StateCPS s) where
 +
pure a = state' $ \s -> (s, a)
 +
sf <*> sa = StateCPS $ \s -> \g -> caseStateCPS sf (\stf -> let (s', f) = stf s in caseStateCPS sa (\sta -> let (s'', a) = sta s' in g s'' (f a)))
 +
 +
instance Monad (StateCPS s) where
 +
return a = state' $ \s -> (s, a)
 +
sa >>= f = StateCPS $ \s -> \g -> caseStateCPS sa (\sta -> let (s', a) = sta s in runStateCPS (f a) s' g)
 +
 
=Кр4=
 
=Кр4=
 +
== deforestation ==
 +
Дана функция, необходимо её упростить, пользуясь техникой ''deforestation''.
 +
 +
'''Мотивация:''' допустим, есть какая-то функция следующего вида:
 +
 +
<code>
 +
  foldl 0 (*) . filter (> 0) . map (\ x -> 3 * x - 10)
 +
</code>
 +
 +
Первый map создаёт новый список, потом filter возвращает ещё список, и так далее. Если функций много (а их вполне может быть сколько угодно), то такой подход перестаёт быть эффективным. Идея в том, чтобы написать функцию, которая делает все необходимые действия "за раз": в данном примере можно рассматривать элемент списка, применять к нему функцию, потом проверять на условие в filter, а потом сразу считать произведение. Иногда можно посмотреть на композицию функций и придумать сразу оптимальный вариант. Это и требуется сделать во втором задании. Но можно и не думать, а применить стандартный алгоритм для преобразования, который даёт ответ.
 +
 +
[http://www.sciencedirect.com/science/article/pii/030439759090147A По этой ссылке] описаны правила, по которым нужно преобразовывать функцию. Если коротко, то всё сводится к inline'у тел функций, причём мы хотим добиться отсутствия вызовов других функций на месте аргументов внешней функции (рекомендуется для начала почитать ссылку, посмотреть правила и пример оттуда).
 +
 +
=== Пример ===
 +
Будет разобран пример из [https://pp.vk.me/c622121/v622121192/ff98/NtvrRei7bR4.jpg фото].
 +
 +
<code>
 +
<font color=green>-- дано</font>
 +
func = foldr (+) 0 . map (\x -> x * 10)
 +
 +
<font color=green>-- сначала перепишем композицию в обычную аппликацию для дальнейшей ясности</font>
 +
func0 l = foldr (+) 0 (map (\x -> x * 10) l)
 +
 +
<font color=green>-- теперь инлайним foldr, то есть раскрываем его тело</font>
 +
func1 l = '''case''' (map (\x -> x * 10) l) '''of'''
 +
                [] -> 0
 +
                (x:xs) -> x + (foldr (+) 0 xs)             
 +
         
 +
<font color=green>-- а теперь инлайним map, заодно раскроем лямбду</font>
 +
func2 l = '''case''' ('''case''' l '''of'''
 +
                      [] -> []
 +
                      (y:ys) -> y * 10 : map (*10) ys) '''of'''
 +
                [] -> 0
 +
                (x:xs) -> x + (foldr (+) 0 xs)
 +
               
 +
<font color=green>-- применяем преобразование case'a case'ов, то есть выносим внутренний case на первое место</font>
 +
func3 l = '''case''' l '''of'''
 +
                [] -> ('''case''' [] '''of'''
 +
                            [] -> 0
 +
                            (x:xs) -> x + (foldr (+) 0 xs))
 +
                (y:ys) -> ('''case''' (y * 10 : map (*10) ys) '''of'''
 +
                                [] -> 0
 +
                                (x:xs) -> x + (foldr (+) 0 xs))
 +
                               
 +
<font color=green>-- раскрываем внутренние case'ы: в них pattern-matching сразу срабатывает</font>
 +
func4 l = '''case''' l '''of'''
 +
                [] -> 0
 +
                (y:ys) -> 10 * y + (foldr (+) 0 (map (*10) ys))
 +
               
 +
<font color=green>-- замечаем, что у нас получилось в конце выражение foldr (+) 0 (map (*10) ys), а это по сути наша функция func0,
 +
которую мы раскрывали изначально, поэтому тому куску можно дать другое имя</font>
 +
func5 l = '''case''' l '''of'''
 +
                [] -> 0
 +
                (y:ys) -> 10 * y + func5 ys
 +
</code>
 +
 +
== stream fusion ==
 +
 +
По сути это то же самое, только вводятся два дополнительных типа, а стандартные функции подстраиваются под них.
 +
* [http://code.haskell.org/~dons/papers/icfp088-coutts.pdf Статья]
 +
* [http://www2.tcs.ifi.lmu.de/~senjak/haskellbeatsc.pdf Презентация с красивым форматированием (мотивация)]
 +
* [http://www.mit.edu/~mtikekar/posts/stream-fusion.html Применение в реальной жизни]
 +
* [http://sprunge.us/ZONH Разбор задания с кр]
 +
 +
== zippers and functions differentiation ==
 +
 +
Для каждой структуры данных (datatype'а) в Haskell можно составить соответствующий ей zipper: это другая структура данных, которая позволяет "гулять" по нашей структуре, взяв в фокус текущий элемент и запоминая при этом остальное состояние структуры данных (или контекст). Для списка легко придумывается zipper: мы находимся на какой-то позиции в списке, знаем значение элемента на этой позиции, знаем часть списка слева от текущего элемента и справа (для более глубокого понимания читай LearnYourHaskell). Поэтому zipper для списка имеет следующий вид:
 +
 +
<code>
 +
'''data''' ZipperList a = ZList a [a] [a]
 +
</code>
 +
 +
Но не для всех типов получается легко придумать zipper методом пристального взгляда. Чтобы составить zipper для произвольного типа без особых усилий, можно представить тип как функцию от параметра типа, а затем найти производную этого типа. Тогда если типу соответствует функция <tex> f(a) </tex>, то zipper выражается следующим образом: <tex> z(a) = a \cdot f'(a) </tex>.
 +
 +
Рассмотрим внимательней типа List:
 +
<code>
 +
'''data''' List a = Nil | Cons a (List a)
 +
</code>
 +
 +
Ему соотвествует следующее уравнение в функциях типов: <tex> f(a) = 1 + a \cdot f(a) </tex>. Если теперь продифференцировать обе части уравнения, то можно будет найти производную для списка. Обозначим список элементов типа <tex> x </tex> как <tex>L(x)</tex>. Из формулы для списка легко выражется, что <tex> L(x) = \dfrac{1}{1 - x} </tex>. Этим равенством будем пользоваться в дальнейшем.
 +
 +
=== Пример ===
 +
Найдём теперь zipper для какого-нибудь конкретного класса:
 +
<code>
 +
'''data''' Mice a = Haystack a (Mice a) a | Baboon (Mice a) | List' a a a
 +
</code>
 +
 +
Запишем уравнение типа для него: <tex> f(a) = a \cdot f(a) \cdot a + f(a) + a \cdot a \cdot a \ (1)</tex>.
 +
 +
На самом деле порядок аргументов в типе не очень важен, мы сами его задаём, поэтому можно написать чуть более сокращенную запись:
 +
 +
<tex> f(a) = a^2 \cdot f(a) + f(a) + a^3 </tex>
 +
 +
Забудем на некоторое время, что мы работаем с типами. Продифференцируем обе части уравнение по переменной <tex> a </tex>, получим линейное уравнение относительно производной.
 +
 +
<tex> f'(a) = 2a \cdot f(a) + a^2 \cdot f'(a) + f'(a) + 3a^2 </tex>
 +
 +
Заметка: на этом надо остановиться и написать соответствующий рекурсивный тип. За дальнейшие действия будет сняты 0.5 баллов(ЯН: "слишком сложное решение")
 +
 +
<code>
 +
<font color=green>-- Итого ответ:</font>
 +
'''data''' DMice a = S a (Mice a) | H a (Mice a) | M a a (DMice a) | Y (DMice a) | A a a | K a a | Shmyak a a
 +
</code>
 +
 +
Забавное, но бесполезное для сдачи ФП, продолжение:
 +
 +
Выразим производную.
 +
 +
<tex> f'(a) = \dfrac{2a \cdot f(a) + 3a^2}{1 - (a^2 + 1)}  = (2a \cdot f(a) + 3a^2) \cdot \dfrac{1}{1 - (a^2 + 1)} \ (2)</tex>
 +
 +
В итоге у нас производная является произведением двух функций, а для типа это значит, что он является произведением двух типов. При умножении на константу у нас будет просто несколько одинаковых конструкторов с разными именами.
 +
<code>
 +
<font color=green>--сначала распишем производную типа, полученного сразу после дифференцирования (1), если соблюдать исходный порядок аргументов в типах</font>
 +
'''data''' DMice a = S (Mice a) a | H a (DMice a) a | M a (Mice a) | Y (DMice a) | A a a | K a a | Shmyak a a
 +
</code>
 +
 +
Теперь распишем первую скобку в (2):
 +
<code>
 +
  '''data''' DMice' = M1 a (Mice a) | M2 a (Mice a) | C1 a a | C2 a a | C3 a a
 +
</code>
 +
 +
Дальше идёт дробь. Вспоминаем, что на самом деле ей отвечает тип <tex> L(a^2 + 1) </tex>.
 +
Поэтому получаем в итоге:
 +
<code>
 +
'''data''' DMiceListElem a = DM1 a a | DM0
 +
'''data''' DMiceList a = MNil | MCons (DMiceListElem a) (DMiceList a)
 +
'''data''' ZMice a = ZMice a (DMice' a) (DMiceList a)
 +
</code>
 +
 +
* [http://learnyouahaskell.com/zippers LearnYourHaskell {{---}} Zippers]
 +
* [http://sprunge.us/HCDN Пример zipper'a из кр]

Текущая версия на 19:05, 4 сентября 2022

Содержание

Кр1

Убрать все сокращения и расставить все скобки

(λ a b . (λ c d e . e) a) (x y) y (λ f . x) y

Решение

Скобки ставятся по следующим правилам:

  • тело абстракции заключается в скобки: λ x . M [math] \Rightarrow [/math] λ x . (M)
  • аппликация левоассоциативна: a b c d [math] \Rightarrow [/math] ((a b) c) d
  • сокращения раскрываются во вложенные лямбды (сразу с расставлением скобок): λ a b c . M [math] \Rightarrow [/math] λ a . (λ b . (λ c . (M)))

Важно: тело абстракции забирает всё до конца той скобки, в которую заключена.

Итого: ((((λ a . (λ b . ((λ c . (λ d . (λ e . (e)))) a))) (x y)) y) (λ f . (x))) y

Привести в нормальную форму

λ a b . a (λ c . b c) a (λ d . d) a
λ a . (λ b . y) (λ c . y (y (λ d . a a a)) (x x) a)

Решение

В нормальной форме нет редукций. Если нормальная форма существует, то её можно достичь при помощи редукций нормальным порядком, а аппликативным можно и не достичь.

  1. Уже в нормальное форме, как ни странно
  2. λ a . y

Нормальный порядок редукции

(λ a . y (y (y (λ b . a))) y) (x (x (x (λ c d . d) y)) x)

Здесь про стратегии редуцирования с примерами и определениями.

Нормальный порядок редуцирования — сначала раскрывается самый левый самый внешний редекс. Пример не очень удачный, так в нём всего одна редукция, после которой получится: y (y (y (λ b . (x (x (x (λ c d . d) y)) x)))) y

Более показательные и содержательные примеры (во всех случаях одна редукция будет произведена):

  • (λ a . a) ((λ x . x) y) [math] \Rightarrow [/math] (λ x . x) y
  • x (λ a . ((λ x . x) y) ((λ z . z) y)) [math] \Rightarrow [/math] x (λ a . y ((λ z . z) y))

Аппликативный порядок редукции

Здесь ещё про стратегии редуцирования, но немного другим языком (может быть, кому-то более понятным).

Аппликативный порядок редуцирования — первым делом редуцируем самый левый самый глубокий терм. То есть сначала упрощаем "аргументы" аппликации.

Те же примеры (во всех случаях одна редукция будет произведена):

  • (λ a . a) ((λ x . x) y) [math] \Rightarrow [/math] (λ a . a) y
  • x (λ a . ((λ x . x) y) ((λ z . z) y)) [math] \Rightarrow [/math] x (λ a . ((λ x . x) y) y)

Ещё один для разнообразия: ((λ x . y) (λ z . t)) ((λ a b c . a b c ((λ s . t) y) (λ t . x) u) (λ x . x)) ((λ x . x x) z) [math] \Rightarrow [/math] ((λ x . y) (λ z . t)) ((λ a b c . a b c ((λ s . t) y) (λ t . x) u) (λ x . x)) (z z)

Ленивый порядок редукции

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

То есть пример:

(λ f . f f) ((λ x . x) z)

Сначала делаем обычную редукцию нормальным порядком и получаем:

((λ x . x) z) ((λ x . x) z)

А потом после редукции нормальным порядком надо сделать изменения сразу в двух термах, потому что они якобы в коробках, и получим суммарно за 2 редукции:

z z

Выписать систему уравнений типизации

(λ a . a a) (λ b c . c)

Решение

Сначала надо дать типы всем термам и подтермам, раздавая каждый раз новые буквы новым переменным и термам. А потом связать эти буквы по следующим правилам:

  • если у нас абстракция (λ x . M) :: T0, x :: T1, M :: T2, то добавляем в систему T0 = T1 -> T2,
  • если имеем аппликацию (M N) :: T0, M :: T1, N :: T2, то добавляем T1 = T2 -> T0
  • если у нас переменная в теле абстракции встречается несколько раз и мы раздаём каждый раз ей новые буквы, то надо будет потом приравнять типы в аргументе абстракции и внутри её тела.

Итого:

(λ a . a a) (λ b c . c) :: A

(λ a . a a) :: B, (λ b c . c) :: C

a :: D, (a a) :: E

первая и вторая буквы "a" в E — a :: F, a :: G

Можем сразу расписать часть системы уравнений:

B = C -> A

B = D -> E

F = G -> E

D = F

D = G

Теперь расписываем терм с типом C (раскрыв сокращения для начала): (λ b . (λ c . c)) :: С

b :: H, (λ c . c) :: I

c :: J, c :: K

И добавляем уравнения:

C = H -> I

I = J -> K

J = K

Кодирование по Чёрчу

Выписать кайнды конструкторов типов, выписать типы конструкторов, закодировать по Чёрчу:

data Policeman a = Doctor a | Mice
data Tree a b c = Frog c | Pip (Tree a b c)

Этого задания не было в первой кр, поэтому оно будет расписано во второй. Вместо него была система уравнений типов чуть более адовая, чем в прошлом примере.

Кр2

Фотки

Разбор будет по фоткам 3, 4, 5 (остальные задания аналогичны):

N1. Порядок редуцирования

См. прошлую кр

E0. Определить примитивные конструкции

pair = \ x y p . p x y
fst  = \ r . r (\ x y . x)
snd  = \ r . r (\ x y . y)
fix  = \ f . (\ x . f (x x)) (\ x . f (x x))

Легко проверить, что fst (pair a b) = a, подставив и сделав редукции.

E1. Превратить let-биндинги в один большой лямбда-терм.

Конструкция

let x = z in y

превращается в

(\x . y) z

А пример просто превратится в

(\foo. [main]) [foo]

где [foo] — тело foo, [main] — тело main.

E2. let-биндинги, но с возможной взаимной рекурсией

foo = foo ((\ a . bar) foo)

bar = (\ a . y) y (\ b . y)

main = (\ a . foo (a z) (y y)) y

Решение

Осторожно! Магия

Расписывать формальный алгоритм довольно нудно и неприятно, поэтому здесь объяснение того, что происходит, а на примере должно быть понятно.

Сначала по каждому терму из условия надо составить терм с таким же именем, только штрихованный. В нём мы будем использовать первые буквы остальных термов. Фиксируем порядок аргументов, например для foo' это будет f b m. Тогда у всех остальных термов будет циклический порядок. То есть для bar' будет b m f, а для main' — m f b.

Теперь пишем foo'. Сначала используем fix. Потом абстракцию, аргументами которой является нужный набор из циклических перестановок (см. соответствие выше), а телом абстракции является тело foo с изменениями. Если встречается имя терма из задания, то надо его заменить на нужный циклический порядок. И если имена первых букв по каким-то причинам не подходят (коллизятся со связанными переменными), то надо более удачные имена этим переменным придумать.

Итого, после преобразований:

foo'  = fix (\ f b m . f b m ((\ a . b m f) (f b m)))
bar'  = fix (\ b m f . (\ a . y) y (\ b . y))
main' = fix (\ m f b . (\ a . f b m (a z) (y y)) y)

Результирующий терм выглядит как вызов штрихованной функции в нужной циклической перестановке:

main = main' foo' bar'

Но так как в этом задании дополнительные термы использовать нельзя, то main', foo', bar' надо проинлайнить в main.

N2. Раскрыть, как в E1 и нормализовать

В общем, в задании всё сказано. Надо превратить в один большой терм как в E1, а затем нормализовать, как в задании из первой кр.

S1. Расписать систему уравнений типов

Как в первой кр.

TP1. Убрать сокращения и расставить скобки

Именно это и требуется сделать. Разве что там вместо тела абстракции расписан её тип. А (->) в типе в отличие от аппликации правоассоциативна, то есть в

a -> b -> c

скобки ставятся следующим образом:

a -> (b -> c)

Итого:

  • дано: (\ a b . b -> b -> a) x
  • получается: (\ a . (\ b . b -> (b -> a))) x // вроде бы тут как раз весь тип внутри не надо заключать в скобки

TF1. Составить терм по типу

Тут надо пользоваться логикой. Вроде бы во всех примерах можно решить методом пристального взгляда. Мотивация: чтобы решение системы уравнений типов совпадало с полученным типом. Но в некоторых случаях довольно трудно (или даже невозможно) придумать терм по типу, например здесь не придумывается:

(a -> b) -> b -> a

Решение

Дано: forall a b c . (b -> c -> a) -> (c -> b) -> c -> a

Ответ: \f g c . f (g c) c

A1. Закодировать типы по Чёрчу (без взаимной рекурсии)

 data Doctor a = Minute a | Maybe a a a
 data Hour a b = Hour (Hour b b) (Doctor a) (Doctor b) | Roll b (Doctor a)

Решение

У каждого типа есть [math] N \geqslant 1[/math] конструктов, а у каждого конструктора есть [math] K \geqslant 0 [/math] аргументов.

Фиксируем тип с [math] N [/math] конструкторами. Каждый конструктор [math] C_i [/math] этого типа превращается в абстракцию, в которой сначала идут [math] K_i [/math] переменных — аргументы конструктора, а потом [math] N [/math] переменных, отвечающих конструкторам. В теле просто выбирается нужный конструктор и применяется ко всем аргументам.

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

 -- сначала Doctor 
 Minute = \ a . \ x y . x a
 Maybe  = \ a b c . \ x y . y a b c
 caseDoctor = \ p . \ x y . p x y
 -- теперь Hour 
 Hour = \ a b c . \ x y . x a b c
 Roll = \ a b . \ x y . y a b
 caseHour = \ p . \ x y . p x y

Интересное наблюдение: переменная p в case является как раз нужным конструктором, в котором уже подставлены все аргументы этого конструктора.

A2. Закодировать типы через [math] \mu [/math] - комбинатор

data Return a b = List (Return b a) (Return b a) b | Roll (Return a a) (Return a a) (Mice a)
data Mice a = Bucket (Mice a) (Return a a) | Haystack (Mice a) a

Решение

Магия как в E2!

Опять делаем соотвествие между TypeName и TypeName'. Чтобы написать TypeName', необходимо преобразовать объявление дататипов по следующим правилам:

  • сначала идёт mu (это как fix, только для типов),
  • потом какая-нибудь уникальная буква для типа (например x для Return и y для Mice),
  • после точки абстракция, которая сначала принимает в качестве аргумента другую уникальную букву, а затем аргументами параметры типа,
  • T1 | T2 заменяется на T1 + T2,
  • T1 T2 заменяется на T1 [math] \times [/math] T2,
  • параметры типа оставляем как есть,
  • если в конструкторе идёт наш тип, то пишем нашу уникальную букву, а затем уникальную букву другого типа, а если другой типа — наоборот; после чего параметры конструктора,
  • если тип не наш и не буковка параметр датайпа, и не принимает параметров (например Nothing), то пишем 1 вместо неё.
Return' = mu x . \ y . \ a b . (x y b a) [math] \times [/math] (x y b a) [math] \times [/math] b + (x y a a) [math] \times [/math] (x y a a) [math] \times [/math] (y x a)
Mice'   = mu y . \ x . \ a . (y x a) [math] \times [/math] (x y a a) + (y x a) [math] \times [/math] a

После этого пишем ответ:

Return = Return' Mice'
Mice   = Mice' Return'

H1. Написать Haskell-код какой-нибудь структуру данных

  • Квадродерево: ссылка на pastebin
    не совсем то, что требует Ян, но я пока не распарсил то, что он требует; возможно, более правильная версия появится позже

Кр3

ITMOPrelude

  1. gromakovsky
  2. yakupov
  3. itanf

Primitive

Nat

data Nat
(+.)
(-.)
(*.)
divides :: Nat -> Nat -> Bool

Rat

data Rat
(%+)
(%-)
(%*)
(%/)
euler :: ?

List

Угадайка

Дают тип, надо написать название функции из List.hs и реализовать её.

Комбинаторика

Тут можно использовать только набор заранее определённых функций листа( среди которых нет даже ++ )

subsequences :: [a] -> [ [ a ] ]
permutations :: [a] -> [ [ a ] ]

Algebra

class Monoid a where
	mempty :: a
	mappend :: a -> a -> a

class Monoid a => Group a where
	ginv :: a -> a

mconcat :: (Monoid a) => List a -> a
mconcat = foldr mappend mempty

instance Monoid Unit where
	mempty	  = Unit
	mappend _ _ = Unit

instance Group Unit where
	ginv _ = Unit

instance (Monoid a, Monoid b) => Monoid (Pair a b) where
	mempty	  = Pair mempty mempty
	mappend a b = Pair {fst = fst a `mappend` fst b,
						snd = snd b `mappend` snd b}

instance (Monoid a) => Monoid (Maybe a) where
	mempty					= Just mempty
	mappend (Just a) (Just b) = Just $ mappend a b
	mappend _ _			   = Nothing

newtype First a = First { getFirst :: Maybe a}

instance Monoid (First a) where
	mempty					= First Nothing
	mappend (First Nothing) x = x
	mappend x _			   = x

newtype Last a = Last { getLast :: Maybe a}

instance Monoid (Last a) where
	mempty				   = Last Nothing
	mappend x (Last Nothing) = x
	mappend _ x			  = x

newtype Any = Any { getAny :: Bool }

instance Monoid Any where
	mempty				  = Any False
	mappend (Any a) (Any b) = Any $ a || b

newtype All = All { getAll :: Bool }

instance Monoid All where
	mempty				  = All True
	mappend (All a) (All b) = All $ a && b

-- Лексикографическое сравнение
instance Monoid Tri where
	mempty	   = EQ
	mappend LT _ = LT
	mappend EQ a = a
	mappend GT _ = GT

newtype Sum a = Sum { getSum :: a }

instance Monoid (Sum Nat) where
	mempty				  = Sum natZero
	mappend (Sum a) (Sum b) = Sum $ a +. b

newtype Product a = Product { getProduct :: a }

instance Monoid (Product Nat) where
	mempty						  = Product natOne
	mappend (Product a) (Product b) = Product $ a *. b

instance Monoid (Sum Int) where
	mempty				  = Sum intZero
	mappend (Sum a) (Sum b) = Sum $ a .+. b

instance Group (Sum Int) where
	ginv = Sum . intNeg . getSum

instance Monoid (Product Int) where
	mempty						  = Product intOne
	mappend (Product a) (Product b) = Product $ a .*. b

instance Monoid (Sum Rat) where
	mempty				  = Sum ratZero
	mappend (Sum a) (Sum b) = Sum $ a %+ b

instance Group (Sum Rat) where
	ginv = Sum . ratNeg . getSum

instance Monoid (Product Rat) where
	mempty						  = Product ratOne
	mappend (Product a) (Product b) = Product $ a %* b

instance Group (Product Rat) where
	ginv = Product . ratInv . getProduct

instance Monoid (List a) where
	mempty = Nil
	mappend = (++)

Categories

class Category cat where
	id  :: cat a a
	(.) :: cat b c -> cat a b -> cat a c

class Functor f where
	fmap :: (a -> b) -> f a -> f b

class Monad m where
	(>>=) :: m a -> (a -> m b) -> m b
	return :: a -> m a

class (Functor f) => Applicative f where
	pure :: a -> f a
	(<*>) :: f (a -> b) -> f a -> f b

class Functor m => MonadJoin m where
	returnJoin :: a -> m a
	join :: m (m a) -> m a

data Identity a = Identity a
runIdentity a = a

instance Monad Identity where
	return x = Identity x	
	(Identity x) >>= f = f x

data Maybe a = Just a | Nothing

instance Monad Maybe where
	Nothing  >>= f  =  Nothing
	(Just x) >>= f  =  f x
	return x = Just x

instance Monad [] where
  m >>= f  = concat (map f m)
  return x = [x]

class MonadFish m where
	returnFish :: a -> m a
	(>=>) :: (a -> m b) -> (b -> m c) -> (a -> m c)

data State s r = State (s -> (r, s))

runState (State f) s = f s

instance Monad (State s) where	
	return r = State (\s -> (r, s))		
	(State x) >>= f = State h
		where
		h s0 =
			let
				(r1, s1) = x s0
				State g = f r1
				(r2, s2) = g s1
			in
				(r2, s2)

newtype IdentityCPS a = IdentityCPS {runIdentityCPS :: forall r . (a -> r) -> r}

caseIdentityCPS :: IdentityCPS a -> (a -> r) -> r
caseIdentityCPS = \x -> \f -> runIdentityCPS x f

constrIdentityCPS :: a -> IdentityCPS a
constrIdentityCPS = \a -> IdentityCPS $ \f -> f a

instance Functor IdentityCPS where
	fmap f ma = IdentityCPS $ \g -> caseIdentityCPS ma (\a -> g (f a))

instance Applicative IdentityCPS where
	pure = constrIdentityCPS
	mf <*> ma = IdentityCPS $ \g -> caseIdentityCPS ma (\a -> caseIdentityCPS mf (\f -> g (f a )))

instance Monad IdentityCPS where
	return = constrIdentityCPS
	ma >>= f = IdentityCPS $ \g -> caseIdentityCPS ma (\a -> runIdentityCPS (f a) g)

newtype MaybeCPS r a = MaybeCPS {runMaybeCPS :: (a -> r) -> r -> r}

caseMaybeCPS :: MaybeCPS r a -> (a -> r) -> r -> r
caseMaybeCPS = \x -> \f -> \g -> runMaybeCPS x f g

justCPS :: a -> MaybeCPS r a
justCPS a = MaybeCPS $ \f -> \g -> f a
nothing :: MaybeCPS r a
nothing = MaybeCPS $ \f -> \g -> g

instance Functor (MaybeCPS r) where
	fmap f ma = MaybeCPS $ \g -> \h -> caseMaybeCPS ma (\a -> g (f a)) h

instance Applicative (MaybeCPS r) where
	pure = justCPS
	mf <*> ma = MaybeCPS $ \g -> \h -> caseMaybeCPS ma (\a -> caseMaybeCPS mf (\f -> g $ f a) h) h

instance Monad (MaybeCPS r) where
	return = justCPS
	ma >>= f = MaybeCPS $ \g -> \h -> caseMaybeCPS ma (\a -> runMaybeCPS (f a) g h) h

newtype StateCPS s a = StateCPS {runStateCPS :: forall r . s -> (s -> a -> r) -> r}

caseStateCPS :: (StateCPS s a) -> ((s -> (s, a)) -> r) -> r
caseStateCPS = \x -> \f -> f $ \s -> runStateCPS x s (\s -> \a -> (s, a))

state' :: (s -> (s, a)) -> StateCPS s a
state' st = StateCPS $ \s -> \f -> let (s', a) = st s in f s' a

instance Functor (StateCPS s) where
	fmap f sa = StateCPS $ \s -> \g -> caseStateCPS sa (\st -> let (s', a) = st s in g s' (f a))

instance Applicative (StateCPS s) where
	pure a = state' $ \s -> (s, a)
	sf <*> sa = StateCPS $ \s -> \g -> caseStateCPS sf (\stf -> let (s', f) = stf s in caseStateCPS sa (\sta -> let (s, a) = sta s' in g s (f a)))

instance Monad (StateCPS s) where
	return a = state' $ \s -> (s, a)
	sa >>= f = StateCPS $ \s -> \g -> caseStateCPS sa (\sta -> let (s', a) = sta s in runStateCPS (f a) s' g)

Кр4

deforestation

Дана функция, необходимо её упростить, пользуясь техникой deforestation.

Мотивация: допустим, есть какая-то функция следующего вида:

 foldl 0 (*) . filter (> 0) . map (\ x -> 3 * x - 10)

Первый map создаёт новый список, потом filter возвращает ещё список, и так далее. Если функций много (а их вполне может быть сколько угодно), то такой подход перестаёт быть эффективным. Идея в том, чтобы написать функцию, которая делает все необходимые действия "за раз": в данном примере можно рассматривать элемент списка, применять к нему функцию, потом проверять на условие в filter, а потом сразу считать произведение. Иногда можно посмотреть на композицию функций и придумать сразу оптимальный вариант. Это и требуется сделать во втором задании. Но можно и не думать, а применить стандартный алгоритм для преобразования, который даёт ответ.

По этой ссылке описаны правила, по которым нужно преобразовывать функцию. Если коротко, то всё сводится к inline'у тел функций, причём мы хотим добиться отсутствия вызовов других функций на месте аргументов внешней функции (рекомендуется для начала почитать ссылку, посмотреть правила и пример оттуда).

Пример

Будет разобран пример из фото.

-- дано
func = foldr (+) 0 . map (\x -> x * 10)

-- сначала перепишем композицию в обычную аппликацию для дальнейшей ясности
func0 l = foldr (+) 0 (map (\x -> x * 10) l)

-- теперь инлайним foldr, то есть раскрываем его тело
func1 l = case (map (\x -> x * 10) l) of
               [] -> 0
               (x:xs) -> x + (foldr (+) 0 xs)               
         
-- а теперь инлайним map, заодно раскроем лямбду
func2 l = case (case l of
                     [] -> []
                     (y:ys) -> y * 10 : map (*10) ys) of
               [] -> 0
               (x:xs) -> x + (foldr (+) 0 xs)
               
-- применяем преобразование case'a case'ов, то есть выносим внутренний case на первое место
func3 l = case l of
               [] -> (case [] of
                           [] -> 0
                           (x:xs) -> x + (foldr (+) 0 xs))
               (y:ys) -> (case (y * 10 : map (*10) ys) of
                               [] -> 0
                               (x:xs) -> x + (foldr (+) 0 xs))
                                
-- раскрываем внутренние case'ы: в них pattern-matching сразу срабатывает
func4 l = case l of
               [] -> 0
               (y:ys) -> 10 * y + (foldr (+) 0 (map (*10) ys))
                
-- замечаем, что у нас получилось в конце выражение foldr (+) 0 (map (*10) ys), а это по сути наша функция func0, 
которую мы раскрывали изначально, поэтому тому куску можно дать другое имя
func5 l = case l of
               [] -> 0
               (y:ys) -> 10 * y + func5 ys

stream fusion

По сути это то же самое, только вводятся два дополнительных типа, а стандартные функции подстраиваются под них.

zippers and functions differentiation

Для каждой структуры данных (datatype'а) в Haskell можно составить соответствующий ей zipper: это другая структура данных, которая позволяет "гулять" по нашей структуре, взяв в фокус текущий элемент и запоминая при этом остальное состояние структуры данных (или контекст). Для списка легко придумывается zipper: мы находимся на какой-то позиции в списке, знаем значение элемента на этой позиции, знаем часть списка слева от текущего элемента и справа (для более глубокого понимания читай LearnYourHaskell). Поэтому zipper для списка имеет следующий вид:

data ZipperList a = ZList a [a] [a]

Но не для всех типов получается легко придумать zipper методом пристального взгляда. Чтобы составить zipper для произвольного типа без особых усилий, можно представить тип как функцию от параметра типа, а затем найти производную этого типа. Тогда если типу соответствует функция [math] f(a) [/math], то zipper выражается следующим образом: [math] z(a) = a \cdot f'(a) [/math].

Рассмотрим внимательней типа List:

data List a = Nil | Cons a (List a)

Ему соотвествует следующее уравнение в функциях типов: [math] f(a) = 1 + a \cdot f(a) [/math]. Если теперь продифференцировать обе части уравнения, то можно будет найти производную для списка. Обозначим список элементов типа [math] x [/math] как [math]L(x)[/math]. Из формулы для списка легко выражется, что [math] L(x) = \dfrac{1}{1 - x} [/math]. Этим равенством будем пользоваться в дальнейшем.

Пример

Найдём теперь zipper для какого-нибудь конкретного класса:

data Mice a = Haystack a (Mice a) a | Baboon (Mice a) | List' a a a

Запишем уравнение типа для него: [math] f(a) = a \cdot f(a) \cdot a + f(a) + a \cdot a \cdot a \ (1)[/math].

На самом деле порядок аргументов в типе не очень важен, мы сами его задаём, поэтому можно написать чуть более сокращенную запись:

[math] f(a) = a^2 \cdot f(a) + f(a) + a^3 [/math]

Забудем на некоторое время, что мы работаем с типами. Продифференцируем обе части уравнение по переменной [math] a [/math], получим линейное уравнение относительно производной.

[math] f'(a) = 2a \cdot f(a) + a^2 \cdot f'(a) + f'(a) + 3a^2 [/math]

Заметка: на этом надо остановиться и написать соответствующий рекурсивный тип. За дальнейшие действия будет сняты 0.5 баллов(ЯН: "слишком сложное решение")

-- Итого ответ:
data DMice a = S a (Mice a) | H a (Mice a) | M a a (DMice a) | Y (DMice a) | A a a | K a a | Shmyak a a

Забавное, но бесполезное для сдачи ФП, продолжение:

Выразим производную.

[math] f'(a) = \dfrac{2a \cdot f(a) + 3a^2}{1 - (a^2 + 1)} = (2a \cdot f(a) + 3a^2) \cdot \dfrac{1}{1 - (a^2 + 1)} \ (2)[/math]

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

--сначала распишем производную типа, полученного сразу после дифференцирования (1), если соблюдать исходный порядок аргументов в типах
data DMice a = S (Mice a) a | H a (DMice a) a | M a (Mice a) | Y (DMice a) | A a a | K a a | Shmyak a a

Теперь распишем первую скобку в (2):

 data DMice' = M1 a (Mice a) | M2 a (Mice a) | C1 a a | C2 a a | C3 a a

Дальше идёт дробь. Вспоминаем, что на самом деле ей отвечает тип [math] L(a^2 + 1) [/math]. Поэтому получаем в итоге:

data DMiceListElem a = DM1 a a | DM0
data DMiceList a = MNil | MCons (DMiceListElem a) (DMiceList a)
data ZMice a = ZMice a (DMice' a) (DMiceList a)