FP_HSE2020Fall_06

Fp06.hs

{-# 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
-}