FP_HSE2020Fall_14

Fp14.hs

{-# LANGUAGE StandaloneDeriving, FlexibleContexts, UndecidableInstances #-}
module Fp14 where

newtype Fix f = In { out :: f (Fix f) }
-- ср. fix f = f (fix f)
deriving instance Show (f (Fix f)) => Show (Fix f)
deriving instance Eq (f (Fix f)) => Eq (Fix f)

{-
GHCi> :k Fix
Fix :: (* -> *) -> *
GHCi> :t In
In :: f (Fix f) -> Fix f
GHCi> :t out
out :: Fix f -> f (Fix f)
-}


-- data Nat = Z | S Nat

-- функтор, описывающий структуру типа
-- N = \X. 1 + X
data N x = Z | S x deriving Show

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

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

{-
нерекурсивный функтор
GHCi> :t Z
Z :: N x
GHCi> :t S Z
S Z :: N (N x)
GHCi> :t S (S Z)
S (S Z) :: N (N (N x))
тип Nat, то есть Fix N, как его неподвижная точка
GHCi> :t In Z
In Z :: Fix N
GHCi> :t S (In Z)
S (In Z) :: N (Fix N)
GHCi> :t In (S (In Z))
In (S (In Z)) :: Fix N
GHCi> :t In (S (In (S (In Z))))
In (S (In (S (In Z)))) :: Fix N
-}


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

-- функтор, описывающий структуру типа
-- L = \A. \X. 1 + A * X
data L a l = Nil | Cons a l deriving Show

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

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

{-
-- нерекурсивный функтор
GHCi> :t Nil
Nil :: L a l
GHCi> :t Cons 'i' Nil
Cons 'i' Nil :: L Char (L a l)
GHCi> :t Cons 'h' $ Cons 'i' Nil
Cons 'h' $ Cons 'i' Nil :: L Char (L Char (L a l))
--тип List Char, то есть Fix (L Char), как его неподвижная точка
GHCi> :t In Nil
In Nil :: Fix (L a)
GHCi> :t In $ Cons 'i' $ In Nil
In $ Cons 'i' $ In Nil :: Fix (L Char)
GHCi> :t In $ Cons 'h' $ In $ Cons 'i' $ In Nil
In $ Cons 'h' $ In $ Cons 'i' $ In Nil :: Fix (L Char)
-}


-----------------------------------------------------------------

-- Рассмотрим преобразование 
copy :: Functor f => Fix f -> Fix f
copy (In x) = In (copy <$> x)

-- Утверждение: это преобразование есть тождество.

{-
Напишем обобщение copy, которое заменяет In :: f (Fix f) -> Fix f не на себя же, 
а на произвольную phi :: f a -> a.
(Для данных функтора f и типа a функция phi :: f a -> a известна как f-алгебра.)
-}
type Algebra f a = f a -> a
{-
Получим обобщение понятия свёртки, катаморфизм:
-}

cata :: Functor f => Algebra f a -> Fix f -> a   -- Functor f => (f a -> a) -> Fix f -> a
cata phi (In x) = phi (cata phi <$> x)

{-
A useful mnemonic is to think of a catastrophe destroying something.
-}

-- Если в примере с функтором N задать функцию phi, заменяющую Z на 0, а S на succ, 
-- то получим N-алгебру типа N Int -> Int
phiN :: Algebra N Int -- алиас для N Int -> Int
phiN Z     = 0
phiN (S n) = succ n

-- Применяя cata к этой алгебре, получим стандартный преобразователь 
natToInt :: Nat -> Int -- алиас для Fix N -> Int
natToInt = cata phiN

{-
GHCi> natToInt $ In (S (In (S (In Z))))
2
-}

-- Пример (L a)-алгебры
phiL :: Algebra (L a) [a] -- алиас для L a [a] -> [a]
phiL Nil         = []
phiL (Cons e es) = e : es

listify :: List a -> [a] -- алиас для Fix (L a) -> [a]
listify = cata phiL
{-
GHCi> listify $ In Nil
[]
GHCi> listify $ In $ Cons 'i' $ In Nil
"i"
GHCi> listify $ In $ Cons 'h' $ In $ Cons 'i' $ In Nil
"hi"
-}

-- Ещё пара списочных алгебр

phiLLen :: Algebra (L a) Int --  L a Int -> Int
phiLLen Nil         = 0
phiLLen (Cons _ es) = 1 + es

phiLSum :: Num a =>  Algebra (L a) a -- Num a => L a a -> a
phiLSum Nil         = 0
phiLSum (Cons e es) = e + es
{-
GHCi> cata phiLLen $ In $ Cons 'h' $ In $ Cons 'i' $ In Nil
2
GHCi> cata phiLSum $ In $ Cons 2 $ In $ Cons 3 $ In Nil
5
-}

{-
Конструктор In :: f (Fix f) -> Fix f сам является алгеброй
(с носителем Fix f)
-}
phiIn :: Algebra f (Fix f)
phiIn = In
{-
Эта алгебра называется инициальной алгеброй.


Инициальная алгебра сохраняет всю информацию о 
структуре, поданной на вход. Ее катаморфизм --- 
тождественная функция
-}

copy'' :: Functor f => Fix f -> Fix f
copy'' = cata phiIn  -- == id

{-
Имеется уникальный гомоморфизм из инициальной алгебры
в любую другую с данным функтором \lstinline!f!. 

ЗАКОНЫ

(1 cata-cancel) 
cata phi . In == phi . fmap (cata phi)

(2 cata-refl)
cata In == id

(3 cata-fusion)
f . phi == phi . fmap f => f . cata phi == cata phi

(4 cata-compose)
eps :: f :~> g => 
cata phi . cata (In . eps) == cata (phi . eps)

-}


----------------------------------------------------------------------

-- Анаморфизм

-- Введём операцию, обратную In
--out :: Fix f -> f (Fix f)
--out (In x) = x

-- Рассмотрим преобразование рекурсивного типа в себя
copy' :: Functor f => Fix f -> Fix f
copy' x = In (copy' <$> out x)

-- Утверждение: это преобразование есть тождество.

{-
--  Покажем что copy' = id на примере выражения In (S (In (S (In Z)))) типа Nat:
copy'               (In (S (In (S (In Z)))))   ~> по def copy'
In (fmap copy' (out (In (S (In (S (In Z))))))  ~> по def out
In (fmap copy'          (S (In (S (In Z))))    ~> по def fmap
In (S (copy'               (In (S (In Z)))))   ~> по def copy'
In (S (In (fmap copy' (out (In (S (In Z))))))) ~> по def out
In (S (In (fmap copy'          (S (In Z)))))   ~> по def fmap
In (S (In (S (copy'               (In Z)))))   ~> по def copy'
In (S (In (S (In (fmap copy'(out  (In Z))))))) ~> по def out
In (S (In (S (In (fmap copy'          Z)))))   ~> по def fmap
In (S (In (S (In Z)))))
-}

-- Заменим в copy' каждое вхождение out :: Fix f -> f (Fix f) 
-- на произвольную функцию psi :: a -> f a 

type Coalgebra f a = a -> f a 

-- Получим нотацию анаморфизма
ana :: Functor f => Coalgebra f a -> a -> Fix f
ana psi x = In (ana psi <$> psi x)

-- Пример 

psiN :: Coalgebra N Int   -- Int -> N Int
psiN 0 = Z
psiN n = S (n-1)

-- задает анаморфизм
intToNat :: Int -> Nat
intToNat = ana psiN

{-
GHCi> intToNat 3
In {out = S (In {out = S (In {out = S (In {out = Z})})})}
-}

{-
Терминальная коалгебра
Функция out :: Fix f -> f (Fix f) является коалгеброй
-}

psiOut :: Coalgebra f (Fix f)
psiOut = out

copy''' :: Functor f => Fix f -> Fix f
copy''' = ana psiOut  -- == id

-------------------------------------------------------

{-
Гилеморфизм (Hylomorphism) - последовательное применение 
анаморфизма, а затем катаморфизма:
-}

hylo :: Functor f => Algebra f a -> Coalgebra f b -> b -> a
hylo phi psi = cata phi . ana psi

phiLProd ::  Algebra (L Integer) Integer 
phiLProd Nil         = 1
phiLProd (Cons e es) = e * es

psiLToZero :: Coalgebra (L Integer) Integer
psiLToZero 0 = Nil
psiLToZero n = Cons n (n-1)

factorial :: Integer -> Integer
factorial = hylo phiLProd psiLToZero 

{-
> factorial 5
120
> factorial 100
93326215443944152681699238856266700490715968264381621468592963895217599993229915
608941463976156518286253697920827223758251185210916864000000000000000000000000

Эффективность не страдает! 
Все надстройки стираются при компиляции и отсутствуют в рантайме.
-}

{-
Ката- и аноморфизмы легко выразить через гилеморфизм:
-}

cata' :: Functor f => Algebra f a -> Fix f -> a
cata' phi = hylo phi out 

ana' :: Functor f => Coalgebra f a -> a -> Fix f
ana' psi = hylo In psi