3622
правки
Изменения
→A2. Закодировать типы по Чёрчу (с взаимной рекурсией)
== A2. Закодировать типы по Чёрчу (с взаимной рекурсией) ==
'''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-код какой-нибудь структуру данных ==
