Бананы, линзы, оригами и примкнувшая к ним сегодня натуральность fold

[deniok]

The Origami style is based around the idea that datatypes are fixpoints of shape functors.
(сегодняшний LtU)

Про всё заявленное в теме не напишу, а про это - напишу :)

Общеизвестное :)
Обычная рекурсия

fac n = if n == 0 
           then 1
           else n * fac (n-1)

может быть выражена через комбинатор неподвижной точки fix:

-- нерекурсивный хэлпер
fac' f n = if n == 0 
               then 1 
               else n * f (n-1)
-- рекурсия здесь
fac = fix fac'

Комбинатор неподвижной точки определен так:

fix f = f (fix f)

Аналог fix для типов
А теперь - от обыденного к прекрасному! ;) Можно написать аналог fix для типов:

data Rec f = In (f (Rec f))

где тип f должен быть, ясен пень, полиморфно параметризован (а для дальнейших вкусностей ещё и instance Functor).
Тип конструктора данных для типа Rec

In :: f (Rec f) -> Rec f

дает понять, что это - действительно fix уровня типов.

Теперь мы можем выразить все обычные рекурсивные типы как фиксированные точки функторов.


Пример 1
Рекурсивный тип данных натуральных чисел (классическая запись)

data Nat = Z | S Nat

Выразим его, как неподвижную точку функтора

-- функтор, описывающий структуру типа
data N c = Z | S c

instance Functor N where
  fmap g  Z    = Z
  fmap g (S x) = S (g x)

-- рекурсивный тип вводим через неподвижную точку функтора на уровне типов
type Nat = Rec N

Проверяем типы:

-- нерекурсивный функтор
Z       :: N c
S Z     :: N (N c)
S (S Z) :: N (N (N c))
-- тип Nat (то есть Rec N) как его неподвижная точка
In Z                   :: Rec N
In (S (In Z))          :: Rec N
In (S (In (S (In Z)))) :: Rec N

Пример 2
Рекурсивный тип данных арифметических выражений (классическая запись)

data Expr = Num Int | Add Expr Expr

Выразим его, как неподвижную точку функтора

-- функтор, описывающий структуру типа
data E e = Num Int | Add e e

instance Functor E where
 fmap g (Num n)    = Num n
 fmap g (Add e e') = Add (g e) (g e')

-- рекурсивный тип вводим через неподвижную точку функтора на уровне типов
type Expr = Rec E 

Проверяем типы:

-- нерекурсивный функтор
Num 3                             :: E e
Add (Num 3) (Num 5)               :: E (E e)
Add (Add (Num 3) (Num 5)) (Num 7) :: E (E (E e))
-- тип Expr (то есть Rec E) как его неподвижная точка
In (Num 3)                                                 :: Rec E
In (Add (In (Num 3)) (In (Num 5)))                         :: Rec E
In (Add (In (Add (In (Num 3)) (In (Num 5)))) (In (Num 7))) :: Rec E

Пример 3
Рекурсивный тип данных списка (классическая запись)

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

Выразим его, как неподвижную точку функтора

-- функтор, описывающий структуру типа
data L a l = Nil | Cons a l

instance Functor (L a) where
 fmap g Nil        = Nil
 fmap g (Cons a l) = Cons a (g l)

-- рекурсивный тип вводим через неподвижную точку функтора на уровне типов
type List a = Rec (L a) 

Проверяем типы:

-- нерекурсивный функтор
Nil                     :: L a l
Cons 'i' Nil            :: L Char (L a l)
Cons 'h' (Cons 'i' Nil) :: L Char (L Char (L a l))
-- тип List a (то есть Rec (L a)) как его неподвижная точка
In Nil                                 :: Rec (L a)
In (Cons 'a' (In Nil))                 :: Rec (L Char)
In (Cons 'a' (In (Cons 'b' (In Nil)))) :: Rec (L Char)

Ссылки:

Bananas in Space - классика жанра :)

Origami programming

Parametric Datatype-Genericity - сегодняшняя новинка (must read!)

Comments

[migmit.livejournal.com]

Ну, instance Functor не всегда получится - data X a b = X (a -> X b a) (смешной тип, я понимаю).
Меня ещё всегда забавляло, как в системе с рекурсивными типами примитив fix оказывается ненужным.

[deni-ok.livejournal.com]

Я ещё в бананах не дошёл до этого :(
Кофункторы или дифункторы?

[migmit.livejournal.com]

Я эту статью не дочитал, не знаю, что они там называют чем.
В данном случае, это будет контравариантный функтор. Вообще, насколько я понимаю, каноническая интерпретация рекурсивных типов делается через функтор C^opxC->C, где C - категория типов.

[deni-ok.livejournal.com]

Про контравариантный да, это понятно.

Похоже это то, что они дифункторами зовут:

class Difunctor f where
   dimap :: (a -> b) -> (c -> d) -> (f b c -> f a d)

instance Difunctor (->) where
   (f `dimap` g) h = g . h . f

data Rec f = In (f (Rec f) (Rec f))

[vshabanov.livejournal.com]

А в чем фишка? Зачем вместо простой записи делать функторы с fixpoint-ами. Что это дает?

[deni-ok.livejournal.com]

С точки зрения прикладного программирования - ничего. А вот для исследования стратегий трансформации и оптимизации функционального кода - довольно много. То есть руками, конечно, программист будет писать простые типы данных, а вот компилятор может их при необходимости перевести их в fixpoint-форму.

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

[vshabanov.livejournal.com]

А кто есть свободные теоремы? (догадываюсь, что откуда то из Theorems for free, но не читал)

[deni-ok.livejournal.com]

Они :)

http://deni-ok.livejournal.com/6909.html

[deni-ok.livejournal.com]

Ну а собственно свободная теорема - это та, которая следует исключительно из типа полиморфной функции:

Для любой f :: forall a . [a] -> [a] и любой g :: a -> b верно

map g . f = f . map g

Здесь = означает эквивалентность. При наличии в языке _|_ (жопа: ошибка или отсутствие останова) на g должно быть наложено требование строгости: g _|_ должно равняся _|_.

[vshabanov.livejournal.com]

Ага. Уже посмотрел в wadler.pdf
Вначале долго думал почему. Потом доперло, что она полиморфная, и элементы списка не трогает, только сам список.

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

bottom = жопа ))

Только не понял, почему требование строгости, м.б. наоборот нестрогости?

[deni-ok.livejournal.com]

Если wadler.pdf это мой, то пример на стр.48-50