Skip to content

Instantly share code, notes, and snippets.

@deniok

deniok/Fp06.hs Secret

Last active Oct 11, 2020
Embed
What would you like to do?
FP_HSE2020Fall_06
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE RankNTypes #-}
module Fp06 where
-- Функции, равные экстенсионально, но не интенсионально
suc, suc' :: (forall a. (a -> a) -> a -> a) -> (a -> a) -> a -> a
suc = \n s z -> n s (s z)
suc' = \n s z -> s (n s z)
zero, one, two :: (a -> a) -> a -> a
zero = \s z -> z
one = \s z -> s z
two = \s z -> s (s z)
{-
*Fp06> suc two (+1) 0
3
*Fp06> suc' two (+1) 0
3
*Fp06> suc two ([42]++) []
[42,42,42]
*Fp06> suc' two ([42]++) []
[42,42,42]
-}
{-
Полиморфизм второго ранга необходим, чтобы мы не могли передавать
в качестве первого аргумента ничего, кроме чисел Черча.
Без него экстенсионального равенства нет
-}
suc'', suc''' :: ((a -> a) -> a -> a) -> (a -> a) -> a -> a
suc'' = \n s z -> n s (s z)
suc''' = \n s z -> s (n s z)
{-
Prelude> suc'' (\s z -> if z == 0 then 5 else 4) (+1) 0
4
Prelude> suc''' (\s z -> if z == 0 then 5 else 4) (+1) 0
6
-}
-- Производные представители (Derived Instances)
data Point a = Point a a
deriving Eq
-- Point 3 5 == Point 3 5
-- В GHC можно и отдельно
-- (подключив расширение StandaloneDeriving)
deriving instance Show a => Show (Point a)
{-
GHCi> Point 3 5
Point 3 5
-}
-- вспомогательная эмуляция низкоуровневой реализации
eqInt :: Int -> Int -> Bool
eqInt x y = x == y
-- словарь для Eq', то есть запись из его методов
data Eq' a = MkEq { eq,ne :: a -> a -> Bool }
-- функции-селекторы выбирают методы равенства и неравенства из этого словаря
{-
GHCi> :t eq
eq :: Eq' a -> a -> a -> Bool
GHCi> :t ne
ne :: Eq' a -> a -> a -> Bool
-}
-- объявления instance транслируются в функции, возвращающие словарь...
dEqInt :: Eq' Int
dEqInt = MkEq {
eq = eqInt,
ne = \x y -> not $ eqInt x y
}
-- ... или в функции, принимающие некоторый словарь и возвращающие более сложный словарь
dEqList :: Eq' a -> Eq' [a]
dEqList (MkEq e _) = MkEq {
eq = el,
ne = \x y -> not $ el x y
} where
el [] [] = True
el (x:xs) (y:ys) = x `e` y && xs `el` ys
el _ _ = False
-- Функция elem теперь принимает словарь в качестве явного параметра
elem' :: Eq' a -> a -> [a] -> Bool
elem' _ _ [] = False
elem' d x (y:ys) = eq d x y || elem' d x ys
{-
GHCi> elem' dEqInt 2 [3,5,2]
True
GHCi> elem' dEqInt 2 [3,5,7]
False
GHCi> elem' (dEqList dEqInt) [3,5] [[4],[1,2,3],[3,5]]
True
GHCi> elem' (dEqList dEqInt) [3,5] [[4],[1,2,3],[3,8]]
False
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.