Бананы, линзы, оригами и примкнувшая к ним сегодня натуральность 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

[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))