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

Материал из Викиконспекты
Перейти к: навигация, поиск
(permutations)
(Кр3)
Строка 299: Строка 299:
 
#* [https://github.com/itanf/ITMO-Training-FunctionalProgramming/blob/master/ITMOPrelude/Primitive.hs Primitive.hs]
 
#* [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]
 
#* [https://github.com/itanf/ITMO-Training-FunctionalProgramming/blob/master/ITMOPrelude/List.hs List.hs]
==Натуральные числа==
+
 
  data Nat = Zero | Succ Nat deriving (Show,Read) <font color=green>-- Определение натуральных чисел</font>
+
==Primitive==
natZero = Zero    <font color=green>-- 0</font>
+
===Nat===
  natOne = Succ Zero <font color=green>-- 1</font>
+
  data Nat
 +
(+.)
 +
(-.)
 +
(*.)
 +
 
 +
divides :: Nat -> Nat -> Bool
 +
 
 +
===Rat===
 +
data Rat
 +
(%+)
 +
(%-)
 +
(%*)
 +
(%/)
 +
 
 +
  euler :: ?
 +
 
 +
==List==
 +
 
 +
===Угадайка===
 +
Дают тип, надо написать название функции из '''List.hs''' и реализовать её.
 +
 
 +
===Комбинаторика===
 +
 
 +
'''Тут можно использовать только набор заранее определённых функций листа( среди которых нет даже ''++'' )'''
 +
 
 +
subsequences :: [a] -> [ [ a ] ]
 +
 
 +
permutations :: [a] -> [ [ a ] ]
 +
 
 +
==Algebra==
 +
class Monoid a
 
   
 
   
  natCmp :: Nat -> Nat -> Tri  <font color=green>-- Сравнивает два натуральных числа</font>
+
  instance Monoid Nat  
natCmp Zero Zero = EQ
+
 
natCmp Zero (Succ _) = LT
+
==Categories==
natCmp (Succ _) Zero = GT
 
natCmp (Succ n) (Succ m) = natCmp n m
 
 
natEq :: Nat -> Nat -> Bool  <font color=green>-- n совпадает с m</font>
 
natEq Zero    Zero    = True
 
natEq Zero    (Succ _) = False
 
natEq (Succ _) Zero    = False
 
natEq (Succ n) (Succ m) = natEq n m
 
 
natLt :: Nat -> Nat -> Bool  <font color=green>-- n меньше m</font>
 
natLt Zero    Zero    = False
 
natLt Zero    (Succ m) = True
 
natLt (Succ n) Zero    = False
 
natLt (Succ n) (Succ m) = natLt n m
 
 
infixl 6 +.  <font color=green>-- Сложение для натуральных чисел</font>
 
(+.) :: Nat -> Nat -> Nat
 
Zero    +. m = m
 
(Succ n) +. m = Succ (n +. m)
 
 
infixl 6 -. <font color=green>-- Вычитание для натуральных чисел</font>
 
(-.) :: Nat -> Nat -> Nat
 
Zero -. _ = Zero
 
n -. Zero = n
 
(Succ n) -. (Succ m) = n -. m
 
 
infixl 7 *. <font color=green>-- Умножение для натуральных чисел</font>
 
(*.) :: Nat -> Nat -> Nat
 
Zero    *. m = Zero
 
(Succ n) *. m = m +. (n *. m)
 
 
natDivMod :: Nat -> Nat -> Pair Nat Nat <font color=green>-- Целое и остаток от деления n на m</font>
 
natDivMod n m =
 
    if (n natLt m)
 
        then Pair Zero n
 
        else Pair (Succ div) mod where Pair div mod = ((n -. m) natDivMod m)
 
 
natDiv n = fst . natDivMod n <font color=green>-- Целое</font>
 
natMod n = snd . natDivMod n <font color=green>-- Остаток</font>
 
  
==Целые числа==
+
  class (Functor f) => Applicative f
  data Int = Plus Nat | Minus Nat deriving (Show,Read)
 
 
intZero  = Plus Zero
 
intOne    = Plus (Succ Zero)
 
intNegOne = Minus (Succ Zero)
 
 
intNeg :: Int -> Int
 
intNeg (Plus x) = Minus x
 
intNeg (Minus x) = Plus x
 
 
intCmp :: Int -> Int -> Tri
 
intCmp (Plus Zero) (Minus Zero) = EQ
 
intCmp (Minus Zero) (Plus Zero) = EQ
 
intCmp (Plus Zero) (Minus (Succ x)) = GT
 
intCmp (Minus Zero) (Plus (Succ x)) = LT
 
intCmp (Plus (Succ x)) (Minus Zero) = GT
 
intCmp (Minus (Succ x)) (Plus Zero) = LT
 
intCmp (Plus x) (Plus y) = natCmp x y
 
intCmp (Minus x) (Minus y) = natCmp y x
 
 
intEq :: Int -> Int -> Bool
 
intEq (Plus Zero) (Minus Zero) = True
 
intEq (Minus Zero) (Plus Zero) = True
 
intEq (Plus Zero) (Minus (Succ x)) = False
 
intEq (Minus Zero) (Plus (Succ x)) = False
 
intEq (Plus (Succ x)) (Minus Zero) = False
 
intEq (Minus (Succ x)) (Plus Zero) = False
 
intEq (Plus x) (Plus y) = natEq x y
 
intEq (Minus x) (Minus y) = natEq x y
 
 
   
 
   
  intLt :: Int -> Int -> Bool
+
  Monad Join m
intLt (Plus Zero) (Minus Zero) = False
 
intLt (Minus Zero) (Plus Zero) = False
 
intLt (Plus Zero) (Minus (Succ x)) = False
 
intLt (Minus Zero) (Plus (Succ x)) = True
 
intLt (Plus (Succ x)) (Minus Zero) = False
 
intLt (Minus (Succ x)) (Plus Zero) = True
 
intLt (Plus x) (Plus y) = natLt x y
 
intLt (Minus x) (Minus y) = natLt y x
 
 
   
 
   
  infixl 6 .+., .-.
+
  data Identity
(.+.) :: Int -> Int -> Int
 
(Plus m) .+. (Plus n) = Plus (m +. n)
 
(Minus m) .+. (Minus n) = Minus (m +. n)
 
(Plus (Succ m)) .+. (Minus (Succ n)) = (Plus m) .+. (Minus n)
 
(Minus (Succ m)) .+. (Plus (Succ n)) = (Plus n) .+. (Minus m)
 
x .+. (Plus Zero) = x
 
x .+. (Minus Zero) = x
 
(Plus Zero) .+. y = y
 
(Minus Zero) .+. y = y
 
 
   
 
   
  (.-.) :: Int -> Int -> Int
+
  instance Monad Identity
n .-. m = n .+. (intNeg m)
 
 
   
 
   
infixl 7 .*.
+
  data Maybe
(.*.) :: Int -> Int -> Int
 
(Plus m) .*. (Plus n) = Plus (m *. n)
 
(Minus m) .*. (Minus n) = Plus (m *. n)
 
(Plus m) .*. (Minus n) = Minus (m *. n)
 
(Minus m) .*. (Plus n) = Minus (m *. n)
 
 
 
==Рациональные числа==
 
  data Rat = Rat Int Nat
 
 
   
 
   
  ratNeg :: Rat -> Rat
+
  instance Monad Maybe
ratNeg (Rat x y) = Rat (intNeg x) y
 
 
   
 
   
  ratInv :: Rat -> Rat
+
  instance Monad []
ratInv (Rat (Plus x) y) = Rat (Plus y) x
 
ratInv (Rat (Minus x) y) = Rat (Minus y) x
 
 
   
 
   
  ratCmp :: Rat -> Rat -> Tri
+
  data State
ratCmp (Rat a b) (Rat c d) = intCmp (a .*. (Plus d)) (c .*. (Plus b))
 
 
   
 
   
  ratEq :: Rat -> Rat -> Bool
+
  instance Monad State
ratEq (Rat a b) (Rat c d) = intEq (a .*. (Plus d)) (c .*. (Plus b))
 
 
   
 
   
  ratLt :: Rat -> Rat -> Bool
+
  newtype CpsIdentity
ratLt (Rat a b) (Rat c d) = intEq (a .*. (Plus d)) (c .*. (Plus b))
 
 
   
 
   
  internalRatPlus :: Rat -> Rat -> Rat
+
  instance Monad CpsIdentity
internalRatPlus (Rat a b) (Rat c d) = Rat ((a .*. (Plus d)) .+. (c .*. (Plus b))) (b *. d)
 
 
   
 
   
  internalRatShorten :: Rat -> Rat
+
  newtype CpsMaybe
internalRatShorten (Rat (Plus a) b) = Rat (Plus (a /. (gcd a b))) (b /. (gcd a b))
 
internalRatShorten (Rat (Minus a) b) = Rat (Minus (a /. (gcd a b))) (b /. (gcd a b))
 
 
   
 
   
  infixl 7 %+, %-
+
  instance Monad CpsMaybe
(%+) :: Rat -> Rat -> Rat
 
n %+ m = internalRatShorten (internalRatPlus n m)
 
 
   
 
   
  (%-) :: Rat -> Rat -> Rat
+
  newtype CpsState
n %- m = n %+ (ratNeg m)
 
 
   
 
   
  infixl 7 %*, %/
+
  instance Monad CpsState
(%*) :: Rat -> Rat -> Rat
 
(Rat a b) %* (Rat c d) = Rat (a .*. c) (b *. d)
 
 
(%/) :: Rat -> Rat -> Rat
 
n %/ m = n %* (ratInv m)
 
 
 
==GCD==
 
 
 
'''Тут я не уверен, можем ли использовать ''natMod'' или надо дополнительно реализовывать её.<br/>Ещё мы вроде бы не можем использовать дополнительные функции!'''
 
 
 
gcd :: Nat -> Nat -> Nat
 
gcd n Zero = n
 
gcd n m = gcd m (natMod n m)
 
 
 
==Метод Ньютона==
 
==subsequences==
 
subsequences :: List a -> List (List a)
 
subsequences Nil = Cons Nil Nil
 
subsequences (Cons x xs) = subsequences xs ++ (map (Cons x) $ subsequences xs)
 
 
 
==permutations==
 
permutations :: List a -> List (List a)
 
permutations Nil = Cons Nil Nil
 
permutations (Cons x ab) = perm Nil x ab where
 
    perm left m Nil = map (Cons m) (permutations left)
 
    perm left m (Cons r rx) = (map (Cons m) $ permutations $ left ++ (Cons r rx)) ++ (perm (Cons m left) r rx)
 
 
 
==А так же==
 
* Дают тип какого-нибудь foldr и просят написать какой-нибудь foldr.
 
* Написать определения каких-нибудь тайпклассов.
 
* Написать какие-нибудь инстансы.
 
* Доказать эквивалетность каких-нибудь двух определений монады.
 
* CPS-преобразовать какие-нибудь типы.
 
* Написать монадные инстансы для CPS-преобразованных типов.
 
  
 
=Кр4=
 
=Кр4=

Версия 11:43, 28 апреля 2015

Содержание

Кр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
    почему я не знал 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 

instance Monoid Nat 

Categories

class (Functor f) => Applicative f 

Monad Join m

data Identity

instance Monad Identity 

data Maybe

instance Monad Maybe 

instance Monad []

data State 

instance Monad State

newtype CpsIdentity

instance Monad CpsIdentity

newtype CpsMaybe

instance Monad CpsMaybe

newtype CpsState

instance Monad CpsState

Кр4