Жесткая переменная в прикладной реализации - PullRequest
Новая
       85

Жесткая переменная в прикладной реализации

2 голосов
/ 04 августа 2020

Я получаю сообщение об ошибке компилятора для аппликативного экземпляра Safeness, например: 

{-# LANGUAGE InstanceSigs #-}

module Main where

main :: IO ()
main = pure ()


data Safeness a 
    = Unsafe a
    | Safe a
    | VerySafe a
    deriving (Eq, Show)


instance Functor Safeness where
    fmap :: (a -> b) -> Safeness a -> Safeness b
    fmap f (Unsafe x) = Unsafe $ f x
    fmap f (Safe x) = Safe $ f x
    fmap f (VerySafe x) = VerySafe $ f x


instance Applicative Safeness where
    pure :: a -> Safeness a
    pure x = Safe x

    (<*>) :: Safeness (a -> b) -> Safeness a -> Safeness b
    (<*>) (Safe f) (Safe x) = Safe $ f x       
    (<*>) (VerySafe f) (VerySafe x) = VerySafe $ f x    
    (<*>) _ x = x

Ошибка компилятора: 

    * Couldn't match type `a' with `b'
      `a' is a rigid type variable bound by
        the type signature for:
          (<*>) :: forall a b. Safeness (a -> b) -> Safeness a -> Safeness b      
        at C:\practise\app\Main.hs:27:14-58       
      `b' is a rigid type variable bound by
        the type signature for:
          (<*>) :: forall a b. Safeness (a -> b) -> Safeness a -> Safeness b      
        at C:\practise\app\Main.hs:27:14-58       
      Expected type: Safeness b
        Actual type: Safeness a
    * In the expression: x
      In an equation for `<*>': (<*>) _ x = x
      In the instance declaration for `Applicative Safeness'
    * Relevant bindings include
        x :: Safeness a
          (bound at C:\practise\app\Main.hs:30:13)
        (<*>) :: Safeness (a -> b) -> Safeness a -> Safeness b
          (bound at C:\practise\app\Main.hs:28:5) 
   |
30 |     (<*>) _ x = x       
   |

Я понимаю этот b не обязательно должен совпадать с a, но может; и я всегда заставляю его быть таким же в определенном случае. Что в этом не так, и как еще я могу кодировать это для предполагаемой функциональности?

1 Ответ

3 голосов
/ 04 августа 2020

Проблема, как указано в сообщении об ошибке, заключается в следующем: 

(<*>) _ x = x

Давайте дадим первому аргументу имя для ясности и предоставим «дырку» для тела: 

(<*>) f x = _

Затем компилятор сообщит нам: 

/Users/jpurdy/Code/Safe.hs:24:17: error:
    • Found hole: _ :: Safeness b
    …
    • Relevant bindings include
        x :: Safeness a
        f :: Safeness (a -> b)
        (<*>) :: Safeness (a -> b) -> Safeness a -> Safeness b

Единственные значения, которые вы можете вернуть: Unsafe (_ :: b), Safe (_ :: b) или VerySafe (_ :: b), поэтому вы должны указать b; с помощью параметризации only вы можете получить b, сопоставив f, чтобы получить a -> b, и сопоставив x, чтобы получить a, и применив функцию к Значение. Другими словами, вы не можете просто вернуть x без изменений.

К сожалению, решение зависит от того, что вы хотите сделать. Вы можете пометить результат с помощью минимум безопасности двух аргументов: 

VerySafe f <*> VerySafe x = VerySafe $ f x
VerySafe f <*> Safe x     = Safe $ f x
VerySafe f <*> Unsafe x   = Unsafe $ f x

Safe f     <*> VerySafe x = Safe $ f x
Safe f     <*> Safe x     = Safe $ f x
Safe f     <*> Unsafe x   = Unsafe $ f x

Unsafe f   <*> VerySafe x = Unsafe $ f x
Unsafe f   <*> Safe x     = Unsafe $ f x
Unsafe f   <*> Unsafe x   = Unsafe $ f x

И это проще, если вычесть параметр безопасности из вашего типа (в алгебре типов от * 1029 от * a + a + a до 3 × a ): 

data Safety = Unsafe | Safe | VerySafe
  deriving (Eq, Ord)

data Safeness a = Safeness Safety a

instance Applicative Safeness where

  -- Combine safeties with ‘min’, or use
  -- ‘deriving (Semigroup, Monoid) via (Min Safety)’
  -- to use the Semigroup ‘<>’ operator.
  Safeness s1 f <*> Safeness s2 x
    = Safeness (min s1 s2) (f x)

  -- Must use ‘VerySafe’ instead of ‘Safe’
  -- since it’s the identity for ‘min’,
  -- to satisfy the ‘Applicative’ laws.
  -- (Or respectively ‘mempty’ = ‘maxBound’.)
  pure = Safeness VerySafe

Или вы можете пофантазировать и использовать GADT для поднятия параметра безопасности до уровня типа, вышесказанного экземпляр Applicative, но позволяет комбинировать только значения с одинаковой безопасностью: 

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}

data Safety = U | S | V

data Safeness (s :: Safety) a where
  VerySafe :: a -> Safeness 'V a
  Safe     :: a -> Safeness 'S a
  Unsafe   :: a -> Safeness 'U a

apply :: Safeness s (a -> b) -> Safeness s a -> Safeness s b
apply (VerySafe f) (VerySafe x) = VerySafe (f x)
apply (Safe f)     (Safe x)     = Safe (f x)
apply (Unsafe f)   (Unsafe x)   = Unsafe (f x)
-- (Other cases are impossible because ‘s’ won’t match.)

В качестве дополнения вы можете использовать расширение DeriveFunctor для записи deriving (Functor) для Safeness.

...