3622
правки
Изменения
м
)После этого пишем ответ: Return = Return' Mice' Mice = Mice' Return'
* [[АВЛ-дерево]]: [http://pastie.org/private/qbiu60aetjm9zrpqzrow ссылка на pastie]*: почему я не знал Haskell, когда это дерево было в лабе по дискретке на первом курсе? ;( просто списывается с конспекта один в один...* [[Квадродеревья | Квадродерево]]: [http://pastiepastebin.org/privatecom/sf1vdmrpe7ifvqgdongwq jV4DeRvv ссылка на pastiepastebin]
→H1. Написать Haskell-код какой-нибудь структуру данных
* аппликация левоассоциативна: 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 . (λ d . (λ e . (e)))) a))) (x y)) y) (λ f . (x))) y
=== Решение ===
В нормальной форме нет редукций. Если нормальная форма существует, то её можно достичь при помощи редукций [[#Нормальный порядок редукции|нормальным порядком]], а [[#Аппликативный порядок редукции|аппликативным ]] можно и не достичь.
# Уже в нормальное форме, как ни странно
[http://pv.bstu.ru/flp/fpLectures.pdf Здесь] ещё про стратегии редуцирования, но немного другим языком (может быть, кому-то более понятным).
'''Аппликативный порядок редуцирования''' {{---}} первым делом редуцируем самый правый левый самый глубокий терм. То есть сначала упрощаем "аргументы" аппликации.
Те же примеры (во всех случаях одна редукция будет произведена):
((λ 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)
== Ленивый порядок редукции ==
'''Ленивый порядок редуцирования''' {{---}} это когда мы якобы заворачиваем терм в коробку, и если делаем редукцию в одном из термов коробки, то она делается во всех. При этом сам порядок редуцирования нормальный.
То есть пример:
(λ f . f f) ((λ x . x) z)
Сначала делаем обычную редукцию нормальным порядком и получаем:
((λ x . x) z) ((λ x . x) z)
А потом после редукции нормальным порядком надо сделать изменения сразу в двух термах, потому что они якобы в коробках, и получим суммарно за 2 редукции:
z z
==Выписать систему уравнений типизации==
== 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 и нормализовать ==
Интересное наблюдение: переменная 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
== H1. Написать Haskell-код какой-нибудь структуру данных ==
*: не совсем то, что требует Ян, но я пока не распарсил то, что он требует; возможно, более правильная версия появится позже
=Кр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=
== 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 из кр]
