Skip to content

Instantly share code, notes, and snippets.

@deniok

deniok/Fp14.hs Secret

Created Dec 3, 2020
Embed
What would you like to do?
FP_HSE2020Fall_14
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment